LIO*: Low Level Information Flow Control in F. - Jean-Joseph Marty; Lucas Franceschino; Jean-Pierre Talpin; Niki Vazou (CoRR, 2020)

Verified Functional Programming of an Abstract Interpreter. - Lucas Franceschino; David Pichardie; Jean-Pierre Talpin (SAS, 2021)

Programmation vérifiée à l'intersection des types dépendants et de l'analyse statique. (Verified Programming at the Intersection of Dependent Types and Static Analysis). - Lucas Franceschino (2021)

Charon: An Analysis Framework for Rust. - Son Ho; Guillaume Boisseau; Lucas Franceschino; Yoann Prak; Aymeric Fromherz; Jonathan Protzenko (CAV (4), 2025)

hax: Verifying Security-Critical Rust Software using Multiple Provers. - Karthikeyan Bhargavan; Maxime Buyse; Lucas Franceschino; Lasse Letager Hansen; Franziskus Kiefer; Jonas Schneider-Bensch; Bas Spitters (IACR Cryptol. ePrint Arch., 2025)