Software is undergoing an inversion. For the entire history of the field, the scarce resource was the ability to write code. That constraint is gone. Models now generate code at a pace no company can keep up with. And the pace is only getting faster.
The industry's answer is to point the same models at the problem. LLM-as-judge: have one model grade what another wrote. It is better than nothing, and it will improve. But it carries a structural flaw that scale alone does not repair: the judge and the author were trained on the same distribution, optimized for the same objective, to produce code that looks right. A model trained to write plausible code, asked to review plausible code, is fluent in precisely the failure mode it exists to catch. Its errors are not independent of the author's errors. They are correlated. And correlated errors are the one thing a review process exists to eliminate.
The underlying mistake is treating review as a language task. It is not. Correctness is not a property of syntax; it is a property of logic. Two programs can be textually near-identical and semantically opposite. A reviewer that operates on surface form is grading prose. A reviewer worth trusting has to operate on semantics.
There is a domain where meaning is the only thing left: formal specification. Strip a program of its syntactic sugar and what remains is exactly the object a reviewer must judge: the logic itself. This is not a new idea. Formal methods have been proving programs correct for fifty years, and in that time they earned a reputation: rigorous, expensive, and unable to scale beyond avionics and kernels. A reputation that was well deserved. Every specification had to be written by hand, by rare experts, for one codebase at a time.
But machine learning changes the economics. But only if the ground truth exists. Models learn what their data teaches them, and today the data teaches them to write. There is abundant supervision for generating code and almost none for judging it: real code, labeled for correctness by expert review, paired with the formal specification of what it actually does. That dataset is the missing ingredient — the bridge between the scale of learned models and the rigor of formal logic. Neither side is sufficient alone. Formal methods have the rigor but cannot scale. Learned judges scale but lack the rigor. The data is where they meet.
Someone has to build the ground truth for the age of machine-written code. That is what we are doing.