Verifying AI-Generated Code: Lessons from NASA (Leonid Bugaev)

Coding agents write code faster than anyone can review it. Testing alone won't save you, and code review was never enough. Safety-critical teams at NASA, in automotive and in avionics solved this decades ago: classify risk by consequence, write requirements as contracts, and prove them with evidence like MC/DC. I'll show how we apply the same discipline to agent workflows on real open-source projects, with a live demo.

Outline of the session:

- Voyager, Mars Climate Orbiter, and why "the tests pass" isn't evidence
- Claim, control, evidence, decision: the loop safety-critical teams use
- Classify before you engineer: NASA software classes, ASIL and consequence-based risk
- Requirements as contracts: structured specs and NASA's FRET requirements tool
- Testing as evidence: MC/DC coverage and evidence packs a reviewer can trust

- Live demo: tracing a real Omarchy bug (pressing Enter could uninstall an app) from requirement to a failing reproducer to a verified fix with Proof
- AI governance: making agents follow approved requirements instead of guessing

ABOUT LEONID

Leonid Bugaev is the founder of Proof, a tool that brings high-assurance verification to AI-assisted development. He created GoReplay and spent years building API infrastructure at Tyk API management, used by top financial institutions and governments.

Today he applies NASA, automotive and avionics methods (requirements management, hazard analysis, MC/DC and formal verification) to agent workflows. Proof's public work includes fixes in rsync, gRPC-Go, GraphQL Hive Router and Omarchy.

- LinkedIn: https://www.linkedin.com/in/leonidbugaev
- Twitter: https://x.com/buger
- GitHub: https://github.com/buger
- Proof: https://reqproof.com (demo project: https://portal.reqproof.com/projects/omarchy)