Vero's two task modes: proof-only and code-and-proof, both requiring full coverage

dawnsongtweets · x · 2026-08-23

Vero defines two task modes: proof-only (prove every spec against the provided reference implementation) and code-and-proof (implement every API, then prove every spec against your own code). Both require full coverage—any unproven spec leaves room for exactly the bug it would have caught. Code-and-proof couples implementation choices with proof obligations for end-to-end evaluation of repository-scale verified code generation.

Related event: Dawn Song's Team Releases Vero, First Repo-Level Formal Verification Benchmark(8 posts)→

Original post →

More from Research

Research channel →