Stop pedaling: First principles for spec-driven agentic development
summary
Claims that agentic tooling speeds development while preserving trust by pairing fast nondeterministic agents with a deterministic harness: built a verifier for Michelson in 5 hours that emits machine-checked certificates (Rock proof assistant), and Nomadic Labs runs four experiments including verified models for the layer‑one token module and liquid‑staking design. The harness enforces specification and knowledge, architecture and code quality, tests proofs static analysis and recommends indexed Markdown in Git for reliable agent input.
AI-written summary · about
chapters (16)
- 0:00Introduction
- 0:45Beyond incremental AI agents
- 2:32First principles for cost structure
- 3:40Agents as assembly line
- 5:28Speed without structure danger
- 6:55Reliable output with harnesses
- 9:43Agent context architecture
- 10:47Feedback loops and validation
- 11:28Michelson verifier example
- 13:55Refining specs with interaction
- 15:23Deterministic validation pipelines
- 15:43Formal methods costs in Tezos
- 18:08Tezos formal methods investment
- 19:34Formal methods advantage
- 20:18Conclusion
- 20:39Q&A
related talks
21mDesigning in the age of the 10x engineer
23mStop Making LLMs Deterministic: A Spec-Driven Software Factory
42mRestoring Trust in AI-Native Development
29mBuilding Trust in AI Agents
20mDark Factories: Verification-First Agentic Engineering
01h 16mCoding Agents: New opportunities for formal methods?
50mSpec-driven Development using Coding Agents
01h 04mSpec-Driven Development: Agentic Coding at FAANG Scale and Quality