Combining Agentic AI and Lightweight Formal Methods To Find Bugs in a Production(…)
summary
Combines the executable-spec framework for Android pKVM with an OpenAI Codex-based agent that writes ambient-C ghost code and tests, running for about one month on a single ChatGPT Pro account and one human. Agent generates roughly 1,700 lines of ghost code and test harness porting, triages discrepancies, and surfaces logical ownership violations; it finds four previously unknown and substantial bugs (plus two others), all confirmed and fixed by Google.
AI-written summary · about
chapters (8)
- 0:00Agentic AI and formal methods
- 1:07Executable specs in C
- 3:57Verifying Android PKVM hypervisor
- 6:25AI agent writes specs
- 9:15Autonomous testing and bug discovery
- 13:18Memory isolation bug
- 15:04Why specs matter
- 16:30Conclusion and future
related talks
48mHow to Verify AI-Generated Code with Codex
38mOne Android Dev, Ten AI Teammates: Scaling Delivery With Claude Code
34mMulti-coding agent workflows
19mKeynote: Towards Building Safe and Secure Agentic AI
09mMulti-agent collaboration in practice: make AI code an app for you
35mBeyond the Hype and Hyperbole
15mClearAgent: Agentic Binary Analysis for Effective Vulnerability Detection
35mShip - Hype: Rolling Out AI at Scale to 60 Android Engineers