Yichus

Yichus answers questions about programs. Which inputs affect this output? Why did this value come out the way it did? Is it safe to apply this batch of transfers? Every answer is checkable instead of being a guess: a structural fact of the compiled program, a replayed concrete run, or an honest “can’t be sure, because…”. The catch is also the reason it works. Programs have to be written in Bosatsu, a small language where every program terminates and every side effect is declared. That is the research bet. A language this small is what buys the guarantees, and there is no retrofitting them onto the Python or TypeScript you already have. The same compiled form does double duty: it runs the interactive demos on this site, and the code-review fact tools read it.

Why? is per-value provenance: click any output and see exactly how it was derived. What-If re-runs with changed inputs and compares outcomes. New here? Start with the Playground. You can also watch Why? work in the tax calculator, or read the AI code-review story.

Exact, Checkable Program Facts Verifiable AI Code Review Why? + What-If Provenance Benchmarked, Losses Included

Fact tooling for coding agents Measured

Fact Tooling: Review From Extracted Facts

Exact, checkable facts about a program: which fields are never read, which inputs never affect an output, what happened when it ran. An AI reviewer's claims then get verified mechanically against those facts.

Verified Mutation Flows: A Tutorial

You write the multi-step mutation flow once, as a factory nobody calls. Every mutation stays plain straight-line code, and a checker proves each one follows the flow. Extract the parts afterward and you get an all-or-nothing batch for free.

Measurements

On a 47k-line codebase with 26 planted defects, a fact-only AI reviewer found 25 with zero false accusations. A source reader at the same token budget found 23. Given unlimited budget, the reader found all 26, at 1.85× the cost. Full data for every round, including the ones the tools lost.

Mini-Ledger Batch Admission

Declare which account balances must never go negative. The checker then decides which transfers in a batch can be safely admitted, and it hands back a trace explaining every deferral, verified by replaying the real handlers.

Spec-First Verification

Declare state-machine properties in Bosatsu, then watch verdicts flip from inconclusive to violated (with counterexample traces) to holds.

 Explorer trust overview screenshot

Explorer Trust Verification

Detect when AI-generated functions fake their outputs, meaning hard-coded results dressed up as computation. The check uses the same provenance and dependence facts as the rest of this site.

Explorer Playground

Interrogate an existing Bosatsu codebase in your browser: overview, trace, search, guided lessons. (This one answers questions about code. The Playground below is where you write it.)

Playground

Write Bosatsu simulation code and compile it entirely in your browser, with no server required. It opens with a working example. Edit that, run it, and click any result to see its Why? provenance.

Open Playground Powered by Scala.js

Featured demos

How It Works

The architecture, end to end. Watch a button click become a direct DOM mutation with zero re-renders, and see why the analysis reads that same compiled form.

Why? Panels in the Tax Calculator

Open the tax calculator and inspect exactly how each output was derived.

Provenance Explorer

Watch data flow light up as derived values trace back to their sources.

IO Effects Are Values

Step through an IO lifecycle and see why effects-as-values makes static analysis possible.

AI Code Detection

Detect when AI-generated code fakes outputs instead of using real inputs.

Time Travel Puzzle

Program a move loop, predict future-self collisions, then verify the replay. The rules are pure Bosatsu.

Learn

Interactive Tutorial

Follow a Yichus-specific walkthrough and jump to Bosatsu docs for language basics.

IO Analysis Sidecar

Export the compiled program's analysis file, .matchless.analysis.json. (Matchless is Bosatsu's compiled form.) You get IO sites, causal edges, and per-binding purity summaries.

Explorer + Debugger

Drive a stateful debugging session over compiled Bosatsu from the CLI daemon (yichus's long-running analysis server) and the explorer at once.

Service Analysis

Audit CRUD services for permission findings and query diagnostics, derived from the compiled program's typed intermediate representation.

View on GitHub

github.com/snoble/yichus holds the docs, the source, the measurement artifacts, and local setup (JVM + sbt).

Simulation demos Why? + What if?

Investment

Run a set of portfolio assumptions and compare how the scenarios come out.

source

Archive

early experiments, toy demos, and fixtures, kept for the record

UI building blocks

Counter

The smallest state update there is. The same event always gives the same output.

source

Todo List

Operations on list state, where adding and removing take predictable update paths.

source

Form Input

Controlled inputs that stay in sync with state, with no hidden effects.

source

Particles

A lot of animated state changing at once, driven by incremental runtime updates.

source

Standalone pages

Particle System

Five particles with gravity, bouncing, and damping. 60fps canvas animation in pure Bosatsu.

Cross-Platform Drag & Drop

Items move between zones on desktop and mobile, using O(1) style binding updates.

UI Update Benchmark

Direct incremental updates compared against React 18 render loops across three scenarios.

More calculators

Compound Fold

Fold-based compounding, a language-mechanics exercise.

Closure Capture

How closure capture behaves, as a language-mechanics exercise.

Game fixtures

Time Travel Stepper

Step the deterministic rules fixture tick by tick to inspect collisions, rewinds, and win conditions.

source

Grid Smoke Test

Validate the reusable grid renderer, tile palette, and entity drawing primitives that power the game.

source