Bootstrapping the Verified Software Stack
A shared, verified software stack, starting with every project in the nixpkgs ecosystem.
lf-lean: The frontier of verified software engineering
lf-lean is a verified translation from Rocq to Lean of all 1,276 statements in Logical Foundations, done by frontier AI 350× faster than humans.
Catching bugs with fractional proofs
Fractional proof decomposition fuses partial evaluation and property-based testing to scale testing compute logarithmically with bug rarity, instead of linearly.