Security auditing in the age of (good enough) AI

A security audit team used AI agents not merely for agentic code review but to build a full suite of custom tooling and formal models before touching the code. Faced with the Miden zero-knowledge VM’s custom stack-machine assembly (MASM) and virtually no developer tooling, the team spent six months having LLMs (notably Claude and Codex) generate an LSP server/VS Code extension, a decompiler with a reusable intermediate representation, a static-analysis/abstract-interpretation engine, and command-line tooling. Decompilation targeted a well-defined MASM subset because implicit stack inputs/outputs, lack of calling conventions, and varying stack effects make full automatic lifting unreliable; the decompiler’s IR, produced across 100+ AI-generated commits, became the foundation for data-flow and type analyses.

Those tools found over 400 locations requiring stronger type validation and a single high-severity vulnerability: an underconstrained prover-supplied remainder in mod_12289 that lets a malicious prover craft values to subvert arithmetic checks and forge Falcon signatures to drain accounts. Parallel work translated MASM to Lean and yielded 95 machine-checked correctness proofs covering core binary arithmetic; that formalization also exposed two subtle bugs missed by unit tests (a 64-bit rotate-right edge case and an issue in a 256-bit component). The effort shows that AI-driven tooling plus formal proofs both uncovers real vulnerabilities and raises assurance where conventional reviews struggle.