Discussion
summary
Discussion argues that automated proof generation from LLMs and tools like CoPilot has a roughly 40% chance of working for real verification workflows, but raises concrete failure modes: spec bugs, verifier kernel bugs, and exploitability when proof search is brute forced. Attendees compare Daphne, Daikon, gradual verification and property-based testing as interoperable ways to handle partial specifications, and give concrete engineering wins — Rust-style error messages and IDE Intellisense — as the practical levers that increase adoption.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:03Planning discussion topics
- 8:58AI proofs and verifier soundness
- 17:11Partial vs complete specs
- 23:30Specs in education and industry
- 31:56Type systems and error messages
- 42:14Specification language design
- 50:55Cost-benefit of writing specs
- 57:38Testing spec completeness
- 1:00:11Closing remarks
related talks
53mSemantics-based program manipulation in the age of LLMs
21mA Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
01h 17mProof-Carrying Code For the Age of AI: Machine-Checked Guarantees from(…)
32mCan We Trust AI-Generated Code?
22mTowards Verified Code Reasoning by LLMs
23mBeyond Tests: What to Verify in AI-Generated Code
01h 03mImproved Assistance for Interactive Proof
23mBeyond Tests What to Verify in AI Generated Code