Automatically Synthesising Programs that We Can Trust
summary
Claims an automated synthesiser called SuSLik generates imperative C-like programs plus machine checkable proofs and that those proofs are verifiable in Coq rather than trusting the synthesiser itself. Implementation is ≈7,000 lines, a real bug appears where generated code violates the spec, and the remedy is post hoc certificate generation by translating synthesis proof trees into verification proofs in separation logic. Evaluated on singly and doubly linked lists and BST delete, Coq checking often takes longer than synthesis and 6 of 15 side conditions needed manual proofs.
AI-written summary · about
chapters (22)
- 0:00Intro
- 1:52Program Synthesis
- 6:27Building Trust
- 8:54Synthetic Separation Logic
- 13:01Syntax
- 15:14Deductive Synthesis
- 16:23The Problem
- 17:14Trust
- 18:54Certification
- 19:56Verification
- 20:55Fundamental discrepancy
- 22:25Finding the right abstraction
- 23:17Interpreting proofs
- 24:47Delaying proofs
- 25:30State of proofs
- 25:59Passing the state explicitly
- 28:23Demo
- 29:13Target Logic
- 30:12SMT Solvers
- 30:46Hammers
- 32:19Summary
- 33:03Questions
related talks
22mTowards Automated Verification of LLM-Synthesized C Programs
41m"Do What I Mean": The History of AI and Program Synthesis
17mNeuro-Symbolic Proof Generation for Scaling Systems Software Verification
22mA Certifying Proof Assistant for Synthetic Mathematics in Lean
01h 00mIntroduction to Coq - Part 1 of 2
15mA benchmark for vericoding: formally verified program synthesis
01h 16mCoding Agents: New opportunities for formal methods?
01h 08mLean: Machine-Checked Mathematics and Verified Programming, Past and Future