Verus proves Rust correct for all inputs. Code review still can't define "correct."

Amazon detailed Verus, a Rust verifier used in Firecracker and AWS Lambda that mechanically proves annotated functions against a mathematical spec for all possible inputs rather than reviewing code. A developer argues this highlights the structural gap in AI code review: unlike query planning, where a 4B model post-trained with agentic reinforcement learning beat Postgres's default plans by 44.7% on join-heavy queries because execution time is a cheap, objective reward, code review lacks a fast verifiable signal. The proposed fix is to shrink the unverifiable part of review by leaning on specs, tests, type safety, and provable checks.

Amazon shipped a blog post on Verus, their Rust verifier used in Firecracker and AWS Lambda. Verus doesn't review your code. It proves it: annotated functions get checked against a mathematical spec for every possible input, mechanically, no model in the loop. Correctness stops being a judgment call and becomes a pass/fail. I keep coming back to that because it's the sharpest version of the gap the AI-review space is stuck in. A reviewer, human or model, is answering "is this diff correct?" There is no verifier for that question. There's a spec verifier, a compiler, a type checker, a test suite, and none of them cover what "correct" means in a real codebase. Interestingly, the RL crowd already knows this. There's a recent experiment where a 4B model was post-trained with agentic reinforcement learning to produce Postgres query plans that beat Postgres's default by 44.7% on join-heavy queries rohanbansal.com/qorl . The model started unable to produce a valid plan for 99 of 113 queries and learned fast. Why? Because the RL reward is verifiable: query execution time is a single clean, measurable axis. The model gets a number back for every rollout and improves against it. Query planning is RL-trainable precisely because the reward is cheap and objective. Code review is not. There is no fast objective number for "did this change introduce a bug" that isn't itself a narrow proxy. And that's the structural reason autonomous review plateaus: you can't reinforce a behavior you can't measure. When the judgement comes from a reviewer hour, RL has nothing clean to optimize. So the answer to "how do we review the growing volume of AI code" isn't a better reviewer model. It's to shrink the unverifiable part of the question: nail specs, real tests, type safety, provable checks, getting more of review into categories a tool can verify rather than judge. Every line you move from "does a human think it's right" to "the tool proved it matches the spec" is a line RL and AI review can actually get better at. Verus is the extreme end of that. The principle is the same at any level: give the reviewer a verifiable target and it stops being vibes. I wrote more about why models shouldn't self-review here, and the grade isn't the point either; the verifiable axis is.