Lazy Validation and Self-Healing for Agentic Programs
summary
A typed DSL called Pact DSL treats LLM plans as programs, with generated JSON-schema types, workflows, and access-control policies validated at the point of generation via lazy validation and repaired by a self-healing runtime. Safety properties — preservation and policy monotonicity — are mechanically proved in Lean4. Implementation adds a firewall MCP that checks every tool call; results show nearly threefold lower output token use and about half the wall-clock time versus assertion-based baselines, enabling more reliable long-running agentic workflows.
AI-written summary · about
chapters (9)
- 0:00Lazy validation intro
- 4:06First-class principles
- 9:00Policy hierarchy evolution
- 11:45Schema validation workflows
- 12:43Runtime failure checks
- 16:27GitHub agent integration
- 18:42Summary
- 19:04Lean proof clarification
- 20:07Policy monotonicity firewall
related talks
33mVerifiably Safe Agentic Compute
50mFrom Prompt Hacking to Architectural Determinism: Engineering Reliable GenAI Systems
34mHow can we trust our agents?
20mBuilding Deterministic Infrastructure for Non Deterministic AI Agents
53mSemantics-based program manipulation in the age of LLMs
26mLanguage Model Agents Enable Semi-Formal Programming
30mFrom Constraints to Cognition: A Hybrid Framework for Adaptive, Explainable(…)
22mStop pedaling: First principles for spec-driven agentic development