Mostly Automated Proof Repair for Verified Libraries

on YouTube ↗19m

" summary

Tool Sisyphus takes an old Coq-verified OCaml function, a changed OCaml implementation, and emits a mostly-automated Coq proof by combining dynamic program alignment, enumerative invariant synthesis, and a novel proof-driven testing technique that extracts executable tests from Coq proof terms. Evaluation repairs proofs for 10 OCaml programs from real libraries, completes most fixes in under minutes, and leaves only a small number of easy, user-proof obligations; the approach reliably suggests correct invariants and produces working Coq proofs.

AI-written summary · about

" chapters (12)

1. 0:00Introduction
2. 0:23Speaker intro
3. 1:05Verified sequence to array
4. 3:14Program verification
5. 5:00Proof maintenance pain
6. 6:24Cus tool intro
7. 8:46Generating invariants
8. 10:17Proof-driven testing
9. 12:42Cus workflow
10. 13:23Evaluating Cus
11. 14:47Key takeaways
12. 15:28Q&A