Mi-Cho-Coq, a Framework for Certifying Tezos Smart Contracts. - Bruno Bernardo; Raphaël Cauderlier; Zhenlei Hu; Basile Pesin; Julien Tesson (FM Workshops (1), 2019)

Albert, An Intermediate Smart-Contract Language for the Tezos Blockchain. - Bruno Bernardo; Raphaël Cauderlier; Basile Pesin; Julien Tesson (Financial Cryptography Workshops, 2020)

Making Tezos Smart Contracts More Reliable with Coq. - Bruno Bernardo; Raphaël Cauderlier; Guillaume Claret; Arvid Jakobsson; Basile Pesin; Julien Tesson (ISoLA (3), 2020)

Programming microcontrollers through high-level abstractions. - Steven Varoumas; Basile Pesin; Benoît Vaugon; Emmanuel Chailloux (VMIL@SPLASH, 2020)

Verified Lustre Normalization with Node Subsampling. - Timothy Bourke; Paul Jeanmaire; Basile Pesin; Marc Pouzet (ACM Trans. Embed. Comput. Syst., 2021)

Verified Compilation of a Synchronous Dataflow Language with State Machines. (Compilation vérifiée d'un langage synchrone à flots de données avec machines à états). - Basile Pesin (2023)

Verified Compilation of Synchronous Dataflow with State Machines. - Timothy Bourke; Basile Pesin; Marc Pouzet (ACM Trans. Embed. Comput. Syst., 2023)

Programming microcontrollers through high-level abstractions: The OMicroB project. - Steven Varoumas; Basile Pesin; Benoît Vaugon; Emmanuel Chailloux (J. Comput. Lang., 2023)

Formally Verified Hardening of C Programs against Hardware Fault Injection. - Basile Pesin; Sylvain Boulmé; David Monniaux; Marie-Laure Potet (CPP, 2025)