So Fable is back out today (July, 2nd) so what better way to put it to the test than to take it for a spin on a VERY challenging problem I've wanted to look into for recon-gen.

In short the problem is this:

• Recon-gen works by establishing a set of axioms and theorem about accounting systems: https://github.com/chotchki/recon-gen/blob/v16.2.0/src/recon_gen/docs/SPEC.md#primitives-axioms
• Using those a set of sql queries are created to materialize the theorms and show violations: https://github.com/chotchki/recon-gen/blob/v16.2.0/src/recon_gen/common/l2/schema.py
• We then test these every way we possibly can think of: multiple database engines, planting and detecting violations

There is a hidden gap, a big one. How do you know that one derives from the next faithfully and correctly across the CLASS of inputs, not just our hand picked examples?

To address this I really wanted to leverage formal proofs to show the sql match or derive from the theorem.

However there is a very good reason why my college computer degrees are from the college of business NOT engineering. As much as I watch Veritasium (https://www.youtube.com/veritasium) for fun and enjoy all their math content, I CANNOT prove a theorem to save me. (Thus in college I switched from Computer Science to Management Information Systems).

This is where Claude's Fable model has been very helpful today. I knew I wanted to bridge this gap, I had done enough research to know Z3 (https://github.com/Z3Prover/z3) would be a suitable to help with this, I just had no idea how to make progress.

One VERY long ultracode session with Fable and I'm landing proofs for the correctness of the following parts:

• The laws. Every invariant now lives in ONE place as a small Python function written straight from the spec — drift is the reported balance minus the sum of posted legs, overdraft is a balance that can't go negative and so on (residuals.py). Nothing else restates them.
• The enumeration gate (this is the workhorse). The test harness emits the REAL sql a deployment would run, loads an exhaustive set of hand-built boundary cases into an actual database, runs the detectors and checks that the rows the sql flags are EXACTLY the rows the law calls violations. Every case, on DuckDB, Postgres and Oracle.
• A completeness check that turns an un-verified detector into a build failure (which is how I found one that had shipped its whole life covered by nothing).
• The Z3 lane. The SAME law functions run through the solver — no rewrite, no second copy (the prover) — to prove they behave for ALL integers: a violation in one account can't be hidden by unrelated activity in another, and the amounts scale the way money should.

(Claude here — Chris asked for Z3 and half-expected me to aim a theorem prover at his sql and declare it proven.)

I'm not that bad, just thought the spike was incorporated into the implementation... twice ;)

(The honest answer is sharper than that: to check the sql against the spec, running the REAL sql over every boundary case beats hand-writing a Z3 model of it, because that model is just one more copy of the law nobody has checked — and it can't see what the real database does, like a UNIQUE index blowing up a refresh. So Z3's real job is the smaller, harder one: proving the LAWS themselves are sound, so the thing we measure the sql against isn't quietly wrong. We built both. He signed off on exactly the right design, he just called it by the wrong name for an afternoon.)

Here's why any of this ties back to the real code. A reconciliation rule has to exist TWICE — there's what "drift" means (a sentence), and there's the sql that hunts for it across a customer's warehouse of millions of rows (a page of it, once per database engine). Those two drift apart the moment you stop watching: someone tunes the sql for speed, the meaning quietly shifts a column, and now your detector is lying with a straight face. This phase built a machine-checked bridge between them. The meaning lives in the Python law, the emitted sql does the hunting, and every build re-proves the two haven't drifted apart — exhaustively, on a real engine — or it goes red and hands you the exact case where they split. The Z3 half guards the other end, that the meaning itself is well-behaved. Neither half touches the other's copy, so there's no third artifact to keep in sync.

It's less a Venn than a spectrum — concrete and specific on one end, symbolic and unbounded on the other — and the honest bit is the blind spots. Each check misses exactly what the next one is built to catch, which is the whole reason all three exist:

# Same reconciliation rule, three checks — a spectrum, concrete + real-sql
# on top to symbolic + unbounded on the bottom. Each blind spot is the
# next check's reach: that's why all three earn their keep.
vars: { d2-config: { pad: 30 } }
direction: down

plant: "PLANT TESTS   (concrete · runs the real sql)\n\nreach:  the bug shapes I THOUGHT to plant\nblind spot:  a bug I never imagined" {
  style: { fill: "#eaf3ff"; stroke: "#3b7dd8"; stroke-width: 2 }
}
enum: "ENUMERATION GATE   (concrete · runs the real sql)\n\nreach:  EVERY boundary state, sql == the law —\ncatches shapes I would never have planted\nblind spot:  amounts outside the bounded domain" {
  style: { fill: "#eaf3ff"; stroke: "#3b7dd8"; stroke-width: 2 }
}
z3: "Z3 LANE   (symbolic · no database at all)\n\nreach:  the law holds for ALL integer amounts\nblind spot:  never touches the sql itself" {
  style: { fill: "#fff1e8"; stroke: "#d8813b"; stroke-width: 2 }
}
plant -> enum: "same real sql,\nwider net" { style: { stroke-dash: 4 } }
enum -> z3: "same law,\nno bound on the numbers" { style: { stroke-dash: 4 } }

To be clear, this is NOT to say recon-gen is formally proven, it is not and the research suggests that's not currently possible. That didn't make this useless, the process of working through implementing what we did found MANY subtle bugs and has added further rigor to the test suite. For me that is absolutely worth it and seeing that formal methods are so approachable now, I will probably be reaching for this tool far more often!

Image from Bonque & Kindermann photography, Public domain, via Wikimedia Commons