Fact tooling: code review from extracted facts

Yichus computes machine-checkable facts about programs, without heuristics or guesswork. Every fact is one of two things, and says which: a structural fact of the compiled program (exact by construction), or an observation of real, seeded runs (always labeled “bounded observation, not proof”). The catch: it works only on Bosatsu, a small language where every program terminates and every side effect is declared; those two guarantees are what make this possible. If you want code reviews (AI reviews above all) whose claims can be verified or refuted mechanically, this is for you.

Sixty-second version

Here is a small pricing module (it ships in the repository at demos/pricing, so every command on this page runs as written). It has three real problems, plus a fourth finding that only running the code can surface.

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        # ...but this branch always wins in practice

One command, yichus explore --agenda demos/pricing/*.bosatsu (the “agenda” is the tool’s list of noteworthy facts, one card each), reports this verbatim:

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. Whether each fact is true has already been settled mechanically.

Every fact type

Eleven kinds of fact, each with real code and the tool’s actual output. The first eight are computed statically, so they are exact by construction. Running the code on seeded, type-derived inputs produces the last three, which always carry the label “bounded observation, not proof.”

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)   # this branch never runs
    case _:  x

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

Check a review against the facts

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"}
]}

yichus verify-claims claims.json demos/pricing/*.bosatsu returns (actual 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: “nothing is wrong here” arrives backed by an enumerated count of the read sites examined. Every fact kind has a claim kind, plus no-<kind> absence forms; the full vocabulary is in the agent tooling guide.

Fact diff: what changed between two versions

yichus fact-diff computes all the facts for two versions of a program and reports which facts appeared or disappeared. Here someone replaced quote’s real computation with the hard-coded 42 (actual output, trimmed):

The change’s real story: the price became a constant, the callers’ data now goes nowhere, and the “depends on its inputs” evidence vanished. Each fact lists who is affected downstream (“blast radius: 2 consumers”), and claims like “no new dead fields” fail the change with exit code 1, same as the verifier.

Results

Measured on planted-defect codebases with independent AI reviewers, scored against a hidden key. The strongest results:

• On a 46,922-line codebase with 26 planted defects, at equal token budgets (~100k each): the fact-using AI reviewer found 25 of 26; the source-reading reviewer found 23 of 26. Its misses were exactly the defects whose evidence was spread across files it could not afford to open.
• The fact-using reviewer read 0.4% of the source and cost 46% less than the source-reading review, at equal accuracy.
• Facts’ cost barely moves with codebase size: 112k → 137k tokens while the program grew 16,000 → 47,000 lines.
• Wrong claims get caught: mandatory claim-checking took one weak AI reviewer from 6 false accusations to 0.

Try it

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 demos/pricing/*.bosatsu     # every fact, as 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 — the page's
# diff above is exactly that edit, seen in reverse:
cp -r demos/pricing old
yichus fact-diff --before old/pricing.bosatsu \
  --after demos/pricing/pricing.bosatsu

There is also yichus tla, a separate feature that model-checks declared state-machine invariants and reports holds/violated/inconclusive verdicts with counterexample traces. See the spec-first verification demo.

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