Approach
We ship intelligence you can check.
Not a benchmark to trust — a result you can re-run. Everything we build is graded by an objective oracle, not another model’s opinion.
What we deliver
Systems where a verifier — not a model’s say-so — decides what ships.
PNRD#1 proves the principle on mathematics: an open model lifted to 47% on miniF2F, every proof checked by the Lean kernel. We build the same verifier-decidesmechanism into everything else — including multi-agent generation, where conflicts are resolved against ground truth (does the code actually support the claim?) rather than by an arbiter model’s opinion. One thread: replace judgment with verification.
A receipt, not a brag: when we wrapped a cheapmodel in a dense spec to test “cheap → frontier,” the spec alone shipped a blank, brokenresult. What made it work was the verification loop catching it and repairing against the real error — for about a cent. The verifier was the value, not the prompt. We publish the partial result too.
Checked, not claimed.
Most AI results ask you to trust a number. Ours hand you the receipt. When the gate is a mechanical check rather than a model's opinion, correctness stops being a promise and becomes something you can re-run.
A harness is only as good as its oracle.
With a sound oracle, test-time compute buys large, trustworthy gains. With a weak or absent one, the very same machinery is neutral — or worse. We measured both, and we publish both.
Lean kernel · miniF2F
24.6% → 47.1% (+22.5 pts)
self-graded / hidden tests
≈ 0 — neutral to negative
Blocked beats faked.
An honest “it didn’t pass” is worth more than a confident wrong answer. We report KILL verdicts next to the wins, because a lab that only shows you its hits isn’t showing you anything.
The boundary
The law has two clauses — and the second is where we lose.
“A harness is only as good as its oracle” isn’t a slogan. Tightened, it’s a law with two clauses — and the honest half is the second one.
Our wrapper is a selector: it surfaces the best answer a cheap model already sampled. That is worth a lot in the right place and worth nothing in the wrong one. Here is the line, drawn both ways — because a lab that only shows you the side it wins on isn’t drawing a line, it’s selling one.
Work an external oracle can grade against the true objective:
- Formal proofs — checked by a theorem-prover kernel. On miniF2F-test (244 problems), open gpt-oss-120b went 24.6% → 47.1%, every proof verified by the Lean 4 kernel, false-positive rate exactly zero.
- Spec-bound code — graded by a compiler, a type-checker, or a held-out test suite that actually runs the answer. In our wrapper test the loop — not the prompt — was load-bearing: it caught a blank, broken render a dense spec alone had shipped and repaired it for ~1¢. (That test reached parity with a plain one-shot — competent, not frontier; see the receipt below.)
- Constraint-satisfying output — structured results a schema or constraint validator can accept or reject mechanically.
Work no sound oracle can grade — here the frontier model’s edge is irreducible:
- Open-ended, creative, strategic, taste work — the only available grader is an LLM judging another LLM, which is structurally unreliable: over 50% error on JudgeBiasBench, plus self-preference, verbosity, and position bias. You’re stuck at the cheap model’s average sample, and the frontier model’s average is simply better.
- Tasks the answer is never sampled for — if the correct answer isn’t in the cheap model’s N draws, no oracle can select it. A selector can’t author what the model never produced. That coverage gap is exactly the frontier model’s edge, and prompting cannot manufacture it.
Two gates, and both must open at once. One: a sound, out-of-model oracle — a compiler, a held-out test suite, a prover kernel, a type-checker, a schema validator — that checks the true objective, never an LLM-judge and never a proxy. Two: plausible coverage — the right answer sits within the cheap model’s sample support at feasible N, with real headroom, not a saturated benchmark. Best-of-N is upper-bounded by pass@k: it picks the best answer the model already sampled; it never adds one. Elicitation surfaces latent capability — it does not create it. Drop either gate and you fall back to the cheap model’s average, which the frontier model beats.
Receipt, both sides: the miniF2F lift above is real and re-runnable. A separate internal head-to-head (n = 40 slice, not a third-party benchmark — treat a few points as noise) had gpt-oss + harness top the open field at 42.5% at low cost. And when we held the cheap model fixed to isolate the wrapper, the spec alonelanded at parity with a plain one-shot — competent, not frontier. The load-bearing part was the verification loop, not the prompt. We have not shown cheap == frontier in general, and we’re not going to imply it.