LMF will soon participate to Rust Paris 2026 with a presentation dedicated to Creusot on June 9, 2026, its formal verification tool for Rust programs.

During this presentation, Li-yao Xia (R&D Engineer) and Jacques-Henri Jourdan (Research Fellow) will explain how Creusot uses deductive verification to prove the absence of certain classes of errors in Rust programs. This approach relies on writing function contracts—that is, formal specifications that precisely describe the expected behavior of functions. The presentation will also feature several case studies of libraries and applications verified with Creusot.

On Thursday, March 13, 2025, all the partners of the Decysif project (TrustInSoft, AdaCore, OCamlPro, and the LMF team) gathered at the OCamlPro offices in Paris’s 14th arrondissement for the project’s plenary meeting!

It was the perfect occasion for these twenty engineers to come together and take stock of the progress on research topics, projects, and tools that are continuously growing and evolving!

It was also a great opportunity to review the remaining objectives and to discuss the organization and schedule of the work ahead.

We are thrilled to share that Alt-Ergo 2.6 has officially been released!

Alt-Ergo is an automated prover developped by OCamlPro widely used in formal verification, it plays a key role in static analysis frameworks like the TIS Analyzer, SPARK and Frama-C.

This latest version introduces a series of improvements and new features, particularly in bit-vector reasoning, model generation, and optimization.

The updates in Alt-Ergo 2.6 are directly tied to the progress made in the DéCySif joint research project between AdaCore, Inria, OCamlPro, and TrustInSoft.

On Tuesday, December 19, 2023, all partners of the Decysif project (TrustInSoft, AdaCore, OCamlPro, and the LMF team) gathered at the TrustInSoft offices in the 14th arrondissement of Paris for the project kickoff meeting!

It was a great opportunity to review the ambitious goals of the project, exchange between partners about the organization and agenda of the work. The meeting ended, as is often the case with these well-acquainted partners, with intense technical discussions on the interaction between Why3 (repository) and Alt-Ergo (repository), use cases for testing Creusot (code source), and techniques for detecting vulnerabilities using TIS Analyzer (repository of the OS kernel) or Spark (repository).