Most security teams use AI agents merely to scan source code for obvious bugs, but this approach barely scratches the surface of what autonomous systems can deliver. During a recent audit of the Miden zero-knowledge virtual machine, Trail of Bits used agents to generate complete developer tooling from scratch, including a custom language server protocol implementation, a decompiler, a static analysis engine, and a formal Lean specification.
The Miden architecture executes low-level assembly for complex cryptographic primitives with almost no pre-existing tooling. Instead of manually inspecting undocumented assembly, the team directed agents to synthesize the toolchain and model the virtual machine executor formally. This automated setup generated ninety-five machine-checked correctness proofs and uncovered a critical vulnerability where an unvalidated input allowed malicious provers to forge Falcon signatures.
Building the infrastructure to audit a system yields far higher leverage than asking a language model to spot bugs directly. When agents construct the compilers, analyzers, and formal proofs around a target runtime, human auditors gain mathematical verification and deep visibility that manual review cannot match.








