Return of the Theorem
summary
Claims that AI agents must be treated guilty until proven safe and that every proposed action is deferred until a verifier proves it fits formal business rules. Uses Horn clause logic (Universalis-style guarded clauses), SMT solver (Z3) and classic taint-analysis to check agent-generated plans as set-inclusion against formalized rules. Demonstrates prevention of $1 car sales, unauthorized purchases, keylogger exfiltration and data leaks by rejecting plans without proofs; architecture auto-formalizes requests, has the model produce a program plus proof, and only executes verified plans.
AI-written summary · about
chapters (8)
- 0:00Speaker Introduction
- 1:18Coding Is a Solved Problem
- 3:06Real-World AI Agent Failures
- 6:13Guilty Until Proven Safe
- 8:54Defer, Verify, Then Execute
- 10:37Formal Specs and SMT Solvers
- 16:45The Verification Architecture
- 19:22Why Not Lean or Python?
