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.
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.
Experiments
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.
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. Learn about the toolchain we use to implement vericoding on the technology page.
Where vericoding matters
The same idea applies where a wrong answer is irreversible: money movement, exactly-once fulfilment, inventory, and regulatory rules. Those cases are on the solutions 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 what the program does. 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