Trail of Bits describes using Claude and Codex as development and review assistants during a security audit of the Miden zero-knowledge VM. Over six months, the team used agents to build an LSP server, decompiler, static analysis engine, MASM linter, and a Lean model of the VM executor, despite Miden assembly having little existing developer tooling. The resulting tools supported both manual and agent-driven review of Miden’s stack-based custom assembly language. Static analyses identified more than 400 reachable locations where type validation could be improved and found a high-severity flaw in the mod_12289 procedure: a prover-supplied remainder was not validated before use. The researchers said a malicious prover could exploit this to forge Falcon signatures and drain accounts controlled by Falcon key pairs. The team also used Lean to verify binary arithmetic procedures, producing 95 machine-checked correctness proofs. Manual examination of the theorem statements and proofs uncovered two additional subtle bugs, involving 64-bit rotation and 256-bit multiplication. Trail of Bits says agent capabilities made exploratory tooling projects economically practical, and Miden adopted the static analysis engine for future library updates.
