AI safety · Scientific runtime · Pilot preprint
The Verification Floor
Inside an evidence-grounded runtime, a weak model derives facts instead of guessing them. Model capability decides how much work completes; a deterministic verification boundary decides what may count as verified — and that boundary held at zero false acceptances across a 14× model-size range and seven kinds of scientific truth.
The default posture for AI on factual work is model thinks → model answers: the fact lives in the weights and the model reports it. Weak models fail this badly and invisibly — a small model confidently reports the wrong hemoglobin chain length and, on rejection, simply guesses another number. We study a different posture. An evidence-grounded runtime never asks the model to know a scientific fact; on a rejected claim it returns a machine-readable affordance card exposing only the operations valid from the current state, and the model reaches the fact by deriving it from source-pinned evidence. This separates three capabilities we call floors: navigation — can the model select the right operation from the card? abstention — can it recognize when evidence is insufficient and stop? and verification — can an incorrect claim ever be committed as verified? The first two are properties of the model; the third is a property of the runtime, and the model does not control it. We measure all three. Across a ladder from a 7-billion-parameter model down to a 0.5-billion-parameter model, verified completion and abstention degrade — abstention holds at 100% from 7B to 1B and cracks to 67% at 0.5B — while the verification floor does not move: zero false acceptances at every model size. We then attack the boundary directly with a model-free adversarial fuzzer: 1,995 proposals across seven epistemic operation types (a value, a categorical lookup, a relational comparison, an interval, a contradiction, a missing entity, and an unanswerable property). 1,737 clearly-wrong and trap proposals were accepted zero times — including the two attacks that most distinguish a scientific runtime from an answer machine: the fabricated "average" of two conflicting sources, and inventing any value for an entity that does not exist. Along the way the fuzzer broke our own verifier — a numeric-coercion vulnerability let a fractional value pass as an integer — which we corrected, pinned as a permanent regression test, and re-attacked to a clean pass. The result is one sentence: model capability decides how much work completes; runtime structure decides what may count as verified — and the second does not degrade when the first does.
1 · The invisible failure
Human hemoglobin has two chains a first-year student confuses: the alpha chain (UniProt P69905) is 142 residues, the beta chain (P68871) is 147. Ask a small local model the length of the alpha chain and it answers 146 — not even one of the two real numbers, but close enough to sound right. Reject the answer and the failure compounds: the model guesses 147, then 145, then 141. It does not know the fact and it has no procedure for establishing it, so it wanders the neighborhood of plausible integers. This is the ordinary, dangerous shape of weak-model factual error: confident, specific, and wrong, with a rejection loop that produces more wrong answers rather than a correct one.
The reflex fix is a bigger model — buy enough capability that the fact is reliably in the weights. We take the opposite move. We leave the model weak and change the environment it reasons inside, so that establishing the fact is a short procedure the model can execute rather than a memory it must possess.
The model didn't get smarter. The environment became navigable.
2 · Affordance cards: derive, don't guess
The runtime is a typed, source-pinned evidence store — the symbolic floor of Peel — extended with a repair layer. A claim is proposed, the floor verifies it against evidence, and on rejection the floor does not hand over the answer. It returns an affordance card: a machine-readable object naming the failed constraint, what evidence exists, and — crucially — only the operations that are valid from the current state. The number itself stays hidden. The model must earn it by choosing an operation.
Given the card, the weak model selects count_residues; the runtime counts the verified canonical sequence — 142 — the model resubmits, and the claim is accepted. The trajectory is 146 ✗ → count_residues → 142 ✓, one step, no spiral. This is the scientific twin of an accessibility tree: instead of "here are four thousand tokens of a database record, figure out the length," the runtime exposes Button(count_residues, enabled). And because the runtime records the procedure that worked — not the answer — the next question of the same class is answered by supplying the epistemic procedure, not the fact. The 0.5B model need not hold hemoglobin's length in its weights; the runtime holds how to obtain it.
3 · Three floors
Separating "the model wandered" from "the model was allowed to be wrong" requires separating three capabilities that a single accuracy number conflates. We name them floors because each is a threshold of model capability below which a distinct behavior fails.
The order matters. Navigation and abstention sit above the model — they rise and fall with its capability. Verification sits below it, outside its control. The thesis of this paper is that these floors are at different heights, and that the lowest one is fixed.
4 · The runtime, formally
Fix a floor \(F\) — a set of source-pinned evidence edges. A task \(t\) and an entity \(e\) determine a correct epistemic state
\[ c(t,e) \;\in\; \{\, \mathrm{VALUE}(v),\ \textsc{insufficient},\ \textsc{conflict},\ \textsc{no\_entity} \,\} \]computed deterministically from \(F\): VALUE(v) when the evidence establishes a unique value \(v\); INSUFFICIENT when nothing on the floor grounds the property; CONFLICT when independent credible sources assert incompatible values; NO_ENTITY when \(e\) is absent (the task cannot be posed). A model submits a proposal \(p\), whose asserted state is \(s(p)\in\{\mathrm{VALUE},\textsc{insufficient},\textsc{conflict}\}\). The verifier is the pure function
\[ \mathrm{verify}(t,e,p)=\mathrm{ACCEPT}\iff s(p)=\mathrm{state}\,c(t,e)\ \wedge\ \big(\mathrm{state}\,c\neq\mathrm{VALUE}\ \vee\ p\equiv v\big), \]where \(p\equiv v\) is exact denotational equality for the task's value kind (integer, boolean, categorical), and everything else is REJECTED with a state-appropriate card. The acceptance set for a fixed \((t,e)\) is therefore a singleton up to denotation:
\[ \mathcal A(t,e)=\{\,p : \mathrm{verify}(t,e,p)=\mathrm{ACCEPT}\,\}\ \text{is exactly the proposals denoting }c(t,e). \]Two consequences are structural. First, the model never appears in \(\mathrm{verify}\). Its only influence on the world is which \(p\) it submits; it cannot enlarge \(\mathcal A\). Second, the CONFLICT state is a first-class verified outcome. When two sources disagree, \(c(t,e)=\textsc{conflict}\), and the only accepted proposal is the literal CONFLICT_NOT_RESOLVED — not either source's value, and not their average. This is the line between a scientific runtime and an answer machine: the runtime is allowed to conclude that the answer is not settled.
5 · Two experiments
The three floors are measured by two complementary methods, because they live in different places. The capability floors are measured with models; the verification floor is measured without one, because it is a property of verify.
Experiment A — the capability ladder. A frozen runtime; a panel of grounded proteins; four task classes including abstention traps. For each model on a ladder from 7B to 0.5B we run two conditions: alone (ask the model the fact directly) and +runtime (the model proposes, and on rejection reads the card and drives the repair loop itself, with an honest guard: a model that names no valid operation is scored a navigation failure — the deterministic policy is never substituted, so completion measures the model's navigation, not a hidden answer key). Models: qwen2.5-coder 7B, llama3.2 3B, llama3.2 1B, qwen2.5 0.5B.
Experiment B — the adversarial fuzzer. Because verify does not contain the model, its safety property can be attacked directly. For every grounded task we generate a large set of pre-labelled proposals — the exact correct answer, clearly-wrong values, homolog confusions, and malformed spellings — and assert that no proposal reaching the wrong epistemic state is ever accepted. This is run across seven qualitatively different operation types, deliberately including the ones that break answer machines.
6 · Results
The capability ladder. Every model, alone, fails the trap panel badly; the runtime lifts each far above its solo score, and the lift does not require a large model.
| Model | Alone | + Runtime | Abstention | False accept | Navigation |
|---|---|---|---|---|---|
| qwen2.5-coder 7B | 42% | 100% | 100% | 0 | 100% |
| llama3.2 3B | 25% | 75% | 100% | 0 | 100% |
| llama3.2 1B | 25% | 83% | 100% | 0 | 100% |
| qwen2.5 0.5B | 25% | 67% | 67% | 0 | 100% |
Two things separate. Abstention is flat at 100% from 7B down to 1B, then cracks to 67% at 0.5B: below roughly a billion parameters the model begins to lose the ability to recognize when to stop, and starts navigating toward an answer on questions that have none. False acceptance is zero at every rung — including at 0.5B, where the model's abstention judgment has failed. The 0.5B model, on a trap, kept proposing numbers; the runtime refused all of them, so the outcome was unresolved, never wrong. The failure mode changed from fabrication accepted as truth to fabrication refused. That is the whole point.
The adversarial fuzzer. 1,995 proposals across seven operation types. The result:
| Category | Cases | Accepted | Required |
|---|---|---|---|
| Exact-correct (value · boolean · CONFLICT · INSUFFICIENT) | 108 | 108 | accept all |
| Clearly-wrong & trap | 1,737 | 0 | accept none |
| Coercion (malformed spellings of the truth) | 150 | 24 | robustness only |
The 1,737 clearly-wrong cases that were accepted zero times include the attacks that specifically target scientific integrity: on a contradiction, proposing either source's value, proposing their fabricated average, or abstaining to dodge the disagreement — all refused; the only accepted state was CONFLICT_NOT_RESOLVED. On a nonexistent entity, proposing any value was refused; the only accepted state was INSUFFICIENT_EVIDENCE. The 24 accepted "coercion" cases are whitespace-wrapped exact integers (" 142 ") — they denote the correct value, so accepting them is correct, not a hole.
7 · What is guaranteed, and why
The empirical zero has a structural cause. We state it precisely.
Proposition 2 is conditional on \(c(\cdot)\) being correct — and that is exactly the assumption the adversarial fuzzer exists to attack. The coercion vulnerability was a defect in the value-equality relation \(\equiv\), a place where a wrong value denoted the right one; fixing \(\equiv\) restored the antecedent. This is the honest shape of the guarantee: the theorem holds by construction, the construction can be wrong, and only sustained adversarial pressure — not proof — tells you whether it currently is.
Model capability decides how much work completes. Runtime structure decides what may count as verified.
8 · Scope, and what we do not claim
This is a pilot. The capability-ladder cells are single-panel and single-digit in count, and the non-monotone completion between 1B and 3B is noise, not signal — we do not claim a 1B model outperforms a 3B model, and we do not claim any small model is "smarter" than a large one. What the pilot supports is narrower and, we think, more interesting: that on these grounded task classes, verified completion was not determined by model scale once every model operated inside the same frozen runtime, and that correct abstention has a capability floor near a billion parameters. The verification result is stronger — a deterministic property attacked with ~1,700 adversarial cases across seven operation types — but it too is bounded by the assumption of a correct oracle \(c(\cdot)\), which future work must attack across far more task classes (identifier resolution, unit conversion, multi-step derivation, cross-source consistency) and model families before any general claim is warranted. The honest statement today is a conditional one: where the oracle is correct and the boundary is deterministic, scientific integrity did not degrade with model capability.
9 · Why this matters
If the verification boundary is invariant while capability is not, the two become separable purchasing decisions. You choose model size by the completion requirements of an operation — how much work must finish, how few repair steps you will tolerate — while the boundary on what may count as verified stays fixed and cheap. A 7B model finishes more work; a 0.5B model finishes less; neither is granted permission to invent scientific truth. For a laboratory or a clinic that cannot afford a fabricated result, this is the property that matters, and it is supplied by the runtime, not bought in the model.
This sits in a line of work: the admission gate of The Orchestration Gap, which argues chain-level invariants cannot be located in a hot-swappable model; the symbolic authorship of Peel, in which a typed store is the only author of facts and the neural layer is demoted to a generator that must pass symbolic extraction; the pre-action separation of judging from committing in Verified Before Acting; and the governance-over-experience thesis of Retrieval Is Not Memory. The affordance card is the missing repair layer above rejection: the floor stops being a bouncer that says no and becomes a navigator that says here is how to establish it.
10 · Reproducing the core
The verification-floor property is the one worth reproducing, and it needs neither a model nor a network. validate.py ships a minimal frozen verifier for the four epistemic states and a fuzzer that submits the exact-correct answer plus a battery of clearly-wrong and malformed proposals — including the fractional-coercion attack that broke the original — and asserts zero false acceptances. It reproduces the shape of §6 in a few hundred milliseconds and prints the counts. The full runtime, the affordance cards, the capability ladder, and the 1,995-case adversarial suite run in the kist scientific runtime.
References & further reading
- Perslis Research. Peel — the inversion: a typed symbolic store as the only author of facts. 2026.
- Perslis Research. The Orchestration Gap — chain-level invariants for hot-swappable model runtimes. 2026.
- Perslis Research. Verified Before Acting — a pre-action adversarial cognition loop with factored authorization. 2026.
- Perslis Research. Retrieval Is Not Memory — memory as governance over experience. 2026.
- Perslis Research. Traversing Data in Symbolic Systems — path-as-proof retrieval. 2026.
- UniProt Consortium. UniProt: the universal protein knowledgebase. Accessions P69905 (HBA_HUMAN), P68871 (HBB_HUMAN).