Bugs
We use formal methods to find bugs in open-source software. Explore the findings and public reports.
QuickProof
Write specifications for C code as small C programs. AI agents write the proofs, and Rocq (formerly Coq) checks them.
QuickMaths
Our harness for mathematical proofs in Lean. We used it to reach #1 on lean-eval in 20 days.