Add new article about verifythis and next rust in paris event

content/en/post/03_verifythis_winners_and_creusot_at_rust_paris.md

@@ -0,0 +1,29 @@
+---
+date: 2026-04-29T17:00:00+02:00
+description: "LMF will soon take part in a Rust Paris meetup with a presentation dedicated to Creusot, its formal verification tool for Rust programs."
+featured_image: '/images/verifythis2026.jpg'
+thumbnail: '/images/verifythis2026.jpg'
+tags: ["event", "creusot", "rustparis"]
+title: "LMF, winner of VerifyThis 2026, will present Creusot at Rust Paris"
+---
+
+LMF will soon participate to **[Rust Paris
+2026](https://event.systematic-paris-region.org/rustparis/)** 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**.

content/fr/post/03_verifythis_winners_and_creusot_at_rust_paris.md

@@ -0,0 +1,32 @@
+---
+date: 2026-04-29T17:00:00+02:00
+description: "Le LMF participera prochainement à un meetup Rust Paris le 9 juin 2026 avec une présentation consacrée à Creusot, son outil de vérification formelle de programmes Rust."
+featured_image: '/images/verifythis2026.jpg'
+thumbnail: '/images/verifythis2026.jpg'
+tags: ["event", "creusot", "rustparis"]
+title: "Le LMF, lauréat de VerifyThis 2026, présentera Creusot à Rust Paris"
+---
+
+Le LMF participera prochainement **[Rust Paris
+2026](https://event.systematic-paris-region.org/rustparis/)** le 9 juin 2026
+avec une présentation consacrée à **Creusot**, son outil de vérification
+formelle de programmes Rust.
+
+Lors de cette présentation, **Li-yao Xia** (ingénieur R&D) et **Jacques-Henri Jourdan**
+(chargé de recherche) expliqueront comment **Creusot** permet de prouver l’absence
+de certaines classes d’erreurs dans les programmes Rust grâce à la vérification
+déductive. Cette approche repose sur l’écriture de contrats de fonctions,
+c’est-à-dire de spécifications formelles décrivant précisément le comportement
+attendu des fonctions. L’exposé présentera également plusieurs études de cas de
+bibliothèques et d’applications vérifiées avec Creusot.
+
+Cet événement fait suite à un résultat majeur obtenu lors de **VerifyThis 2026**,
+le concours international de vérification de programmes organisé à Turin dans
+le cadre d’**ETAPS**. Parmi 24 équipes participantes, **Li-yao Xia** et **Jacques-Henri**
+**Jourdan** ont reçu le prix de la **Best Overall Team**. Le LMF a également été
+distingué avec le prix de la **Best One-Person Team**, décerné à **Jean-Christophe**
+**Filliâtre**.
+
+Ces résultats soulignent à la fois la qualité des travaux du LMF en
+vérification formelle et l’importance croissante de **Creusot**.
+