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.