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.
Scidonia FastTrack
Need to speed up services in C/Rust?
FastTrack applies formal refinement to C and Rust bottlenecks. Check feasibility in 20 minutes. If we do not speed up, you pay nothing.
Learn about FastTrack