Yann Régis-Gianas
I study how to build reliable software when agents write most of the code. My work connects first principles, formal methods, and the realities of operating production engineering teams.
I am Head of Core Engineering at Nomadic Labs, where I help lead the engineering of the Tezos protocol and its surrounding infrastructure at Trilitech and Nomadic Labs, since Tezos is an open ecosystem rather than any single company’s product.
Before joining the Tezos ecosystem, I spent fifteen years as an Associate Professor in Computer Science at the University of Paris. I hold a PhD and an Habilitation à Diriger des Recherches (HDR), and worked on functional programming, programming-language semantics, formal methods, and the verification of critical software.
That path, from proving properties of programs to being accountable for systems in production, is the perspective behind this blog. Code agents make producing software cheaper. They do not make intent, validation, or engineering judgment cheap. I write about the disciplines that close that gap, and I try to attach each argument to something readers can inspect, run, or challenge.
The tools the essays run on
These are the instruments the writing describes, all public and all experimental. Use them as they are, or raid them for parts.
- agentic-loop-kit — the spec-driven loop this blog argues for, packaged as Claude Code skills and the templates they expect.
- laconic — a Claude Code plugin that keeps an auditable model of what the engineer already understands, and uses it to decide what to leave out.
- inbrief, forebrief and backbrief — three interfaces for onboarding onto a project, resolving an ambiguity before it is decided by default, and re-aligning your understanding once a change has landed.
- rocqeteer — certified, efficient programs with Rocq and OCaml, with a small explicit trusted base.
Selected work
- Tezos — a self-amending blockchain protocol, developed and upgraded in production.
- Learn-OCaml — a platform used by universities to teach and assess OCaml programming.
- Menhir — an LR(1) parser generator for OCaml, to which I contributed.
- Morbig — a parser for the POSIX shell language, built for the analysis of real-world shell programs.
- FreeSpec — a Coq framework for implementing and certifying impure computations.
You can also find my public code on GitHub and my research record through the publications linked from those projects.
How this blog works
The essays here are living documents. On these topics, an immutable post goes stale fast, so I revise essays for as long as they stay valid. Each essay carries a version number and its own changelog; the Changes page lists every revision across the blog, and its feed carries the major ones, the revisions after which a re-read is worth your time.
Contact
Unless explicitly stated otherwise, the views expressed here are my own and do not represent Nomadic Labs.