The first open-source release of the platform was made in 2008. Major versions are named after chemical elements, and since version 11 (Sodium) the version number has matched the element's atomic number; for example, version 32 is Germanium and version 33 is Arsenic. Release 33.0 (Arsenic) was published on 24 July 2026.
Significant changes across releases include:
Eva: the value analysis plug-in became consistently named "Eva" in version 18.0 (Argon, October 2018).
E-ACSL: included in the standard distribution from version 15.0 (Phosphorus, May 2017).
WP: the legacy WP engine and its native prover output were removed in version 25.0 (Manganese, June 2022), so WP now always goes through Why3; counterexample generation was added in version 29.0 (Copper, June 2024).
Graphical interface: a new Electron-based GUI, Ivette, was introduced in version 25.0. In version 33.0 the old GTK-based interface was removed and frama-c-gui now launches the new GUI.
Concurrency: the Mthread plug-in, which uses Eva to analyze concurrent C programs, was embedded in Eva in version 31.0 (Gallium, June 2025).
Architecture
This section is missing information about use of Clang for C++ input at least since 2014. Please expand the section to include this information. Further details may exist on the talk page.(September 2021)
Frama-C has a modular plugin architecture comparable to that of Eclipse (software) or GIMP.
Eva (evolved value analysis, formerly "Value analysis") – computes a set of possible values for each variable in a program using abstract interpretation techniques; many other plug-ins use its results.
Jessie – an older deductive verification plug-in built on the Why 2 platform, which sent proof obligations to automatic or interactive provers. The Why 2 platform is no longer under active development, as its authors' efforts moved to Why3, and the last Frama-C version it is documented as compatible with is Chlorine (version 17). Deductive verification is now mainly done with the WP plug-in.
WP (Weakest Precondition) – verifies ACSL properties deductively. It is parameterized by memory model, cooperates with other Frama-C plug-ins such as Eva, and calls external automatic and interactive provers through the Why3 platform; version 33.0 added automatic detection of installed external provers.
E-ACSL– (for Executable ACSL) instruments a program to perform runtime verification of properties, possibly in complement with other plugins such as value analysis and WP (e.g. by checking assertions at runtime for the properties that could not be statically verified with the other plugins).
Impact analysis– highlights the impacts of a modification in the C source code.
Slicing– enables slicing of a program. It enables generation of a smaller new C program that preserves some given properties.
Spare code– removes useless code from a C program.
MetAcsl – a plug-in for expressing, in a compact way, properties that would otherwise need very many ACSL annotations, mainly security properties such as guarded access to sensitive memory locations.
Frama-Clang – an experimental C++ front-end for Frama-C based on the Clang compiler.
Features
Frama-C can be used for the following purposes:
To understand C code which you have not written. In particular, Frama-C enables one to observe a set of values, slice the program into shorter programs, and navigate in the program.
To prove formal properties on the code. Using specifications written in ANSI/ISO C Specification Language enables it to ensure properties of the code for any possible behavior. Frama-C handles floating point numbers.
To enforce coding standards or code conventions on C source code, by means of custom plugin(s)
To instrument C code against some security flaws
Industrial use
Frama-C is aimed at the verification of industrial-size C programs, combining static analysis, deductive verification and testing for safety and security-critical software. It is used for teaching, experimental research and industrial applications, and a 2024 guidebook collects industrial case studies in which it was used to verify safety or security properties. A 2021 overview in Communications of the ACM discusses its use in education and in industrial collaborations.
In the avionics domain, a study at the German company ESG formalized the low-level specification of a software function from a DO-178C-compliant project in ACSL and partially verified the source code with Frama-C's WP plug-in, using Alt-Ergo as the automated prover.
Further reading
Kosmatov, Nikolai; Prevosto, Virgile; Signoles, Julien, eds. (2024). Guide to Software Verification with Frama-C. Springer. doi:10.1007/978-3-031-55608-1.
