The Last Human Job Is Owning the Predicate

In 2009, a team of researchers announced something that had been considered essentially out of reach: a formally verified operating-system kernel. seL4 was a microkernel of roughly nine thousand lines of C, and what made it historic was not the code (microkernels were decades old) but the proof. The team had produced a machine-checked mathematical demonstration that the implementation did exactly what its specification said, no more and no less, with no crashes and no undefined behavior anywhere in it. The proof ran to roughly two hundred thousand lines and took years of effort, on the order of twenty person-years against about two for the kernel itself, far more than writing the code. The kernel was the cheap part. The oracle (the precise, checkable statement of what “correct” meant, and the proof that the code met it) was the expensive part, the novel part, and the actual contribution.

Sit with that ratio, because it is this entire series arriving at its destination. The nine thousand lines of kernel were, in the language of these essays, recombination: a microkernel, a known component. What took the years, and what earned the place in history, was defining correctness sharply enough to be mechanically checked and then proving the artifact met the definition. The code was downstream of the definition, and the definition was the work. At every layer, the human job collapses to the same shape (own the irreversible commitments, define the invariants, and adversarially audit the definitions) because everything downstream of a good definition is tokens.

What follows: how each argument in this series was the same argument in disguise, why building the oracle is the genuinely novel work in exactly the domains AI is worst at, and why the fact that there is no Jepsen for prompt injection yet is the most important sentence in the whole set.

The strongest version of “the models will build their own oracles”

The optimistic close deserves its best form, because it is not naive. Models already help build the very predicates this series says are the human’s job. They generate fuzz harnesses that find real bugs. They propose invariants from a codebase. They draft specifications, suggest edge cases, and increasingly critique their own outputs against stated criteria. Extrapolate the curve and the claim writes itself: if defining and checking is where the work went, the models will simply learn to define and check, and the last human job will dissolve like every job before it. Betting against models acquiring a capability has been a losing trade for a decade, and I’m not going to make that bet here.

Concede the capability and watch where it stops. A model can operationalize a definition you give it (turn “grounded” or “safe” or “correct” into machinery) with increasing skill. What it cannot do is choose which definition to be accountable to, because that choice is not a technical act. It is a commitment to a specific, contestable answer to “what does good mean here,” made under adversaries and consequences the model has no stake in and cannot be held responsible for. Deciding that “grounded” means attributable-to-cited-sources rather than true, that “safe” draws its line here and not there, that this invariant matters more than that one when they conflict: those are irreversible, value-laden commitments someone has to own. A model can build the oracle once you’ve decided what the oracle should certify; deciding what it should certify, and standing behind that decision when reality attacks it, is the part that doesn’t delegate.

The convergent role

Every post in this series was the same claim wearing different clothes. Novelty lives in constraints, not components, so the human specifies the constraint. A problem is closable only when someone can state a trusted success predicate, so the human owns the predicate. The harness is the moat as leverage because whoever operationalizes a constraint first delegates everything downstream, so the human operationalizes the constraint. Oversight has to be adversarial because a passive checker launders error, so the human attacks the definition. Attention should follow irreversibility because code is disposable and commitments aren’t, so the human guards the commitments. Ask for attacks, not tests, and generalize each to its class, so the human names the invariant and the class. The ratchet never reaches done, so the human keeps choosing what to attack next.

Read down that list and it collapses to three things, over and over: own the irreversible commitments, define the invariants precisely enough to be checked, and adversarially audit those definitions. That is the job. Not the implementation, which is tokens; not the recombination, which is tokens; not even most of the hard-but-reversible problem-solving, which is now tokens too. The residue that does not reduce to tokens is the ownership of definitions, and it turns out to be the same residue at every layer of the stack, which is why it is the last human job, and why it is a job and not a task.

Building the oracle is the research

There is a place this stops being philosophy and becomes a business, and it is the open, adversarial domains: the ones from the second post that never close. In a closable domain, the oracle often already exists: mathematics has the proof checker, sorting has the correctness predicate, and the human’s job is mostly to point the loop at the predicate that’s already there. In an open, adversarial domain, the oracle does not exist, and building it is not a step you take after solving the problem. It is the problem.

Jepsen is the cleanest proof of this. Kyle Kingsbury’s durable contribution to distributed systems was not a database and not a clever fix; it was the oracle: a way to turn “is this system actually consistent under failure” into a verdict you could trust and repeat. Once the oracle existed, everything downstream got easier, and the field reorganized around being able to be checked. The oracle was the research. Now ask the obvious next question: where is the Jepsen for prompt injection? For agent safety? For “did this autonomous system just do something catastrophic on my behalf”? It does not exist. There is no trusted, repeatable verdict for those properties, which is exactly why they stay open and exactly why models cannot simply finish them; you cannot climb a predicate that hasn’t been built. Whoever builds those oracles will not be doing security work downstream of a solved problem. They will be doing the defining work, and the defining work is the whole of it.

What this requires architecturally

This is the bet AOCyber is built on, stated in its own terms: systems, not models; capability commoditizes, and trust infrastructure compounds, because the scarce, durable thing is the ability to turn an open constraint into a checkable one faster than anyone else. You can see the shape of it across the product line. DevFlow is the discipline of owning the spec and delegating the tokens, turned into a development harness. The governance layer inside AOCore is an independent oracle in the request path, checking what the model must not be allowed to do rather than trusting the model to check itself. And the direction the whole platform points (toward answers that arrive with a verifiable receipt rather than a confident assertion) is a wager that in a world where generating output is free, the ability to certify output is the thing worth owning.

It is worth being precise about what such an oracle can and can’t promise, because the honesty is the point. You can build a deterministic oracle for a closable slice of an open problem (for “is this answer attributable to the sources it cites,” which is checkable) even though you cannot build one for “is this answer true,” which is not. That narrowing is itself the human move: choosing a predicate sharp enough to be mechanically verified, and being clear-eyed that grounding is not truth. The oracle you can actually build is the one you defined narrowly enough to stand behind. Choosing that definition well is the work no model does for you.

The last human job

So here is where the series lands. The production is leaving: the code, the drafts, the models, the recombination, all of it flowing to tokens faster every quarter, and that is fine, because it was never the scarce part. What remains, at every layer and in every domain, is owning the definition: committing to what “correct” and “safe” and “good” mean here, precisely enough that a machine can check it and an adversary can attack it, and then standing behind that commitment when the adversary does. It is uncomfortable work, because it is exposed (a definition you own is a definition you can be wrong about in public) and it does not feel like the engineering most of us were trained to value. But it is the part that doesn’t reduce, and it is about to be most of the job.

Everything downstream of a good definition is tokens. The definition is the constraint. And the constraint is the work.