Agentic Software Specification and Verification with Frama-C

Institution

The French Alternative Energies and Atomic Energy Commission (CEA) is a key player in research, development, and innovation. Drawing on the widely acknowledged expertise gained by its 20,000+ staff spanned over 9 research centers with a budget of 4.1 billion Euros, CEA actively participates in more than 400 European collaborative projects with a large number of academic (notably as a member of Paris-Saclay University) and industrial partners. Within the CEA Technological Research Division, the CEA List institute addresses the challenges coming from smart digital systems.

Among other activities, CEA List’s Software Safety and Security Laboratory (LSL) research teams design and implement automated analysis in order to make software systems more trustworthy, to exhaustively detect their vulnerabilities, to guarantee conformity to their specifications, and to accelerate their certification. In particular, the Frama-C platform is dedicated to perform a wide range of analyses over C programs (with an experimental C++ front-end).

Motivation

Frama-C is a software platform dedicated to the formal verification of C programs via a wide set of program analysis technics provided as plugins. It is often used in the context of critical software development (in aeronautics, railways, nuclear industry, etc.), where regulations impose very stringent code verification objectives, and integrated as part of a broader safety and/or security validation process.

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 (Lathouwers and Huisman 2024). However, to integrate LLMs into formal verification workflows, we must first understand whether and how their inherent limitations, such as hallucination and the lack of formal guarantees, can be mitigated in a context where correctness is paramount.

Objectives of the Internship

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 (Granberry, Ahrendt, and Johansson 2025). 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 (Mattar et al. 2025).

• 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.

Expected Outcomes

The internship is expected to deliver:

• A prototype framework integrating an LLM with Frama-C to assist in specification and verification tasks.

• A systematic evaluation of the approach on representative C programs.

• A report analyzing the feasibility, limitations, and potential of AI-assisted formal verification workflows.

Qualifications

• Minimal

  • Master student in Computer Science or Computer Engineering (M1/M2).
  • Interest in AI-assisted software engineering and 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.

Characteristics

• Duration: 5-6 months

• Location: CEA Nano-INNOV, Paris-Saclay Campus, France (Work From Home possible up to 2-3 days/week)

• Compensation:

  • €1300 (Bac+4/M1), €1400 (Bac+5/M2) monthly stipend
  • Maximum €229 housing and travel expense monthly allowance (in case a relocation is needed)
  • CEA shuttle in Paris region and 75% refund of transit pass
  • Subsidized lunches

Application

If you are interested in this internship, please send to the contact persons an application containing:

• Your resume
• A cover letter indicating how your curriculum and experience match the qualifications expected and how you would plan to contribute to the project
• Your bachelor and master transcripts, if any
• The contact details of two persons (at least one academic) who can be contacted to provide references

Applications are welcome until the position is filled. Please note that the administrative processing may take up to 3 months.

Contact persons

For further information or details about the internship before applying, please contact:

• Virgile Prevosto (virgile.prevosto@cea.fr)
• Michele Alberti (michele.alberti@cea.fr)

References