Code review from facts about the compiled program

Ask concrete questions about a Bosatsu program: which inputs reach a result, which fields go unread, and what changed after an edit? We built tools that extract facts from the compiled program and test a reviewer’s claims against them.

Each result distinguishes a static fact from a bounded observation of seeded runs. Start with the pricing example below, or run the checks yourself. The tools analyze Bosatsu programs.

Worked example: four facts from a pricing module

Here is a small pricing module (it ships in the repository at demos/pricing, with the commands to reproduce these findings below). It contains deliberate input-ignoring examples and a function that stays constant in the sampled runs.

struct Order(id: Int, qty: Int, discount_code: Int)

def quote(o: Order) -> Int:
  _ = o          # the order is thrown away...
  42             # ...and the "computed" price is hard-coded

def shipping_fee(subtotal: Int, region: Int) -> Int:
  match cmp_Int(region, 0):
    case GT: add(subtotal, 5)
    case _:  add(subtotal, 5)   # both branches identical: region decides nothing

def surge_bonus(x: Int) -> Int:
  match cmp_Int(x, 1000):
    case GT: x        # looks input-dependent...
    case _:  7        # ...the sampled inputs all take this branch

One command, yichus explore --agenda --limit 500 demos/pricing/*.bosatsu (the “agenda” is the tool’s list of noteworthy facts, one card each), produces the excerpts below. The seeded observations use type-derived inputs for this pricing module; they do not establish behavior for every input. Read the complete captured agenda.

Every fact is located and machine-checkable; the run-based ones carry the seed their inputs were generated from. None of them says “bug”. You decide which of these count as bugs. The tool provides a reproducible analysis result; its correctness still depends on the analyzer and its modeled semantics.

Agenda taxonomy: thirteen fact card types

There are thirteen kinds of fact. Each one comes with real code, or with a direct route to the checker that emits it. The taxonomy separates structural findings from seeded observations and declared-flow conformance. The first eight are computed from compiled structure. The next three summarize seeded, type-derived runs; absence or constancy observations are labeled “bounded observation, not proof.” The final two classify each mutation named by a FlowSpec as a structural instance or a located divergence. Run the taxonomy with the explore --agenda command below. The static and flow card emitters are in ExplorerAgenda.scala; seeded observation cards come from ExecutionEvidence.scala.

struct Order(id: Int, qty: Int, discount_code: Int)
# id and qty are read by accessors; discount_code is read by nothing

def quote(o: Order) -> Int:
  _ = o
  42

def shipping_fee(subtotal: Int, region: Int) -> Int:
  match cmp_Int(region, 0):
    case GT: add(subtotal, 5)
    case _:  add(subtotal, 5)

def summary(o: Order) -> Int:
  quote(o)      # quote discards o entirely

def quote(o: Order) -> Int:
  _ = o
  42

refresh: IO[Int] = (
  c <- cell.flat_map()
  _ <- c.read().flat_map()   # read the cell...
  pure(7)                    # ...ignore it, return 7
)

reset: IO[Unit] = (
  c <- cell.flat_map()
  c.write(9)     # overwrites whatever was there, unconditionally
)

package Demo/Report
from Demo/Pricing import Order, quote

def quote(o: Order) -> Int:
  _ = o
  42

def pick_quote(x: Int) -> Int:
  match cmp_Int(x, 999):
    case GT: fallback_quote(x)   # sampled inputs may miss this branch
    case _:  x

def surge_bonus(x: Int) -> Int:
  match cmp_Int(x, 1000):
    case GT: x
    case _:  7

struct Quote(total: Int, currency: String)
def price(o: Order) -> IO[Quote]: ...   # served at /price; nothing in Bosatsu reads currency

Claim verification: supported, refuted, and not-provable verdicts

A review (yours or an AI’s) is submitted as claims, and the verifier answers from the facts. Three claims about the module above:

{"claims": [
  {"kind": "literal-result",   "package": "Demo/Pricing", "binding": "quote"},
  {"kind": "no-detached-read", "package": "Demo/Report"},
  {"kind": "dead-field",       "package": "Demo/Pricing", "struct": "Order", "field": "qty"}
]}

Save the JSON above as claims.json. Running yichus verify-claims claims.json demos/pricing/*.bosatsu produces these verdict excerpts (claims, complete output):

The exit code is 1 because one claim was refuted, so a wrong review fails the same way a failing test does. Look at the second verdict: the absence of detached reads in the stated scope is backed by an enumerated count of the read sites examined. Claim vocabulary is intentionally narrower than the card taxonomy. There is no generic no-<kind> constructor. Selected static facts have direct claims; five card families have general absence claims, package reach has its own negative claim, and flow conformance has flow-instance plus no-flow-divergence. Use a drained claim when a universal statement depends on processing every card in another family. The full vocabulary is in the agent tooling guide.

Fact diff: what changed between two versions

yichus fact-diff compares extracted facts for two source sets, reporting introduced and removed findings and downstream consumers. Replacing a computation with a literal can introduce a literal-result finding and leave callers passing arguments that no longer affect the result.

For a reproducible before/after example, use the fixtures in FactDiffCommandTest.scala. The command recipe below accepts your own two source versions.

Benchmark: fact-tool review versus source review on planted defects

The experiment generates Bosatsu codebases with planted defects (“needles”). Each round is a matched pair: one AI reviewer gets the fact tooling, one reads source, and both are scored against a hidden key. Every round’s raw record is committed under eval/haystack/results/ and rendered on the scoreboard, which defines the columns, the contract-accuracy gate, and the rounds the tools lost. 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. Round 008’s nominal 60k caps failed to bind.

Recorded outcomes on that scoreboard:

• On a 46,922-line codebase with 26 planted defects (round 008), nominal 60k caps failed to bind and both reviewers spent about 100k tokens. The fact-using AI reviewer found 25 of 26; the source-reading reviewer found 23 of 26. Its misses were the defects whose evidence was spread across files it could not afford to open.
• On a 15,417-line round (005b), both reviewers found all 10 planted defects. The fact-using reviewer got there reading 0.4% of the source and spending 23% fewer tokens (142.0k vs 184.7k).
• The rounds vary in program size, defect set, and tool version. They do not isolate the effect of codebase size on review cost.
• Wrong claims get caught. In round 003 a weak (haiku-tier) reviewer filed six false positives. Two of them called a field dead that the tool’s own reads list showed being read (CrewShift.crew_id at crews.bosatsu:149 and FuelOrder.flight_code at fueling.bosatsu:110). The other four were a different shape. It declared the layering clean when the boundaries facts showed an inversion. It reported the declared checker predicates as fabricated computations. It said a parameter never influenced a result when its own text said the opposite. It filed seven “fabrications” that were all label tables or predicates, and missed the one real fabrication. Round 004 made machine-checked claims mandatory, and every checkable claim the same tier filed came back supported (32 of 32, 0 refuted). Three false positives of a different shape survived. All three were universal negatives such as “handler state reads are never detached”, which no claim kind covers. The round recorded that as an open gap.

Build the CLI and run the pricing checks

Needs git, a JVM (17+), and sbt; sbt assembly writes yichus.jar under target/. The pricing module above ships in the repo, so this works end to end:

# one-time setup
git clone https://github.com/snoble/yichus && cd yichus
sbt assembly
alias yichus="java -jar $(pwd)/target/scala-*/yichus.jar"

yichus explore --agenda --limit 500 demos/pricing/*.bosatsu     # up to 500 fact cards
yichus explore --agenda --agenda-type dead-field \
  demos/pricing/*.bosatsu                           # one fact type

# save the three-claim JSON from the section above as claims.json:
yichus verify-claims claims.json demos/pricing/*.bosatsu

# fact-diff wants a "before": copy the module, then edit
# old/pricing.bosatsu to give quote a real computation.
# Compare that edited version with the shipped constant version:
cp -r demos/pricing old
yichus fact-diff --before old/pricing.bosatsu \
  --after demos/pricing/pricing.bosatsu

There is also yichus spec, which checks declared Bosatsu system properties with Yichus’s native bounded and structural methods and records results with counterexample traces. Use --output verdict.json to save its legacy 2.2 JSON artifact. Add --require-holds invariant-name when a named invariant must hold conclusively for the command to succeed. An inconclusive result otherwise remains visible in the artifact; TLC is not run by this command yet. The check chooser compares the available tools. See the spec-first verification demo.

All the benchmark data, including the losses →
Explore the facts live in the playground →

Early UI fixtures and experiments live in the archive.