Projects
I work on infrastructure for Lean-based formal verification: structured mathematical documents, efficient access to the proof engine, experiments with Lean-generated programs, and prototypes for editor and runtime support.
Verso Blueprint is a Lean package for writing structured proof blueprints in Verso. A blueprint connects mathematical exposition with Lean code and declarations, so a formalization plan can be read as a document and checked against the formal development.
It renders navigable HTML with previews, dependency graphs, progress summaries, and metadata for downstream tools.
Other current work
lean-beam is a Claude/Codex skill and local workflow layer for efficient interaction with Lean 4, including experiments around proof-engine access and Monte-Carlo Tree Search.
lean-vir is a proof-of-concept path from Lean 4 IR to wasm32-wasi, useful for exploring how Lean programs and generated artifacts can move toward WebAssembly.
Tech Demos
ml-lab is a Lean-first laboratory for OCaml bytecode and ZAM simulation, giving runtime and bytecode experiments a checked, programmable setting.
imp-lab is a Lean playground for programming-language modeling tooling, centered on small imperative languages and experiments around semantics.
lean-fir is a formally verified compiler from Lean's LCNF intermediate representation to WebAssembly.
lean-mirror packages Lean 4 language support for CodeMirror 6, with a thin LSP client layer, browser transports, and a small demo around lean --server.
Previous projects
Flèche and rocq-lsp
Flèche is a new document processing engine for the Rocq Prover. Flèche is based on state-of-the-art incremental computing techniques and was designed to support real-time checking of hybrid and literate proof documents. Flèche is used, among others, in the following sub-projects that I also co-maintain:
-
rocq-lsp: a LSP server for the Rocq Prover.
-
jsCoq 2: interactive rich documents, run Rocq in your browser!
-
pétanque: lightweight programmatic interaction with the Rocq Prover.
Dune Build System for Rocq
Dune is an industrial-grade build system with great features and performance. We extended Dune to support Rocq projects, supporting most of Dune's key features such as caching and compositional builds. See Dune's Rocq Build Language Documentation for more details and a quick-start guide.
The Rocq Prover
The Rocq Prover is an award-winning interactive theorem prover based on the Calculus of Constructions. I was a member of Rocq's core team from 2015 to 2025, helping co-maintain and design several components, including Rocq's build system, the vernacular layer, and the continuous integration system.