Frama-C, flawless C code analysis

Frama-C is a platform for analyzing programs written in C for critical systems in the nuclear energy, aeronautics, rail, health and other industries. It can guarantee the absence of any software errors and prove the conformity of code to formal properties. This tool has also recently been augmented with modules for verifying cybersecurity properties.


Verifying C code quality

Frama-C is a code analysis platform for programs written in C, capable of ensuring that code is safe and free of any cybersecurity vulnerabilities. It brings two notable qualities to the equation:

  • It can guarantee that code doesn’t contain any software bugs that could cause errors during execution.
  • It allows users to test and prove the conformity of a program to formal properties.

These two qualities make the tool particularly well-suited for nuclear energy, aeronautics, rail, health, and other contexts where there are very stringent requirements for verification, or contexts involving a volume of cases to test that exceeds what conventional tools can handle.

The software is built around a core that manages the code being analyzed and added modules that are specialized for various functionalities. Some are dedicated to a certain analysis technique (such as abstract interpretation, deductive analysis, dynamic property verification, etc.), while others verify specific types of properties, such as temporal and relational properties or global constraints. Still others help users navigate code to identify the causes of a problem, such as data or control dependency. The modules cooperate to diagnose software bugs by exchanging information (partial or final results, annotations, etc.) in a language dedicated for the purpose. They can do this both sequentially and simultaneously.

Recently, Frama-C was augmented with several modules, including one for cybersecurity specifications and verification.

The tool is known around the world and used by a large number of public-sector partners like ANSSI and partner companies like EDF and Thales Dassault Aviation also uses it for technology research.


Multiple analysis techniques and modular architecture

Main advantages:

  • Powerful performance driven by exhaustive analysis techniques.
  • Ability to verify the absence of any vulnerabilities.
  • Modules that work seamlessly together, offering wide flexibility in usage.
  • Open-source code that can be developed to respond to new needs in cybersecurity, digital sovereignty, and deep learning algorithm validation.

Frama-C is one of the few tools in the world to have passed the NIST (National Institute of Standards and Technology) Ockham Sound Analysis Criteria, satisfying the strictest of all requirements, guaranteed code immunity.

Use cases

Critical systems, cybersecurity, and more

  • Critical and/or embedded systems: ensuring the absence of software bugs by using formal verification, verifying functional properties and security properties (privacy, integrity, availability, etc.).
  • Artificial intelligence: analyzing libraries.
  • Cybersecurity: detecting vulnerabilities in programs, verifying countermeasure reliability.
  • Generating tests.
  • Education: Universities in France and abroad can use the software for instruction about testing, analyzing, and verifying programs, as well as more generally in software engineering programs.
Success story

Thales uses Frama-c to certify its smart card OS

Thales needed to certify the virtual machines—the code that executes applications—onboard its smart cards. The company identified two properties—integrity and privacy—that needed to be formally validated. Frama-C helped Thales reach this goal at the end of 2021, a first in the world of mass-produced smart cards.

Click here for more information


Addressing the latest software trends

Planned updates:

  • Analysis of programs that incorporate ML techniques.
  • Using AI techniques to facilitate analysis implementation. This was addressed by the H2020 Decoder project, which generated formal specifications based on natural language documentation, and continued in the LEIA project as part of the French government’s Grand Défi Cyber program.
  • Implementation of new software development and deployment methods (continuous integration) to reuse existing results for the analysis of a new version of a given code (a concept also addressed in the LEIA project).


The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. Patrick Baudin, François Bobot, David Bühler, Loïc Correnson, Florent Kirchner, Nikolai Kosmatov, André Maroneze, Valentin Perrelle, Virgile Prevosto, Julien Signoles, and Nicky Williams. 2021.. Commun. ACM 64, 8 (August 2021), 56–68.

Structuring Abstract Interpreters Through State and Value Abstractions, Sandrine Blazy, David Bühler and Boris Yakobowski. In Verification, Model Checking, and Abstract Interpretation (VMCAI), 2019

Logic against ghosts: Comparison of two Proof Approaches for a List Module SAC 2019, Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue. The 34th ACM/SIGAPP Symposium On Applied Computing, Apr 2019.

How testing helps to diagnose proof failures, Guillaume Petiot, Nikolaï Kosmatov, Bernard Botella, Alain Giorgetti, Jacques Julliand. Springer Verlag, 2018, 30 (6), pp.629 – 657.

Shadow state encoding for efficient monitoring of block-level properties,  Kostyantyn Vorobyov Julien Signoles Nikolai Kosmatov, Proceedings of the 2017 ACM SIGPLAN International Symposium on Memory Management.

MetAcsl: Specification and Verification of High-Level Properties Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall
TACAS (25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems), Avril 2019.


Go to Frama-C website

See also

Focus areas

Cybersecurity: toward safety and privacy by design

Cybersecurity is at the heart of digital sovereignty, and an essential constituent of modern societies. As a crucial element for peace and security in cyberspace, it is an invisible but key enabler fo...
Read more
Research programs

Formal methods

The purpose of the INCA program is to make sophisticated formal verification methods accessible to all companies that develop code.
Read more