Project 01 / 07 / shipped

Tally

A small bank on a double-entry ledger that never loses or doubles a cent, even when the network fails mid-payment.

From the write-up

Tally is a small bank that can never lose or double a cent. Every transfer is written as two entries that cancel out, a payment retried after a dropped connection lands exactly once, every balance can be rebuilt from scratch to prove nothing leaked, and suspicious transfers are flagged after they land with the evidence attached.

Headline numbers / 2

Transfers pushed through 7 runs on Kubernetes while the network and database were made to fail. Not one cent lost or doubled.: 11,054none lost; From the Tally README, fault runs summary line (7 runs, 11,054 transfers and 1,580 retries, 0 violations).
Of transfers flagged as fraud on data the rules had never seen, 82% really were fraud. The first version managed 37%.: 0.8179up from 37%; From the Tally README, fraud table, row Precision / recall on a fresh seed (20260926).

Decisions I made and things that broke

I locked account rows in one fixed order, so two transfers crossing between the same accounts cannot block each other forever.
The first failure tests found five real bugs, now each covered by a test. A stale address cache kept the service calling a dead database for a minute.
Fraud scoring happens after each payment is saved, so a slow or broken scorer can lose a score but never a transfer.

What this proves / 12 skills

AI / ML

Fraud and anomaly detection: Of transfers flagged as fraud on new data, 82% really were fraud. The first rules managed 37%.

Systems

Point-in-time features: A checker rebuilt 16 fraud signals for all 9,290 payments using only earlier data. It found no mismatches.
TLA+ and z3: A TLA+ model follows the transfer code line by line. It passed across about 390,000 distinct states.
Concurrency: Account rows are locked in one fixed order, so two crossing transfers can never block each other forever.
Fault injection: Transfers kept flowing while the network and database were made to fail. Over about 11,000 transfers, not one cent was lost or doubled.

Web / backend

Java: The service is plain Java on the built-in web server, with lightweight threads and hand-written JSON.
PostgreSQL: Database rules back the ledger rules. Each payment key is unique, ordinary balances cannot go below zero, and no entry is zero.
Idempotency: A payment retried after a lost reply lands exactly once. None of about 1,600 retries was applied twice.
HTTP APIs: A small, fixed web API sits over the ledger, with no framework.

Infrastructure

Kubernetes: It is deployed to a local Kubernetes cluster from plain config files, and must pass four release checks plus a failure check.
Observability: Metrics are hand-written, and speed is timed from when each request was meant to go out, so waiting in line counts.
Tests and CI: Automated checks rerun the failure tests on every push as the fifth release check.

The demo, recorded

Tally demo: transfer, retry, reconcile, break it, flag it — Replays runs recorded from the real service: a transfer, a retry after a lost reply, a reconciliation, a fault injection, and a mule chain being flagged.

Papers / 3

arXiv 2607.05076, Can Code Specify a System Precisely Enough to Formally Verify It?It warned that code and its math model can share one misreading, so real failure tests back up the model.
arXiv 2608.22389, KONTOGRAPHIt led to a checker that rebuilds every fraud score with later payments hidden, to prove no score used the future.
arXiv 2609.24446, ActGovEvery new fraud rule is searched by a solver for a case that breaks the stated policies before anyone can turn it on.