Vericoding
Vericoding is AI-guided certified program refinement. The artefact you edit is the specification. An AI proposes a faster program, and a theorem prover certifies that the new program refines the old one: the same behaviour, for every valid input.
Films
Vericoding, in six parts
Film 1 of 6
Vericoding Experiments
parsebot
A grammar in Rocq yields a certified JSON parser, extracted to OCaml. A zero-copy refinement of that parser reaches 267.9 MB/s on gsoc-2018.json, still proved equivalent.
SpecAMQP
An open Lean specification of AMQP 1.0: one shared description that implementations can follow and prove they comply with. The reference implementation is growing into a server that is correct by construction.
LeanIn
A concurrency runtime for Lean 4. Async code compiles to a state machine, and the model is machine-checked. On a pipelined HTTP benchmark it reaches 3.05× Node 22.
lexpat
A Lean 4 port of libexpat's XML 1.0 parsing semantics, for untrusted input. A bounded C surface fails closed outside the calls it implements. The UTF-8 decoder is machine-checked.
The shift
From examples to proof
-
A test samples a number of cases.
-
A contract states the rule.
-
A theorem prover checks that rule for every valid state.
The software is specified in Lean, compiled through C to LLVM IR, and proved against that specification. That method is on the technology page.
Where vericoding is important
The same idea applies where a wrong answer is irreversible: a payment, an access decision, or a safety limit. The sectors where that cost is highest are on the sectors page.
Vericoding is how that standard is met. You edit the specification. An AI proposes the program, and a theorem prover certifies that the new program refines it: the same behaviour, for every valid input.
Further reading: AI-guided certified program refinement and from vibecoding to vericoding.
Vericoding Services
Prove the program correct. Then make it faster.
Models now write more code than you can review line by line. You specify what the program must do. We prove the implementation meets that specification, and where latency or compute cost is the problem, we replace it with a faster program that still does.
See the services