0 Fork 0

Files

T

swaitsandClaude Opus 5.5 3609bf065e feat(core): prove the accounting laws (Kani + Lean); fix three engine gaps

The money arithmetic every invariant rests on now lives in one kernel,
ledger-core/src/kernel.rs: signing a line, totals, net, per-account
movements, reversal, normal balances, trial-balance columns, closing
lines, and the rounding plug for member splits. It is generic over a
checked `Amount` trait. The engine runs it on Decimal (validate,
movements, reverse_entry, account_balance, close_period_to, allocate,
trial_balance): there is one copy of the arithmetic, and it is the one
under proof.

Three layers, docs/verification.md maps every law to its proofs:

- Kani (src/proofs.rs): 17 harnesses prove the kernel at i64 for every
  input up to 4 lines over 3 accounts. An entry is accepted exactly
  when it is two or more positive, in-range lines whose debits equal
  credits; accepted entries net to zero; grouping by account loses
  nothing; a reversal mirrors and cancels its original; trial-balance
  columns balance iff the books net to zero; closing lines zero their
  accounts and a close balances however the net is split; the plug
  makes parts sum to the whole. No panics, no overflow. kani::cover!
  shows the proofs are not vacuous.
- Lean 4 (verify/lean): 24 headline theorems for books of any size. The
  ledger is a state machine (add account, draft, post, reverse, open,
  close), and in every reachable state the books net to zero, the trial
  balance balances (as of any date), and the accounting equation holds.
  Posting only appends ("posted is forever"), closed periods are
  frozen, a close zeroes revenue and expenses and credits exactly the net
  income, and period statements add up. Audit.lean shows standard axioms
  only, no sorry.
- Bridge (tests/kernel_bridge.rs): the Decimal and i64 kernels agree.

What the proofs found (each one missed by every test, fuzzer, and
mutant):

- The engine accepted negative line amounts; only MCP refused them. Now
  NegativeAmountLine: direction is the side's job.
- Summing lines near Decimal::MAX panicked. Lines are now capped at one
  quadrillion and ten decimal places (AmountOutOfRange), which keeps
  every realistic sum exact, and the kernel's sums are checked.
- FX conversion (foreign_amount * fx_rate) could panic the same way; it
  is now a checked multiply.
- Kani itself: 0.68 mis-models symbolic-length copy_from_slice
  (model-checking/kani#4904) and reported a reversal that doesn't net to
  zero. The counterexample, replayed natively, passes, and a 15-line
  standalone crate reproduces the bug. Harnesses avoid bulk copies, and
  a should_panic canary will flag the upstream fix.

`just prove` runs it all (Kani memory- and time-capped, fails on an
unsatisfiable cover or a non-standard Lean axiom). AGENTS.md now makes
formal coverage part of every core change.

Also, docs: GnuCash is *an* oracle, never *the* oracle (Stephen). The
spec is accounting principles, proved. Golden files are recomputed from
principles. External implementations (GnuCash, the old Sheet, QBO/Xero)
are cross-checks whose disagreements get adjudicated, never obeyed.
docs/oracle.md gains "Who is right"; AGENTS, README, architecture,
roadmap, parity, and STATUS are reworded to match.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GWVo7x3UHw5kwCUaWxiejX

2026-10-13 11:12:13 -06:00

4.7 KiB

Raw Blame History

Roadmap

Phase 1 — Semantics core (done)

The engine: money, accounts, journal, ledger commands, trial balance, P&L, balance sheet, cash flow, fixed assets with depreciation, golden files, property tests, mutation testing, fuzzing, and the docs an agent needs to work here. Parity floor: 12 done.

Phase 2 — AI-first interface (done)

The primary interface is MCP, not a cloned GUI (Stephen's call, 2026-10-10).

ledger-store: append-only hash-chained JSONL journal (source of truth), SQLite as disposable projection with auto-rebuild, content-addressed blob store, durable drafts.
ledger-mcp: 27 tools over stdio and Streamable HTTP, preview-before-post, server-side receipt policy (>$25) with anti-splitting, asset management, digest for human review, read-only resources.
ledger-import: QuickBooks CSV import (bank, chart), IIF and XLSX export.
Capability parity 12 of 12 vs the GSheet+GDrive system.
Parallel run with the sheet; cutover per the cutover rule (docs/parallel-run.md).

Phase 3 — Oracle harness (next)

ledger-oracle: fixture books through our engine and other implementations (GnuCash headless first), automatic snapshot() diffing. Each diff is adjudicated from principles; no other program is the authority.
Parity catalog becomes machine-readable; CI enforces the non-regression floor.
Done when: a fixture book produces byte-identical snapshots from both engines with zero manual steps.

Phase 4 — Read-only GUI (first version done, 2026-10-12)

ledger-gui: see plan/gui.md for the design and what's built.

Consumes the ledger-store event log: live updates — the answer to "watch its files to update live."
egui or web; a dumb client holding no accounting logic.
This is the trust layer for humans (Stephen, Kat, the CPA), not the primary interface. Read-only at first; editing stays with the agent.
Design references (Stephen, 2026-10-11; screenshots shared in session, described here):
- Reports with a date range and a column interval (QuickBooks Desktop's P&L: From/To plus Columns = Year/Quarter/Month/...): any statement split into one column per interval plus TOTAL, to see the books over time. The multi-column statement layout in ledger-import::report already renders this shape; the GUI (and the exports) need a per-interval builder over the period-scoped core statements.
- Financial dashboard (Coupler.io's QuickBooks dashboard): P&L, balance sheet, and cash flow overview tables with Last month / Month to date / Year to date columns, each beside charts — income vs. COGS + expenses vs. earnings bars; stacked assets vs. liabilities + equity; cash at end of period; net cash change.
- Business overview (QuickBooks Online home): cards for cash balance with a trend, expenses by category (donut), profit and loss (income vs. expenses), invoices (unpaid, overdue, paid), sales trend, and bank account balances.
- Revenue dashboard (Coupler.io): KPI tiles (paid, overdue, open invoices this month), an invoice table (number, customer, dates, currency, home and foreign amounts, balance, totals), expenses by category by month, invoices by status per month.
- QuickBooks Online dashboard: invoices (unpaid in the last year, overdue vs. not yet due; paid in the last 30 days, deposited vs. not), expenses by category (donut, last month), bank account balances (book vs. bank, items to review), profit and loss (net income, income vs. expenses bars), sales trend (line, by quarter).
- KPI tiles with comparison (QuickBooks accounting dashboard): income, cost of goods sold, expenses, net profit, each with % change vs. the previous 30 days; an auto date-range picker; cash balance over time with a trend line; revenue by month, stacked.
- Cash-flow dashboard: bank balance, debtors, burn rate, cash runway (days) tiles; income vs. expenses for the last six months; a net cash flow forecast with a confidence band; A/P and A/R aging by days past due (the engine already computes both agings); total burn over time.

Phase 5 — Workflow parity

A/R and A/P workflows, bank reconciliation, budgets, scheduled transactions.
Multi-currency with FX translation.
Period close.
The goal: a self-hosted bookkeeping system with a tested claim to proved accounting semantics (cross-checked against GnuCash and others) and capability parity with the old GSheet+GDrive workflow — no SaaS subscription required.

Explicitly not on the roadmap

Bank feeds, payment processing, payroll, tax filing. Those are integrations and regulated domains, not cloning targets. The engine gets clean seams for them; someone else's API provides them.

4.7 KiB Raw Blame History