Benchmark dossier
A score says whether the system got the answer. We also publish whether labels were used during development, which part required probabilistic inference, what became deterministic, whether the verifier can reject, whether the authority itself can be wrong, whether results reproduce — and what remains unresolved.
Last checked October 6, 2026 (UTC)
617/816 across Tax, NBA, and Airline. Answers stayed sealed until one scoring pass.
All 97 tasks x 4 trials, v1.0.1 grading, $0.0164 agent-side per trajectory.
Of 2,705, across 40/43 repositories. Zero false acceptances. 33 metered model calls.
Our verifier found tau2 answer-key errors; maintainers shipped the fixes in v1.0.1.
An independent third party accepted, fixed, merged, or reproduced the specific result.
The artifact or submission is public and checkable, but no external verdict or merge exists yet.
Inputs, harness, outputs, and hashes are frozen and reproducible; no independent external verdict.
A measured research result with meaningful evidence, not yet frozen to publication grade.
Derived from measured anchors plus stated assumptions. Never an observed measurement.
Zero-label rule reasoning · RuleArena
Public · pendingRule text went in; the answers, reference code, and scorer stayed sealed. Two independently built deterministic solvers were developed without gold labels, frozen and hashed, then scored once against 816 official problems.
Official answers, the reference implementation, and the scorer were sealed before development began.
Two solver implementations were built independently from the rule text alone — no gold answers.
Everything that decides an answer is deterministic: extraction code, compiled rule oracles, and the Validity gate.
Answer files were hashed and frozen, then the labels were opened once for a single scoring pass.
The system had to earn the right to answer before it could see whether the answer was correct.
Policy-as-Logic (IBM Research)
Closest published full-set symbolic comparator located. It parses each query with a frontier model at runtime; ByteVerity's solvers are deterministic and were built without labels.
Benchmark forensics
The airline rule text never states which listed bag counts as which numbered fee slot. 93 of 300 official problems change answer when the bag listing order is permuted.
74 of our 91 original airline misses were exactly +$70, +$140, or +$210 — the bag-fee quantum. Both independently built solvers read the order literally, and the run disclosed the unresolved interpretation instead of inventing one.
The reference implementation sorts bags fee-minimisingly before numbering them; the IBM comparator adds an explicit lowest-cost assignment directive. Neither policy appears in the rule text. We filed the gap as RuleArena issue #5.
Post-hoc · not the clean score
Adopting a declared customer-favourable assignment policy scores 0.943 on the original set — post-hoc, chosen after error review, and never quoted as the clean result.
Prospective · the clean score
The same fixed policy was then evaluated once on 300 fresh problems regenerated byte-identically from published seeds: 0.903 prospective (0.760 under the literal reading).
The interesting result was not improving the score. It was locating an exact missing semantic authority, stating it explicitly, and testing the resolution prospectively.
Boundaries
Agents + counter-authority · tau2-bench
Public · pendingTwo customer-service agent domains, run full-population on the canonical harness with a deterministic controller doing most of the work. Both rows are open public PRs: submitted, not merged.
All 50 base tasks × 4 trials, canonical unpatched harness
ByteVerity submitted
pass^1 · pass^4 70.00
agent-side per task
cerebras/gpt-oss-120b under the Validity controller
Best accepted standard
Claude Opus 4.5
official cost
Same model without the controller: 64.67 pass^1 (+23.8 points from the deterministic layer).
All 97 base tasks × 4 trials (388 sims, 0 infra failures), v1.0.1 grading
ByteVerity submitted
pass^1 · pass^4 77.32
agent-side per trajectory
fireworks/deepseek-v4-flash + a 3,672-clause compiled policy store
Best accepted standard
Qwen 3.8 Max
official cost
Dual profile disclosed: with a gpt-5.2-low user simulator the same system scores 77.58. Both runs are frozen and offered in the submission.
Deterministic work retirement
In the submitted banking artifact, 66.3% of assistant turns are zero-cost deterministic controller messages. The artifact is hash-chained to a public release and the cost ledger recomputes to all digits.
Measured in this one frozen banking family; airline was not separately measured, and the fraction is not claimed to grow automatically with usage.
Counter-authority
Externally validatedDeterministic decomposition of failing banking tasks surfaced five ground-truth defects, filed as issues #370–374. Four were fixed in tau2-bench v1.0.1, whose changelog references the issues; one remains open. Re-grading moved every model's banking score, by up to ~9 points.
This externally validates the benchmark-auditing capability — not, by itself, the ByteVerity leaderboard numbers above.
Accepted upstream rows used for comparison · recomputed from the public submission files, October 6, 2026
Boundaries
Formal proof · Vero
Public · pendingUC Berkeley's Vero benchmark asks for kernel-checked Lean 4 proofs of repository-level specifications. ByteVerity's compiled-proof-guidance campaign closed 2,490 of 2,705 specs across 40 of 43 repositories — graded by the untouched upstream grader and the Lean kernel, with zero false acceptances and a per-call SHA-256 ledger of 33 metered proposer calls totaling $0.71.
Intelligence concentrated at the residual, not the whole proof problem.
In the staged pilot, 10 of 11 proof obligations closed with zero model calls; the one terminal residual consumed a single bounded proposal.
93.0% of the 1,319 specs newly closed in the campaign landed in repositories that never consumed a metered proposer call.
The final +94 proof-mode specs (Oct 1 → Oct 2) closed with the metered model-call ledger unchanged.
Formal counter-evidence, filed
We also filed formal counter-evidence against the benchmark itself: a kernel-checked disproof of one reference specification (axioms: [propext]) and defect reports on three repositories (issues #3/#4/#5/#7), including a reference implementation that depends on sorryAx — 119 specs we therefore held rather than claimed.
The benchmark author's reproduction of an earlier bundle (35/37 proof-mode, 5/6 codeproof repositories) is recorded in our submission records; it is not externally confirmed.
Boundaries
The work column
A score tells you whether the system got the answer. We also measure how much expensive work had to be repeated to get it — and the unit differs by experiment: model dollars, model calls, FFT forwards, CPU transactions. The larger quantity is work retired, not merely money saved.
Agent benchmarks
66.3% of banking assistant turns ran with no model call.
Vero proofs
33 metered proposer calls across 2,490 kernel-checked closures.
LITHO
80.87% of recurring aerial computation retired after qualification.
IRU / F2
An 11.65× warm full-consumer transaction against exact CPU recomputation.
Verified work amortization
Can expensive qualified work become an asset whose recurring execution is cheaper than fresh recomputation? These are non-LLM controls for the same architecture: acquisition is expensive, qualification is strict, and reuse is only counted while the qualification holds.
LITHO · computational lithography (non-LLM)
Frozen localA computational-lithography aerial-image basis was rebuilt, qualified against eight fresh direct checks, then served 128 distinct same-family inputs. Acquisition cost 1.81 s; each reuse ran 10.2 ms against a 53.1 ms fair direct baseline that retains its own optical setup.
high first-contact cost → break-even at 33 → lower recurring work
Maximum aerial error 7.749e-7 against a frozen 2e-6 gate.
The stale artifact counted as zero.
The originally admitted basis failed requalification in the audit's numerical environment — 8/8 qualification checks and all 128 diagnostic comparisons out of band — so it was quarantined and counted as zero valid reuse. No tolerance was relaxed. Fast stale knowledge does not count.
IRU · real FPGA (AWS F2)
Frozen localReal AWS F2 FPGA execution against an exact CPU recomputation of the same frozen workload. One use is two complete evaluations (864 pairs, 4,320 fields); every output field matched the CPU/golden reference exactly — 8,674,560 fields per path.
R0 ≠ R1
R0 = re-serving the same immutable input. R1 = new inputs from the same family. Only R0 is demonstrated on hardware; LITHO is the R1 result. The distinction is kept because collapsing it would overstate the economics.
Exhaustive authority · PSD2 SCA
Frozen localThe PSD2 strong-customer-authentication exemption logic (EU 2018/389 RTS) compiled into a sealed decision oracle: a ~640-billion-point raw input space partitioned into 15,808 reachable equivalence cells — every cell pinned, fail-closed to sca_required, offline-verifiable, zero LLM at runtime.
We do not sample the policy space. We partition it into equivalence classes and prove every class — so the question becomes which cell a transaction falls in, never whether the logic was tested there.
Supporting evidence
These do not add new headline claims; each demonstrates one property of the same architecture — public registration, blind-test discipline, honest abstention, or decomposition of what a score actually contains.
82.11 and 81.46 overall — rows #3 and #5 as submitted
Two providers registered upstream via an open PR; a 4,297-file signed evidence bundle reproduces both scores exactly, and with the private engine removed the published 14,083-cell decision tables yield identical output on all 2,078 pages.
Open PR — positions are as-submitted, not merged; maintainers run it with their own API key.
151/188 (80.3%) on the solution-blind subset
A deterministic, model-free-at-runtime patch pipeline scored by the pinned official harness, with a 13/13 local Docker spot reproduction and a public evidence repo.
The 570/731 (77.98%) aggregate includes 349 instances derived from public solution history and is self-marked not leaderboard-eligible; it is never quoted without this decomposition.
70 Lean specs proved about PyJWT's JWS/JWT verification logic — no security defect found
A Lean 4 model of the verify path at a pinned PyJWT commit, proved with no added axioms — including four negative security invariants (no alg=none acceptance, no claim trusted before signature check, no public key accepted as an HMAC secret, no rejected key reaching verification) — and tied to the shipped library by five fault-injection-tested differential harnesses, including PyJWT's own 456-test suite as an oracle, with zero surviving mutants.
The proofs are about a model, not the Python code; the certificate is self-declared PARTIAL (36 of 79 RFC obligations carried by proofs, 43 declared out of scope); HMAC/verification direction only; four low-severity RFC deviations recorded; not reviewed by the PyJWT maintainers.
9/41 categories certified at IoU-precision 0.928, 0 false positives on absent clauses
Blind-test discipline: the receipt names the 32 uncertified categories as unproven residual, and one category was removed when it failed blind (0.918 train → 0.727 blind).
Build-time model proposer; the blind test is the arbiter. Coverage 0.529 — precision is the claim, not breadth.
0.7856 forced-label accuracy on a 900-row pre-registered blind set
In abstaining product mode on the same rows, raw accuracy drops to 0.6922 while unsafe NotMentioned→Entail/Contradict errors fall from 44 to 6. In selective certification over 3,000 blind pairs, the product certifies 23.0% of rows clean at 96.1% gold agreement (3 unsafe). The safety trade is measured, not asserted.
Local evaluation over the public dataset (seeds, predictions, and aggregate retained); forced-label mode is a benchmark-max labeler, not the certified product mode. Not a leaderboard submission.
7/38 full passes (18.4%) on the staged board — the best frontier model managed 8.6%
Every banked pass is freeze-verified and reproduced under the task's own official grader; the final evidence pack adds 17/39 task-native passes with 11 exact-1.0 scores. The winning lineage ends in compiled finite decisions that execute with zero model calls. An earlier abstention-first sweep answered only what it could prove: 3 confirmed / 162 abstained at precision 1.00.
Local reproduction, not an official leaderboard: the pack is self-marked not leaderboard-eligible with no canonical runs; some task inputs are constructed fixtures; the frontier comparison is our own measurement on the same board; one earlier 70.2% math figure was invalidated (a frontier model was load-bearing) and is not used.
27 of 27 certified clauses correct, zero hallucinated certifications
No gold labels existed: fresh filings, oracle certification, honest abstentions, verified by inspection.
Small n — stated as 27 of 27, never as a percentage.
What did not work
tau2 Retail
The controller added zero lift over a competent baseline (0.812 = 0.812 on 114 tasks). Published as-is.
SWE-bench Verified
24 tasks attempted, zero accepted patches — and zero false PATCH_READY claims. The gate refused to lie.
Vero deterministic lane
A more-deterministic v2 engine lane regressed from 40/43 to 5/43 repositories. Both numbers are retained; compiled-knowledge lanes are not monotone.
LITHO retained artifact
The original qualified basis failed requalification in a new numerical environment and was counted as zero valid reuse.
Mutation adequacy
The verifier-qualification methodology itself has a measured limit: a 14.84% equivalent-mutant misclassification rate, disclosed rather than netted out.
ContractNLI retention clause
A category promotion was refused: the gold labels are irreducibly mixed on return/destroy-all obligations without an explicit no-retain clause. The oracle holds rather than fits the noise.
One architecture
Models, humans, and search procedures may propose. They do not certify themselves. An independent check decides what is proven, what is omitted, and what is contradicted; repair is aimed only at the exact residual; and once work is independently admitted, ByteVerity attempts to retain it so future executions pay only for what remains.
Every experiment on this page is a test of a different segment of this loop — rule compilation, agent gating, kernel proof, hardware reuse, exhaustive enumeration, or auditing the authority itself.
PROBLEM / RULEBOOK
↓
PROPOSE (model, human, or search — untrusted)
↓
INDEPENDENT CHECK (compiled oracle, kernel, grader)
↓
PROVEN / OMITTED / CONTRADICTED
↓
EXACT RESIDUAL
↓
REPAIR ONLY WHAT REMAINS
↓
RETAIN VERIFIED CAPABILITYHow we grade ourselves
Wherever possible, predictions are hashed and fixed before labels are opened.
A verifier that cannot reject deliberately broken implementations does not count as a verifier.
When authority is incomplete, the system refuses rather than manufactures certainty — and the refusal is logged.
Local, frozen, submitted, externally validated, and projected results are different evidence classes, labeled as such.
Evidence index
External comparators always link to the external source. Results that exist only as frozen local artifacts say so, and can be inspected under NDA.
RuleArena
tau2-bench
Legal corpora
PyJWT formal audit
LITHO / IRU-F2
The pattern we are testing
Use intelligence for novelty. Keep authority independent. Retain what can be verified. Recompute only what remains unresolved.
Each result above tests one piece of that claim — including the pieces that failed. The dossier is updated when the evidence changes, not when the message does.