Tours, France | Head of Core Engineering at Nomadic Labs

I study how to build reliable software when agents write most of the code, connecting first principles, formal methods, and production engineering.

Before joining the Tezos ecosystem, I spent fifteen years as an Associate Professor in Computer Science. My work has moved between programming languages, proof engineering, developer education, and systems operated in production.

Read the essays: Software engineering in the agent era

At Nomadic Labs, I help lead the engineering of the Tezos protocol and its infrastructure. My current work includes protocol evolution, Tezos X, Smart Rollups, performance, and the use of formal reasoning in production engineering.

I also write living essays about a question that code agents make hard to ignore: when producing code becomes cheap, how do we establish that we built the right thing?

• The Code Agent Crisis
• Why a loop at all
• Talks and conversations
• Revision history

These projects are part of the path that led to my current work.

• Learn-OCaml, a platform for teaching and assessing OCaml programming.
• OCaml with copatterns, an experimental OCaml extension.

• Morbig, a static parser for the POSIX shell language.
• Parsing JavaScript's automatic semicolon insertion, an executable investigation of a famously subtle language rule.

• FreeSpec, a Coq framework for specifying, executing, and certifying impure computations.

• Maplume, a word tracker for writers.
• srit, a terminal speed-reading tool.
• revisor, a clipboard interface for working with language models.

My earlier research covers functional programming, programming-language semantics, proof engineering, incremental computation, parsing, and critical software verification.

• Google Scholar
• Research contributions and conference record

• Blog
• X
• GitHub

Unless explicitly stated otherwise, the views expressed here are my own and do not represent Nomadic Labs.