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.
More from Research
- False Collatz Proof via a Lean Bug: Talk Probes Proof Assistants as LLM-Found Bug Targets — marc_lelarge · 2026-10-16
- Goodfire's Nick Cammarata argues neural networks are 'already clean' in new interpretability essay — ctjlewis · 2026-10-16
- NEJM AI: prompt tuning cuts LLM clinical test-order cost ratio to 1.4x across 19 systems — dvir_a · 2026-10-16
- AI Recommends 3.2x Costlier Care; Models Add Tests in 2/3 of Visits Physicians Ordered None — dvir_a · 2026-10-16
- Prompting cuts LLM over-testing costs across 19 systems, but diagnosis agreement drops — dvir_a · 2026-10-16
- 24 AI Systems Recommend $314 Per Visit in Care vs Physicians' $97, a 3.2x Gap — dvir_a · 2026-10-16