Evidence

Benchmark methods, results, and raw artifacts

The examples on this site show the tools working; they do not show how useful the tools are. Does an AI reviewer find more planted defects with computed program facts than by reading source? Can a reader answer questions about a program from its report? We ran benchmarks to find out. Read each result with its method and limits before drawing a conclusion about the approach.

There are five benchmark families: AI review with fact tooling, program-report reading, distributed-systems counterexamples, writing verified programs, and UI update performance. Each section below states the corpus or program, the comparison method, the recorded result, and a route to the files that support that result. The UI comparison runs locally in your browser; its results are not a committed scoreboard.

Read all of it as a self-run benchmark: the same project builds the tools, generates the challenges, and adjudicates the scoring. Most cells are single runs rather than averages. Failed rounds remain in the record with their reasons, and the benchmark scoreboards render from committed artifacts.

1. Fact-tooling review from computed facts and source

This benchmark measures whether machine-checked program facts beat source reading for AI code review. Each round generates a Bosatsu codebase with planted defects, then fresh AI reviewers hunt them. The programs use Bosatsu and Yichus’s declared IO operations. One works from the fact tools, whose page explains each compiled fact and reviewer query; the other reads source. Both are scored against a hidden key. Eleven rounds are recorded (000–008 and 010; round 5 ran twice), over codebases from 2,028 to 46,922 lines. The project builds the tools, generates the challenges, and scores the runs. Each cell is one run. Model labels are harness tiers, not exact model IDs. Nominal token caps in round 008 failed to bind.

Round 008, the largest recorded codebase, used 46,922 lines with 26 planted defects. At matched ~100k-token budgets, the fact-using reviewer found 25 of 26 and the source-reading reviewer 23 of 26. The record also keeps the losses, including rounds where the facts were slower and a weak-model round with false positives the claim gate cannot cover.

The fact-tooling scoreboard defines its columns and renders every recorded round. The served round 008 JSON contains the headline source and fact scores. The committed results directory contains every per-round artifact.

2. Program-report and source arms on the same quiz

This benchmark measures whether the committed program report page and examples explain enough typed-IR facts to answer review questions. One fresh agent answers a 30-question closed-option quiz about nine corpus programs from the committed reports alone; another answers the same quiz from the Bosatsu sources alone. Every answer-key label is re-derived from the engine's own output in CI, and the recorded verdict is re-checked byte-for-byte. The gate requires equal or better accuracy and tokenLift above 1 (source-arm tokens divided by report-arm tokens, so above 1 means the report arm was cheaper). This is a self-run, single recorded probe, rerun after table-status and cap-accounting changes.

In the recorded run (2026-08-19), both arms scored 29/30. The report arm spent 87,074 tokens against the source arm's 114,291. The measured tokenLift is 1.31, with the same accuracy on about 24% fewer tokens. The gate verdict is pass.

gate.json records the accuracy comparison, token lift, and gate verdict. artifact-score.json records the report arm, and baseline-score.json records the source arm. The committed corpus directory contains the quiz, answer key, reports, and results.

3. Reflection-auth review with and without a counterexample

This benchmark measures whether the distributed-systems checker page, which explains schedule exploration and counterexample traces, changes what a weaker model certifies. The system under test is benchmark task 010's mutual-authentication server with a reflection flaw. The bug exists only across two interleaved sessions. A haiku-tier model judged it three ways: from source alone, with the checker's counterexample schedule, and a control cell on the secure variant.

From source alone it returned SECURE, a false certification whose written argument even noticed the shared direction tag and then reasoned it away. With the counterexample in front of it, the same model returned VULNERABLE and reconstructed the attack. The control cell cleared the secure server. The probe has three cells and runs one trial in each, at about 19.9k tokens per cell. That records one observed case, and the sample is too small to estimate a rate.

iteration-009.md contains the three prompts, model responses, labels, and token counts. It is committed under benchmarks/dist/results/. The distributed-systems benchmark page describes task 010, the other task shapes, and the execution semantics.

4. A verified program in Bosatsu with the tools, or in TypeScript from scratch

This benchmark measures whether an agent writing Bosatsu with the yichus tools reaches a program a hidden property harness establishes with fewer tokens than an agent writing TypeScript from scratch with its own tests. Four forum features, seventeen properties, three fresh sonnet agents per arm per task, and a gate of equal-or-better accuracy with tokenLift above 1 on each of three run pairs.

In the recorded iteration (2026-09-05) the gate fails on all three pairs: the Bosatsu arm established 16 of 17 properties on every run against the TypeScript arm's 16, 17, and 17, and spent roughly twice the tokens (tokenLift 0.54, 0.50, 0.44). The unestablished property is on the concurrent-reply task: the record attributes the Bosatsu misses to a documentation gap in the dist DSL and the TypeScript miss to the harness budget. These explanations do not establish correctness beyond the checks that completed. The rounds the tools lost are published like the rounds they won.

The verified-program benchmark page carries the per-pair table, where the tokens went, and the two misses; summary.json is the served artifact every figure above is read from.

5. UI update throughput against React

The performance experiment asks whether compile-time knowledge of state-to-DOM dependencies can reduce runtime work. The browser harness compares compiled Yichus programs with real React implementations for a counter, a list update, and a targeted state update. Both sides use their actual runtimes.

After warmup, the harness samples each implementation’s update API in bounded batches, yielding between batches and waiting for React to commit before queuing more work. It sums only the time spent issuing calls; the waits are excluded. It does not wait for a committed render after each call. The result is update-enqueue throughput, not frame rate or interaction latency. The implementations also do different work per call: the React list scenarios copy their state collection, while Yichus writes a named state path.

Results depend on your browser, machine, and batching settings. Each row records the controls and browser used; results disappear on reload. No cross-machine speedup is claimed here.

Run the comparison and inspect its linked Bosatsu sources; read the timing harness and React implementations; follow the compiler’s binding map through an actual counter update.