1. The rule
The rule fits in four words: models propose, oracles dispose. Everything else I have to say is commentary on where those four words draw the line.
A model may draft, translate, summarize, and search. All of that is welcome in my shop, and none of it is evidence. Between a model's output and the evidence layer, the layer where results live, where claims get cited and built on and trusted without being re-checked, there has to stand an independent check, and the check has to be the kind of thing that can say no. Not a reviewer skimming for tone. Not a second model agreeing, because a second model agreeing is a second proposal. A mechanism the proposer does not control, whose refusal actually stops the claim at the door, and whose refusal is written down when it happens.
The phrasing sits deliberately close to the old proverb, man proposes, God disposes, because the structure is the old structure. The proposer can be brilliant, tireless, and right most of the time, and the disposition still belongs to something else. What changed is not the structure but the economics. Proposals used to be scarce, so treating a confident one as halfway to a finding was survivable. Machines made proposals nearly free, and a discipline calibrated for scarce proposals fails quietly under abundant ones.
An evidence layer is any place downstream work trusts without re-checking. That is what makes it a layer instead of a pile. The moment a generated result lands there on its own authority, every later consumer inherits a claim nobody disposed of, and the inheritance compounds. So the rule holds at the door, structurally, not as a request that everyone be careful.
2. A receipt that re-derives
The place I hold this line hardest right now is a compiler. A program built with it does not just print results; it can emit a receipt, a sealed record of what ran, what came out, and which invariant the run was checked against. The verifier's job is not to read that record and nod. Its job is to re-derive: whatever can be recomputed from the sealed facts gets recomputed and compared, the invariant is checked again, the sealed exit of the run is checked against a re-run. Agreement is a verdict, not a formality. One schema holds this shape across five kinds of computation, from fully deterministic runs and closed-form probability through seeded randomness to sampled estimates and budgeted search, and the sampled cases carry their sample counts inside the seal, because an estimate without its denominator is a mood.
Some facts cannot be re-derived exactly, and the honest move there is not to fake it. Wall-clock time is the plain example: the verifier re-measures, then reports the sealed value and the fresh one side by side without forcing them to agree, because pretending a re-measurement is a re-derivation would be the exact overclaim this whole apparatus exists to refuse. A receipt states what was checked and how, and nothing stronger. The nulls stay honest. It is slower than trust and more annoying than confidence, and that is not the price of the discipline, it is the discipline.
3. A check that can prove it can fail
A check that has never said no is not known to be a check. It might be one. It might be a rubber stamp with good posture. From the outside the two are indistinguishable until the day it matters.
So the negative fixtures are first-class citizens of the suite. For every way a receipt or a chain of receipts could be forged, there is a test that forges it and demands the right refusal by name. Tamper with one sealed count inside a chained bundle and verification has to fail, and fail with the specific name for that tampering, CHAIN_LINK_UNVERIFIED, not a shrug and a generic error. Reorder the members, drop one, substitute one: each sabotage has its own named failure, and each name is exercised end to end in the ordinary test run. The verifier also carries a self-test whose whole job is to demonstrate, on demand, that the rejections still fire.
That sounds paranoid until you notice which way verification systems rot. They rot toward yes. Deadlines, demos, the slow annoyance of false alarms, every pressure on a checking system pushes in the same direction, and nothing pushes back except deliberately maintained proof that no still works. The yes is the pleasant output. The named no is the product.
4. The boundary, crossed live
The language has a capability for calling out to a model over a socket, which makes the boundary concrete enough to enforce in code. The receipt layer refuses outright to emit or verify a scientific receipt over any program that observes a model. Not discouraged: refused, as a named inadmissibility. A model's involvement does not make a run worthless. It makes the run a proposal, and a proposal gets a different document, a boundary receipt, sealed where the bytes crossed, claiming only what it can honestly claim: that this exchange happened, at this boundary, under this seal. What it never claims is that the model was right.
This month I watched the loop close live. A local model proposed a completion over a real socket. The shim on the far side sealed a boundary receipt over the exchange. The verifier accepted the genuine receipt and refused a tampered copy with a seal mismatch. A model-free kernel did the actual scientific judging under an ordinary receipt of its own. Then a chain bound the proposal and the disposition into one tamper-evident bundle, each member independently re-verified, and tampering the model's member broke the chain by name. Proposal and disposition in one evidence bundle, the wall between them intact and tested from both sides.
For honesty's sake: the branch that carries this end to end is in review as I write, not merged. I am describing a demonstration, not a shipped release, and the distance between those two sentences is the subject of this essay.
5. The stance
None of this is suspicion of models. I use them all day, this essay is openly model-assisted, and the compiler would be years further away without them. The rule is about which layer a model's words may land in on their own authority, and the answer is none, and the answer does not soften as the models improve. A better proposer is a better proposer. The disposition still belongs to something it does not control, or the evidence layer stops being one, and everything downstream inherits the difference without being told.
The rule does not exempt its author either, which is where it bites. Elsewhere in the same toolchain a preregistered confirmatory run is under way as I write, and I am not going to tell you how it is going, because no verdict has been computed yet, and the discipline that refuses a model's self-report refuses mine too. When there is a result it will arrive with its receipts, or it will not arrive.
What I am against is quieter than the loud fears. It is disposition migrating to the proposer, one convenience at a time, until the record is a transcript of what the most fluent party said about itself. Every mechanism in this essay is a way of keeping the no alive somewhere the proposer cannot reach it. The four words are just that, compressed. Models propose. Oracles dispose. And somebody who is neither should be able to check both, which is why the receipts are public.
Process note
This essay was drafted with model assistance at my direction and edited and signed by me, as its own rule requires me to disclose. The technical claims describe public work, principally the compiler at github.com/HarperZ9/buildlang; the demonstration in section 4 lives on an in-review branch, as the essay says. Where a sentence reaches past what the record supports, it is argument, and it should read as argument or it is a defect.