In a collaboration with Anthropic, we proved security properties in more than 100 open-source libraries at the assembly code level and found bugs that years of testing missed.
A shared, verified software stack, starting with every project in the nixpkgs ecosystem.
lf-lean: The frontier of verified software engineeringlf-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.
Fractional proof decomposition fuses partial evaluation and property-based testing to scale testing compute logarithmically with bug rarity, instead of linearly.