GoKawiilTrail of Bits used AI to build custom tools before auditing Miden zkVM
Trail of Bits reports that ahead of auditing the Miden zero-knowledge VM, its team spent six months using AI agents to build an LSP server, decompiler, static analysis engine, and a Lean formal model of the VM executor from scratch, since almost no developer tooling existed for Miden's custom assembly language. The resulting tools and formal proofs helped uncover a security flaw allowing a malicious prover to forge Falcon signatures and steal funds from Miden account holders, plus 95 machine-checked correctness proofs covering much of the Miden core library.