Although formal verification is essential for ensuring the safety and security of software, it remains difficult to deploy and use effectively by non-experts due to its steep learning curve. Recent advances in large language models (LLMs) have demonstrated remarkable abilities in code understanding, synthesis, and reasoning. These advances open promising research directions for assisting developers and verification engineers in formal specification and verification tasks.

The goal of this internship is to explore and evaluate the integration of LLMs assistance into the Frama-C environment to support and automate parts of the specification and verification workflow. The work will focus on identifying the extent to which LLMs can provide meaningful support without compromising the rigor and reliability of formal program analysis.
The following topics represent potential research and technical directions of the internship. Depending on the interests of the intern, one or more of them will be pursued, or other directions might be devised as the internship progresses.

1. Automatic Specification Synthesis: Use LLMs to infer program specifications, selecting an appropriate formalism (e.g., ACSL, MetAcsl, RPP), and explore strategies to evaluate the robustness of synthesized specifications themselves, e.g., using Frama-C’s infrastructure or counterexample-based refinement.
2. Assistance in Verification Configuration: Design mechanisms for LLMs to suggest appropriate Frama-C plugins (e.g., Wp, Eva, E-ACSL, RTE) and configurations or parameters based on the characteristics of
   the analyzed code and objectives.
3. Assessment and Prioritization of Verification Results: When potential issues are reported, develop an LLM-assisted process to classify their severity and likelihood of exploitation, providing a prioritized and interpretable view of verification results, potentially in combination with Frama-C’s results themselves.

All these potential directions raise several challenges at the intersection of software engineering, artificial intelligence, and formal methods.

• Integration Challenge: Setting up an environment where LLMs can interact programmatically with Frama-C, interpret analysis feedback, and refine their outputs iteratively. This can build upon the Loupe framework.
• Reliability and Hallucination Control: Designing mechanisms to detect, quantify, and reduce hallucinations or incorrect inferences produced by the model, possibly through cross-validation against Frama-C’s analysis results.
• Evaluation Metrics: Defining criteria for assessing the quality and usefulness of AI-generated specifications and test cases, both in terms of correctness and their impact on verification coverage.
• Human-AI Collaboration: Studying how AI-generated suggestions can be presented to the user to maximize productivity and trust, ensuring the expert remains in control of final verification decisions.

• Required

  • Interest in AI-assisted software engineering

  • Willingness to explore interactions between LLMs
    and formal verification frameworks

  • Solid knowledge of Python and its ecosystem

  • Ability to work in a team

• Preferred
  • Familiarity with machine learning and large language models, including prompt design or API integration.
  • Familiarity with the Frama-C platform.
  • Some knowledge of the OCaml and C programming languages