February 5, 2026

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.

October 7, 2025One-pager

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.