Trail of Bits Used AI Agents to Build Custom Tools That Found a Signature-Forging Bug in Miden zkVM
Security auditing in the age of (good enough) AI
Trail of Bits spent six months using AI agents to build an LSP server, decompiler, static analysis engine, and Lean model for the Miden zkVM's custom assembly language. The tools uncovered over 400 type-validation gaps and a high-severity flaw: an unvalidated prover-supplied remainder in mod_12289 that would let a malicious prover forge Falcon signatures and drain accounts. The Lean work also produced 95 machine-checked correctness proofs and caught two bugs missed by unit tests.
A malicious prover could exploit this to forge Falcon signatures and drain any Miden account controlled by a Falcon key pair.
- Segv77
Good enough AI for security auditing feels like asking for "good enough" brakes. There's just no room for complacency.
- suhacker256
This is a great example of how we can actually be using AI to do things better, not just faster