Protocol testing using large language models

A system, comprising:

• at least one processor;
• memory in electronic communication with the at least one processor;
• and
• instructions stored in the memory, the instructions being executable by the at least one processor to:
• generate a model generation prompt including a description of a protocol and instructions associated with generating protocol models;
• provide the model generation prompt as an input to a large language model (LLM);
• obtain a modeled component of the protocol, the modeled component of the protocol including executable code generated by the LLM based on the model generation prompt provided as the input to the LLM;
• generate a symbolic harness based on the model generation prompt and based on one or more validity constraints associated with inputs to be handled by the modeled component output by the LLM;
• and
• apply a symbolic execution engine to the modeled component of the protocol based on the symbolic harness to generate a plurality of protocol tests associated with the modeled component of the protocol and which satisfy the one or more validity constraints of the symbolic harness.

A non-transitory computer readable medium storing instructions thereon that, when executed by at least one processor, cause a computing device to:

• generate a model generation prompt including a description of a protocol and instructions associated with generating protocol models;
• provide the model generation prompt as an input to a large language model (LLM);
• obtain a modeled component of the protocol, the modeled component of the protocol including executable code generated by the LLM based on the model generation prompt provided as the input to the LLM;
• generate a symbolic harness based on the model generation prompt and based on one or more validity constraints associated with inputs to be handled by the modeled component output by the LLM;
• and
• apply a symbolic execution engine to the modeled component of the protocol based on the symbolic harness to generate a plurality of protocol tests associated with the modeled component of the protocol and which satisfy the one or more validity constraints of the symbolic harness.