From Vibe Coding to Vericoding
summary
Argues for replacing trial‑and‑error coding with AI that writes code plus machine‑checked proofs, reporting a 12,000‑program benchmark and success rates ranging 27% to 82% by language while earlier auto‑verification rose from 68% to 96% on the same test as LLMs improve. Describes tools and projects: Verilab collaboration platform, Lean for proofs, a recent formal proof of gzip correctness, and an open crowdsourced trust workflow that Docker‑reproduces certificates to avoid closed proprietary lock‑in.
AI-written summary · about
chapters (7)
- 0:00The case for vericoding
- 1:12Bugs and the evolution of coding
- 4:10Defining formal verification
- 13:14Building trust through open tools
- 22:29AI safety and the exportable fraction
- 26:48Optimism for narrow tool AI
- 29:47Q&A and closing thoughts
related talks
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems
21mA Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
18mToward Repository-Level Program Verification with Large Language Models
41mTheory of Modern AI: Learning Theoretic, Game Theoretic, and Algorithmic Perspectives
01h 32mCan AI replace programmers?
40mBeyond the Hype: Realistic Expectations of AI
47mCode Is Cheap. Software Isn’t.
34mAI and Code Quality: Building a Synergy with Human Intelligence