Verifiably Safe Agentic Compute
summary
Claims that LLMs are just branch predictors and that useful agentic systems need a new compute stack not bigger models. Proposes a programming language that emits a Universalis spec, LLMs generate JSON-backed code plus a machine-checkable proof, and a non-ML verifier such as a Lean verifier checks the proof before running on the Automat runtime. Uses structured outputs to enforce syntax, treats proofs as cheap to check and tool calls as primitives rather than teaching models arithmetic.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 0:10Learning from AI history
- 11:12Asymmetry in verification
- 12:54Neural computers vision
- 16:36Programming for the AI era
- 17:51Extended mind and tools
- 21:01The lethal trifecta
- 21:52Principles of secure AI
- 24:36Proof-carrying code
- 25:14The case for new languages
- 28:13Universalis implementation
- 28:56Hybrid user interfaces
- 29:37Intentional programming
- 29:58Open safety problems
related talks
41mFrom AI Software Engineers to AI Knowledge Workers
40mSafe Coding with LLMs - Verifiable Scala Silver Bullet
53mSemantics-based program manipulation in the age of LLMs
01h 00mAI Safety through Programming?
26mLanguage Model Agents Enable Semi-Formal Programming
01h 00mFrom LLM Theory to Practical Agentic Implementations
22mTowards Verified Code Reasoning by LLMs
38mNobody Pages the LLM: Engineering Rigour for Vibe Coding