当 AI 生成代码超出人工阅读能力，解法是工具而非更强的审查者

Six months before the Miden zkVM audit even started, Trail of Bits had already spent most of the real work. Not staring at code. Building an LSP server, a decompiler, a static analysis engine, and a Lean formal model of the VM executor, from scratch, with AI agents, before opening a single review ticket. Their writeup of that effort is the closest thing I've seen to an honest answer to the question everyone keeps asking: how do you review a growing volume of AI-generated code? The reflex is to reach for a stronger reviewer, a bigger model, a stricter linter. Trail of Bits went the other way. When the code under review is a custom assembly language with no developer tooling and near-zero documentation, no reviewer, human or model, wins by reading. So they raised the floor instead. Why reading was never going to win here The Miden core library is written in Miden assembly (MASM), a stack machine architecture where instruction inputs and outputs are implicit, pulled from the stack. Procedures don't declare signatures. Calling conventions don't exist. While-loops aren't required to be stack neutral, so the loop condition can sit in a different stack slot on every iteration. Branches can have different stack effects per path. Stop and think about what that does to manual review. Reading MASM means holding every stack effect in your head, because the syntax won't tell you. The net stack effect of a call is generally impossible to determine statically, and every analysis failure propagates up the call chain. The ceiling on review quality is how long a reviewer can go without a context switch to look up instruction semantics. That is exactly the collapsed, unverifiable surface where the reimplemented crypto I keep writing about goes to hide. So the agents didn't review. They built the missing tooling instead. The tools the agents built An LSP server and VS Code extension that annotates inline stack effects and instruction docs right in the editor, so a reviewer never leaves the flow to look up semantics. A decompiler for a well-defined subset of MASM, the single largest effort, over a hundred AI-generated commits across multiple months. They deliberately narrowed it to a subset they could decompile correctly, rather than a full pipeline that would silently be wrong. And a Lean model of the VM executor. The Lean path produced 95 machine-checked correctness proofs covering a large component of the Miden core library. That's where the real find came from: an unvalidated prover-supplied input that would let a malicious prover forge Falcon signatures and steal funds from Miden account holders. That is not something a reviewer catches by reading a diff. It is something a formal model catches because it is a machine-checked counterexample generator with no blind spot shaped like a human attention span. The middle result is worth flagging too. The decompiler's main value turned out not to be the decompiled output but its internal analysis frameworks and intermediate representation, which they reused for static analysis. If you pay an agent to build tooling, the intermediate artifacts are often the prize, not the surface output. This is the real answer to "how do we review more AI code" Every "AI code review" pitch frames the problem as read throughput: our model reads your new code faster, so you keep up. Trail of Bits is saying the read is the tail. When code volume outpaces humans, you don't need to read more of it better. You need tooling that makes the surface small enough that whatever reading you do, human or model, is worth it. A reviewer reads a diff and shrugs. A machine-checked model reads a whole VM and points at the one line where a forged signature becomes possible. Those are different categories of verification, and only one of them scales past human attention span. That distinction maps to the wait-vs-read frame I used when I ran at this same question on the aicodereview.io side. The bottleneck in PR review has never been the minutes spent reading a diff; it's the hours the PR sits in queue and the size of the surface you have to trust. Tooling that shrinks the surface attacks the real constraint. A bigger reader model just makes the wrong thing faster. Separating the writer from the judge There's a second angle in the same post worth sitting with. Trail of Bits alternated between Claude for planning and development and Codex for reviewing the decompiler. Every new decompiler feature, agents decompiled a randomized set of core library procedures and diffed the output against the original MASM to hunt regressions, with anything found added as a regression test. That is the correlate of the correlated-judge problem. They did not have the same model that wrote the decompiler also judge the decompiler. Different model, and a ground-truth diff, not an LLM's opinion. That's how you avoid the five-reviewers-one-opinion failure. It also lines up with the deterministic-judge argument: once reviewer outputs become the gate, you want a judge that doesn't change its verdict run to run, and that verdict ideally doesn't come from the model under test at all. This is the part most teams skip. The vendor demo shows the reviewer finding a planted bug, and everyone nods. Nobody asks who verified the reviewer's verdict, or whether the writer and the judge shared a model. The Miden audit treats that as load-bearing, which is why the proofs are machine-checked rather than asserted. What to take from it For a team wrestling with the growing-AI-code question: stop buying review throughput and start buying a lower floor. Formal models, decompilers, static analysis frames, anything that turns "read this whole thing closely" into "read the small set of places where analysis says it could break." Three concrete things to steal from Trail of Bits: Build the reviewer's context, not just a bigger reviewer brain. An LSP server that annotates stack effects cost a few days and changed the reading surface more than any model swap. It can kill the context switch, because the context switch is where review depth dies. Narrow the tool to what it can do correctly. They decompiled a subset they trusted rather than shipping a full, subtly-wrong decompiler. That's the same discipline as only asserting what you can verify. A tool that is correct on a subset beats one that is confident everywhere. Keep the judge independent from the writer. Codex judged Claude's decompiler against a raw MASM diff. No shared cleverness, no self-review. If a score can't be reproduced by a different model against ground truth, it isn't a score. The next time a vendor tells you their reviewer handles AI-generated code at volume, ask what they changed about the floor, not the reader. If the answer is "bigger model reads faster," you're still going to lose. If the answer is "we built the thing that makes the surface small," that's the audit that works. Sources: the Trail of Bits writeup, the Miden VM repo, and Transluce's urlquery agent-activity report.