LMF, winner of VerifyThis 2026, will present Creusot at Rust Paris

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.

This event follows a major achievement at VerifyThis 2026, the international program verification competition held in Turin as part of ETAPS. Among 24 participating teams, Li-yao Xia and Jacques-Henri Jourdan received the Best Overall Team award. The LMF was also honored with the Best One-Person Team award, presented to Jean-Christophe Filliâtre.

These results highlight both the quality of the LMF’s work in formal verification and the growing importance of Creusot.