Trail of Bits built custom AI tooling to audit Miden zkVM before reviewing a single line

Security firm Trail of Bits spent six months before the Miden zkVM audit building an LSP server, decompiler, static analysis engine, and a Lean formal model — all using AI agents — rather than relying on human reviewers alone. The challenge stemmed from Miden assembly's stack-based architecture, which has no function signatures or calling conventions, making manual code review extremely difficult to scale. Using the Lean formal model, the team generated 95 machine-checked correctness proofs and uncovered a critical vulnerability: an unvalidated prover-supplied input that could allow a malicious actor to forge Falcon signatures and steal user funds. Trail of Bits argues that as AI-generated code volumes grow, the solution is not faster or stronger reviewers but better tooling that reduces the reviewable surface area. The firm also noted that the decompiler's intermediate analysis frameworks proved more valuable than its final output, suggesting that tooling artifacts built during audits can have broad reuse value.