Evidence

The verified-program benchmark

When an agent builds a feature, what matters is whether the program does what was asked, and the agent's own tests may not show that. Our bet is that an agent writing Bosatsu for a known engine and checking it with our tools (api verify, why, dist, conformance), reaches a program that passes a hidden check on fewer tokens than an agent writing the same features in TypeScript from scratch with whatever tests it thinks prove them.

This benchmark measures that bet on the forum demo: four features, seventeen commissioned properties, and one call-sequence harness that neither arm sees. The hidden harness decides which properties each program establishes, and we count the tokens each arm spent getting there. An agent's own tests, verdicts, and claims count only toward calibration. The README states the adapter contract, the scoring, the judging asymmetry on task 3, and the disclosed biases.

The recorded result (iteration 001, 2026-09-05): the gate fails on every pair

Three fresh sonnet agents per arm per task, twenty-four runs. The Bosatsu arm established 16 of 17 properties on every run; the TypeScript arm established 16, 17, and 17. The Bosatsu arm spent roughly twice the tokens: tokenLift (TypeScript tokens per Bosatsu token) 0.54, 0.50, and 0.44 on the three run pairs. The pre-registered gate is accuracy(A) ≥ accuracy(B) and lift above 1 on each pair; it fails on all three, and the number is published as it came.

Tasks 1, 2, and 4 (the edit window, the locked thread, pinned-then-recent ordering) were 15 of 15 on every run of both arms, and no deliverable failed to compile, verify, deploy, or load. Both misses are on task 3, the reply cap under concurrent replies. The record attributes these misses to incomplete evidence, rather than an observed failing execution. On the Bosatsu arm the race property is read off the agent's own dist world, and all three agents declared the anti-vacuity witness outside the CoverageSpec the extractor discovers, after reverse-engineering an undocumented DSL from type errors: a brief and tool-documentation gap, charged to that arm as pre-registered and fixed before the next iteration. On the TypeScript arm one run's schedule walk was truncated at the scored budget on an adapter that generated more schedule steps; a diagnostic rerun at a larger budget exhausted the space with no failure, and the scored number stands.

Where the tokens went: the Bosatsu agents read a 500-line starting file, learned the language's surface by trial builds, and ran the verifier and the why tool between edits (4–19 tool invocations on tasks 1, 2, and 4 against 1–5 node runs on the other arm); task 3 alone cost 180k–225k tokens per Bosatsu run. What the tools bought is in the agents' notes and not in the score: boundaries confirmed with why on seeded rows, and a missing write permission caught by api verify when a reply began to update the thread.

summary.json carries every run's established count, tokens, per-task results, iterations, calibration, and the three gate verdicts; gate-run1.json, gate-run2.json, and gate-run3.json are the gate's own artifacts. iteration-001.md is the record: the design written before the runs, the results appended. The committed results directory holds every deliverable both arms wrote, every classification, score, and the token ledger.