One typed specification of what it means for a bank's books to be correct — and the dashboards, the SQL, the test scenarios and the regulator-ready audit PDF all derive from that single spec, with a release test that proves they agree row for row. You don't hand recon-gen a dashboard layout. You describe an institution ONCE — its accounts, rails, transfer templates, limits — and everything downstream is a projection of that one spec.

It's open source, on PyPI, with two live demos you can click through right now (repo · handbook · the SPEC).

Rather than tour every feature, let me show you the spine the way I'd explain it at a whiteboard (and I LOVE a whiteboard): take ONE law and follow it the whole way down — from the written spec, to the math, to the SQL the engine emits, to the cell an accountant clicks on a dashboard. The law I'll use is drift, because it's the most basic reconciliation question there is.

The concept: what drift is

A bank records a stored balance for each account at the end of each day — the number it would report if you asked "what's in this account?" It also has the postings: every credit and debit that hit the account. Those two had better agree — the stored balance ought to equal the running sum of the postings.

Drift is the disagreement. When the number the bank wrote down doesn't match the number its own transactions imply, that gap is drift — a missing posting, a duplicate, a feed that quietly fell out of sync with the ledger. Zero drift means the books reconcile; non-zero means something is wrong and you want to find it before a regulator does.

direction: down
base: "base tables\ntransactions + daily_balances" { style.fill: "#f6f8fa"; style.stroke: "#d9e0e6" }
cur: "Current* matviews\nlatest entry per logical key"
comp: "computed_subledger_balance\nΣ posted legs per account · day"
drift: "drift matview\nstored − computed\n(rows ARE the violations)" { style.fill: "#e7f0d4"; style.stroke: "#5f7a2a"; style.bold: true }
dash: "L1 dashboard\nthe Drift sheet"
base -> cur -> comp -> drift -> dash

The axioms: the typed model it stands on

Before you can state the law you need the nouns, and in recon-gen they're all typed — which matters later, because a typed model is what lets a mistake fail at code-generation time instead of in front of a customer.

• Money is a signed decimal in a currency, with the sign tied to direction: a credit is \ge 0, a debit is \le 0.
• An Account has a Scope — Internal (ours) or External (a counterparty) — and an optional parent, so accounts form a tree where leaves roll up into parents.
• A StoredBalance is one asserted end-of-day number for an (account, day). Corrections happen, so a logical key can carry several versions; the one that counts is the latest. The spec names that projection CurrentStoredBalance:

That "latest entry wins" projection is the first SQL layer — a materialized view that takes the max entry per logical key. Everything else builds on it.

The theorems: computing the balance

Drift compares two numbers, so the spec defines both. The computed balance is the cumulative net of every posted transaction through the day's end — not just that day's activity, everything up to it:

And drift is just the stored balance minus that:

That's the whole idea on one line. Younger me would be crying at the math notation / proofs but each of these rules flow on on top of each other.

The constraint: the law itself

The spec states drift as a SHOULD-constraint (RFC 2119 — a healthy feed satisfies it; a violation is a finding, not a crash):

In words: for every leaf internal account-day, the stored balance should equal the computed balance. Leaf-only, because parent accounts have their own roll-up law (ledger drift); internal-only, because we don't get to police a counterparty's books. That's the actual text in the spec, not a paraphrase.

From the law to the SQL

It's realized as a PostgreSQL materialized view, and the spec predicate rides along as a comment directly above the query:

-- SPEC: For every CurrentStoredBalance where Account.Scope = Internal
-- and ¬IsParent(Account), Drift(Account, BusinessDay) SHOULD equal 0.
-- Rows in this view are the violations: stored ≠ computed.
CREATE MATERIALIZED VIEW spec_example_drift AS
SELECT
    sb.account_id,
    sb.business_day_start,
    sb.effective_money                        AS stored_balance,
    cb.computed_balance,
    sb.effective_money - cb.computed_balance  AS drift
FROM spec_example_effective_balances sb
JOIN spec_example_computed_subledger_balance cb
  ON cb.account_id        = sb.account_id
 AND cb.business_day_start = sb.business_day_start
WHERE sb.account_scope       = 'internal'
  AND sb.account_parent_role IS NOT NULL            -- internal leaf accounts
  AND sb.effective_money     IS NOT NULL
  AND sb.effective_money    <> cb.computed_balance; -- the disagreement = a row

(Trimmed to the columns that carry the logic — the real view, all three dialects, is here.)

A few things worth noticing, because they're the difference between a demo and something you'd trust:

• The rule does not automatically generate the SQL. We keep them side by side for review but formally deriving one from the other AT RUNTIME is an open area of research. We're doing our best!
• The rows ARE the violations. Healthy is an empty view. There's no separate "check" that can disagree with the data — the disagreement is the query.
• It layers cleanly. effective_money and computed_subledger_balance are themselves matviews, over the "latest entry wins" Current* projections, over the base tables. One refresh recomputes the whole chain in dependency order.
• The detector does no math. The Python that surfaces violations just SELECTs the view and projects the integer cents back to dollars at the boundary (detect()). The arithmetic lives in exactly one place: the SQL that derives from the spec.

direction: right
law: "the law (SPEC)\nDrift = stored − computed,\nSHOULD = 0" { style.fill: "#e7f0d4"; style.stroke: "#5f7a2a" }
sql: "one matview per dialect\nPostgres · Oracle · DuckDB"
dash: "the Drift sheet\nthe account-days\nthat broke the law"
law -> sql: "realized as"
sql -> dash: "rendered to"

And it emits to Postgres, Oracle and DuckDB from one call site — because the demo runs on DuckDB, the audit deploys on Postgres and a customer might be on Oracle, and all three have to report the same violations. We don't use a SQL transplier because our tricks to work around the quicksight/oracle/duckdb limitations.

How it shows up on the dashboard

The matview is the truth; the dashboard is how a human meets it. Drift gets its own sheet on the L1 reconciliation dashboard — one row per offending account-day, with the stored balance, the computed balance, and the gap between them.

The demo seed plants one on purpose: a +$75 discrepancy on the bigfoot-brews account. It surfaces as a single row on the sheet:

From there the accountant's move is mechanical: filter to that account, diff the day's postings against the stored number, find the missing or duplicated $75, fix the feed, refresh.

You can click the real thing, no install:

• The spec demo — the four persona dashboards over one ledger, with tabs written as plain-English questions.
• Sasquatch Studio — the build side: the model editor, the topology diagram and the training simulator that lets you inject a drift and watch it surface on the sheet.

Want me to go deeper?

That's one invariant of about a dozen, walked end to end. If there's interest I'll do the same for a hairier one — the per-rail limit breach, the chain-XOR alternation check or the four-way agreement test that proves the dashboards, the audit PDF and the raw SQL all report the same violations, row for row. Just ask.