A roadmap for massively accelerating software verification
Theorem makes software verification cheap enough to scale. Where we are on the cost–capability frontier, what we verify next, and why each project makes the next one cheaper.
Blog
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.