Proving file integrity for an xv6 sandbox
We proved that any program inside an xv6 sandbox preserves the original host files, even through crashes. The proof covers compiled machine code under formal semantics for a multicore RISC-V machine.
LLMs are making formal software verification feasible at a much larger scale
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.
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.