// HACKER NEWS — CYBERSECURITY
Security auditing in the age of (good enough) AI
Security firms have published numerous blog posts describing how they pointed their agent harness at a codebase and found dozens of bugs (we’re one of them). However, these posts tend to focus on agentic code review, which is just one aspect of how we use AI in our security reviews. We want to give a different perspective: before code review even starts, agents now allow us to build custom tooling and formal models that improve the quality and depth of our reviews.
We recently reviewed the Miden VM, a new zero-knowledge VM with its own custom assembly language and almost no developer tooling. To prepare, we spent six months having our agents build an LSP server, a decompiler, a static analysis engine, and a Lean model of the VM executor from scratch. These tools found real security issues, like an unvalidated prover-supplied input that would let a malicious prover forge Falcon signatures and steal funds from Miden account holders. Additionally, the Lean work produced 95 machine-checked correctness proofs, covering a large component of the Miden core library.
In late 2025, the Miden team came to us to have parts of their zero-knowledge VM reviewed before launch. Part of the review was scoped to cover the Miden core library, which contains a small set of cryptographic primitives written in a custom assembly language called Miden assembly (MASM). This made us genuinely excited, as it was right up our alley: a high-assurance project writing complex cryptographic code in a low-level custom assembly language that we had never seen before. At the same time, it also presented some unique challenges.
To start, the Miden VM implements a stack-machine architecture. This means that each instruction operates on values read from the stack, and the result of the instruction is then written back to the top of the stack. While conceptually simple, this makes code written in MASM challenging to review, since instruction inputs and outputs are read from the stack and are always implicit. Additionally, since the Miden VM is a completely new architecture, very little existed in terms of developer tooling like IDE support, Language Server Protocol (LSP) servers, and linters.
We knew that we had six months to prepare for the review, since the implementation was not yet feature complete, so we asked ourselves: “What could we spend our time and tokens on to make sure that the review would root out as many bugs as possible in the codebase?”
Since MASM lacked developer tooling, we started out by asking ourselves what kind of tools we would like to have available when the project started. We typically use VS Code to review code, and syntax highlighting and code navigation are essential for readability and being able to follow data flow throughout a codebase. We needed an LSP server and a corresponding VS Code extension for this, and within a few days we had Claude build a working prototype that provided most of the functionality we wanted: features like syntax highlighting, goto definition, finding code references, and displaying procedure docstrings on hover. With these fundamental features in place, we also decided to add more language-specific features like displaying inline instruction documentation, and stack effects for individual instructions.
Having built the LSP server, we started thinking about other ways to provide high-level semantic information to support manual and agent-driven review. We thought it would be interesting to see if we could provide faithful decompilation for MASM procedures inside the VS Code UI, to help the reviewer quickly understand the high-level control flow and data flow of the procedures they were looking at. For MASM, this is a harder problem than it first appears. Stack machine lifting and decompilation is a well-studied problem, but decompiling hand-written MASM is still difficult for a number of reasons.
Most procedures in the core library do not have declared signatures, which means that the number of input