Nomadic Labs · 2024—present
Scaling Tezos data availability
Tech-led the work that raised the Data Availability Layer’s capacity from 670 kB/s to 10 MB/s on four-core machines.
Batched KZG verification · parallel validation · hardware benchmarks
About
I am a software engineer with a PhD in computer science, currently working on the Tezos protocol at Nomadic Labs. My work has ranged from formally verified railway safety software to blockchain infrastructure and developer tooling.
I enjoy taking technically difficult projects from a sound design through to measured, maintainable production systems.
Selected impact
Alstom · 2023—2024
Verified railway safety software
Developed and formally verified SIL 4 automatic-train-protection software, including proof maintenance through a hardware migration.
Atelier B · EN 50128 · safety-critical systems
Tweag · 2021—2023
Secure contracts and faster builds
Helped establish a smart-contract audit practice, then improved Haskell builds by avoiding needless recompilation in rules_haskell.
Security reviews · symbolic execution · Bazel · Haskell
Experience
2024—present
Senior Software Engineer
Nomadic Labs
Core developer of Tezos, focused on the Data Availability Layer and its post-quantum successor.
2023—2024
Software Designer
Alstom
Formal development and verification of safety-critical onboard railway systems.
2021—2023
Software Engineer
Tweag
Functional-programming consulting, smart-contract security, and open-source build tooling.
2017—2020
PhD Researcher
ENS Paris-Saclay & Mines Paris
Type theory, termination analysis, and interoperability between proof assistants.
Research foundation
My doctoral work, supervised by Frédéric Blanqui and Olivier Hermant, studied termination checking for rewrite-rule systems in the λΠ-calculus modulo theory. The goal was both theoretical and practical: turn sound termination criteria into tools that help dependent-type systems interoperate.
PhD thesis · 2020
Dependently-Typed Termination and Embedding of Extensional Universe-Polymorphic Type Theory using Rewriting
FSCD · 2020
Encoding Agda Programs Using Rewriting
Embedding dependently typed Agda programs into Dedukti through rewriting.
Types · 2020
Universe Polymorphism Expressed as a Rewriting System
A rewriting-based account of universe polymorphism.
FSCD · 2019
Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting
With Frédéric Blanqui and Olivier Hermant: a termination criterion for dependently typed higher-order rewriting, implemented in Dedukti.
HOR · 2019
SizeChangeTool: A Termination Checker for Higher-Order Rewriting with Dependent Types
Presentation of the tool at Higher-Order Rewriting.
Open-source
Tools for type theory
Co-maintainer of Dedukti; developer of SizeChangeTool and, with Jesper Cockx, Agda2Dedukti.
Teaching · 2017—2020
Logic, complexity, databases & programming
Taught logic and complexity at ENS Paris-Saclay, a databases project at ENS Paris-Saclay, and introductory algorithmic and C++ programming at IUT d’Orsay.
Writing & research
Nomadic Labs · 2026
DAL bandwidth increase to 10 MB/s
How batching cryptographic checks and parallel validation enabled a 15× bandwidth increase.
Tweag · 2022
Recompilation avoidance in rules_haskell
Using GHC ABI information to avoid unnecessary work in Bazel builds.
FSCD · 2020
Encoding Agda Programs using Rewriting
Research on translating dependently typed programs into the Dedukti logical framework.
CNRS GT LVP · 2021
Presentation at the Languages & Program Verification working group
A presentation given while at Tweag, for the CNRS Langages et vérification de programmes (LVP) working group.
Focus areas
Distributed systemsCryptographyFormal methodsType theoryRewriting systemsSafety-critical softwareSmart-contract securityOCamlHaskellRustRocq / CoqAgda
Contact
Interested in working together? Contact me on LinkedIn or find me on GitHub.