wanderbooks/docs/verification.md

Formal verification: the accounting laws, proved

Tests check the examples someone thought of. Proofs check every case. wanderbooks proves the fundamental laws of double-entry bookkeeping three ways, each covering what the others can't:

Layer	Tool	What it proves	Scope
Code	Kani (bounded model checking)	The engine's own Rust kernel is correct and never panics or overflows	Every input within the bounds: up to 4 lines, 3 accounts, amounts to 2^40; proration by days up to 3 month parts (bounds below)
Laws	Lean 4 (machine-checked proof)	The laws hold for books of any size, after any sequence of commands	Unbounded: any number of entries, accounts, periods, steps
Bridge	proptest	The kernel on Decimal (what the engine runs) agrees with the kernel on i64 (what Kani proves); proration's i128 (the engine's) with its i64 and i32	2,000 random cases per property

Run all of it with just prove (after mise install; see the end).

The kernel

Every invariant rests on a little arithmetic: signing a line, summing sides, grouping by account, flipping for a reversal, reading a balance on its normal side, splitting a movement into trial-balance columns, closing an account, plugging the last share of an allocation. That arithmetic lives in one place, crates/ledger-core/src/kernel.rs. Its functions are small, pure, and generic over an Amount trait with checked operations. The engine calls them on Decimal: JournalEntry::validate, movements, reverse_entry, account_balance, account_movement, period closing, periods::allocate, and the trial balance. There is no second copy of the arithmetic for proofs to drift from.

Kani compiles the same functions at i64 (exact integer money in the smallest unit; the four proration charge harnesses at i32) and explores every input in the bounds. (Grouping by account is proved through movements_into, the allocation-free core that movements wraps: symbolic heap growth is beyond what the model checker explores in reasonable time.) The Lean model in verify/lean restates each function over Int (proration over Nat, both of prorated_through's branches) and proves the laws with no bounds at all.

The laws

Each law, and what proves it. Kani harnesses are in crates/ledger-core/src/proofs.rs; Lean theorems are in verify/lean/Wanderbooks/.

Entries

1. An entry is accepted exactly when it has two or more lines, every amount is positive and in range, and debits equal credits, to the unit.
   • Kani check_lines_is_exact (both directions: no bad entry gets in, no good one is refused), out_of_range_is_rejected
   • Lean Accepted
2. An accepted entry nets to zero.
   • Kani accepted_entry_nets_to_zero · Lean Accepted.net_zero
3. Grouping by account loses and invents nothing: each account's movement is the net of its own lines, and the movements sum to the entry's net.
   • Kani movements_are_per_account, movements_sum_to_the_net · Lean sum_movements
4. Sums are exact and never overflow for in-range lines.
   • Kani sums_are_exact (every harness also fails on any panic or arithmetic overflow)

Reversals

5. A reversal is accepted exactly when the original is, and the two together net every account to zero.
   • Kani reversal_mirrors, reversal_cancels, flip_negates
   • Lean accepted_reversal_iff, movement_with_reversal

Balances and statements

6. Normal sides: a line on an account's normal side raises its balance by the amount; the other side lowers it.
   • Kani normal_side_increases · Lean balance_after_line
7. The trial balance balances, and it balances only if the books net to zero: it is a complete check of the arithmetic.
   • Kani trial_balance_columns · Lean trial_balance_iff, Reachable.trial_balance, Reachable.trial_balance_through (as of any date)
8. The accounting equation: Assets = Liabilities + Equity + (Revenue − Expenses), always and as of any date.
   • Kani normal_balance_is_signed (the fact it rests on, every type and amount) and accounting_equation (end to end, up to three accounts: regrouping signed 64-bit sums is hard for a SAT solver) · Lean accounting_equation, Reachable.accounting_equation, Reachable.accounting_equation_through (any number of accounts)
9. Period statements add up: a year's P&L is the sum of its months'.
   • Lean statements_add_up
10. The statement of cash flows foots (rules.md B-14, plan P3 defect 1): each entry's cash is applied to the sections moving against it, operating, investing, financing, each up to its own movement; what a member or a lender paid or received for the entry, with no cash account moving (rule 11, D-42), is added as a constructive receipt and disbursement that nets to zero within the entry; so each entry's flows sum to its cash and what neither settled sums to zero, and operating + investing + financing is exactly the change in the cash accounts, over any entries, for any tagging whose cash tag follows the account. A reversal's flows, constructive ones included, are its original's negated (so an entry and its reversal in one period drop out together), and net income plus the reconciling items (gains and losses on investing assets, the noncash operating parts, the changes in operating balances) is the operating section, whenever revenue and expense lines are only operating or investing. The engine checks the same identities at runtime and refuses (CashFlowDoesNotFoot) rather than show a statement that doesn't foot.
    • Kani entry_flows_sum_to_cash, entry_flows_pure_are_movements, entry_flows_are_bounded, no_cash_no_flow (end to end on entries of up to three lines, each in any of the four places: four lines ran past half an hour per harness); the reversal's mirror at three lines in two halves, entry_movements_of_a_reversal_mirror (a reversal's cash and section movements are its original's negated) and flows_of_mirrors (kernel::flows_of is odd, for any movements three lines can make), kernel::entry_flows being the one then the other, and end to end on up to two lines, entry_flows_of_a_reversal_mirror (at three lines end to end it took about 14 minutes alone, 2026-10-20, and past 30 minutes at four jobs on a busy machine, 2026-10-21; split then, nothing weakened: the halves cover every three-line entry the end-to-end harness did), take_is_odd_and_bounded, apply_cash_mirrors (the parts, for any amounts), apply_cash_spends_exactly (how a section's cash splits among its kinds, operating's classes included), exchanged_is_bounded (the exchange inside investing and financing that is disclosed, given the cash in and out of the two sections), constructive_nets_to_zero and constructive_mirrors (what a member or lender paid or received for the company, either way, for any amounts: the parts net to zero, settle their own movements toward zero and no further, leave no source beside a use it could settle, and mirror under a reversal)
    • Lean net_splits_by_flow, applyCash_conserves, applyCash_exhausts, applyCash_neg, entry_flows_sum, flows_reversal, constructive_nets, constructive_neg, constructive_sections_net (the kernel's constructive modelled as it is written: two passes of applyCash; its parts by section net to zero), stmt_flows_sum, stmt_flows_reversal (an entry's statement flows, its cash flows plus any constructive triple that nets to zero, and mirrors for a reversal), and over them cashflow_sections_sum_to_cash_change, secNet_cash_is_movement, operating_reconciliation_ties, operating_reconciliation_ties_all, cashflow_reversal_nets; Reachable.cashflow_foots and Reachable.cashflow_is_change_in_cash (in every reachable state: the sections over the entries between two days are the cash accounts' ending balance less their beginning)
    • bridge entry_flows_agree, apply_cash_and_exchanged_agree, constructive_agrees; properties prop_cash_flow_laws, prop_pure_entries_sections_are_movements (5,000 cases each)

The books over time

The Lean model (Ledger.lean) describes the engine as a state machine: add an account, start a draft, post, reverse, open a period, close one, and record how the books are kept (a setting, convention, decision, open item or approval: one step, record, each record abstracted to a number). Each step carries the checks the engine makes before it mutates. These theorems hold in every state reachable from empty books, by any sequence of commands, of any length:

11. The invariant holds: chart codes are unique, every posted entry is acceptable and on known accounts, and no draft is dated in a closed period. (That last one is why the store can journal a post before applying it: a post can never then fail on a closed period.)
    • Lean Step.inv, Reachable.inv
12. The books always net to zero. · Lean Reachable.books_net_zero
13. Posted is forever: posting only appends. After any sequence of commands the old log is a prefix of the new one. Nothing is edited, reordered, or removed.
    • Lean Step.extends, Steps.extends
14. Closed periods are frozen: once a period is closed, no sequence of commands adds, removes, or changes an entry dated in it, and it stays closed.
    • Lean Step.frozen, Steps.frozen
15. How the books are kept changes no entry: in the model, a record (a setting, convention, decision, open item or approval; a vendor's 1099 decision or W-9 flag, a payment method, an entry's payment-method tag) leaves the chart, every posted entry, every draft and every period exactly as they were, and any number of them keeps a reachable state reachable. The model's record step touches only the records by definition, so the proof says the model is sound, not the engine; the engine's side is checked by settings_replay_is_pure, which snapshots every figure and entry around each record (rules.md B-29), and for the 1099 records by decision_and_method_records_change_no_entry (ledger-store tests/form1099.rs; they change the 1099 worksheet by design, never an entry). Settings that change how the same entries are presented (the fiscal year, cash flow roles, members) are outside this law by design. A rename (rename_account, P3, rules.md B-31) is a record too: the model's chart is (code, type) (Ledger.lean), names are not modelled, so a rename is the identity on the model and needs no new Step (plan I-13 is met as P1 met it for records). The engine's side is the property prop_rename_changes_no_figure (ledger-store tests/store.rs: every statement amount, entry and earlier journal line unchanged, live equals replay, the projection unchanged but accounts.name), and the stateful model tests/model.rs keeps a name per account so engine and model agree on every rename's refusal and nothing else moves.
    • Lean Step.record_changes_no_figure, Reachable.records (no axioms at all) · property settings_replay_is_pure · prop_rename_changes_no_figure · model Cmd::Rename · test decision_and_method_records_change_no_entry

Closing

16. A closing line zeroes its account, and a closing entry balances and zeroes every revenue and expense account through the period's last day, whether the net goes to one account or is split among members.
    • Kani closing_line_zeroes, credit_line_credits, closing_entry_balances
    • Lean closingEntry_net, closingEntry_zeroes, closingEntry_accepted, close_zeroes
17. A close credits equity with exactly the net income: revenue minus expenses through the period's last day.
    • Lean net_closings_is_net_income, close_credits_net_income
18. An allocation's parts sum to the whole, to the unit, however the other shares were rounded, and only the last share changes; and the largest-remainder apportionment (kernel::apportion, rules.md B-13) succeeds exactly when the rounded-down parts are short of the whole by less than a unit each, then sums to the whole, gives each part nothing or one unit (one part may also take the sub-unit fraction), and never gives a unit to a part while one with a strictly larger remainder goes without (no member favored by position).
    • Kani plug_last_sums_exactly, apportion_is_exact, apportion_is_fair · Lean plugLast_total, plugLast_keeps, Apportion.ranks_perm, Apportion.apportion_sum, Apportion.apportion_sum_of_shortfall (any number of parts)
19. A run of member closes telescopes: each member's total from a run of cumulative closes is their allocation of everything the run closed (so its rounding is one allocation's, never a sum of them), and each close hands out exactly its net, for any allocation whose parts sum to the whole (rules.md B-13). Since P3 this is the run rule closes journaled "cumulative" replay under (CloseTo::MembersRun).
    • Lean runPart_telescopes, closePart_total · property each_member_stays_within_a_cent_of_their_share

The P3 odd cent (defect 17; rules.md B-13; D-10, D-38) adds three laws:

20. A cumulative members close hands out exactly its net, and leaves each member's running total one allocation of everything the count closed, whatever rule the count's earlier closes were made under, as long as they handed out what they closed. The run rule is the special case where they gave exactly the allocation. A refusal leaves the parts as they were.
    • Kani apportion_cumulative_is_exact, cumulative_closing_entry_balances (the closing entry nets to zero whatever the true-up)
    • Lean trueUp_total, trueUp_running, closePart_eq_trueUp, Apportion.allocW_sum, Apportion.allocW_cumulative_total
    • properties apportion_cumulative_agrees, allocate_cumulative_agrees_with_the_integer_model
21. Bounded drift: no member's running total is ever a minor unit from their exact share. With shares w_i / W (exact decimals) and every amount a whole number of minor units (B-3), after every cumulative close |(given_i + part_i)·W − T·w_i| < W, whatever earlier closes gave. The precondition is the code's: periods::allocate_cumulative refuses a product Decimal would round, so the remainders it ranks are exact, and they sum to whole units (the Lean hypothesis of rem_pos_of_rank_lt).
    • Kani cumulative_close_never_drifts_a_unit_at_halves, cumulative_close_never_drifts_a_unit_at_tenths and cumulative_close_never_drifts_a_unit_at_near_thirds (two members at 50/50, three at 20/30/50%, three at 33.33/33.33/33.34%; every running total, net and earlier split to 2^12 units)
    • Lean Apportion.rem_pos_of_rank_lt (a member given a unit had a positive remainder), Apportion.apportion_drift (one apportionment is within a unit), Apportion.allocW_drift (the model of allocate_cumulative, gain or loss), cumulative_drift (any allocation within a unit stays so under the true-up), Apportion.allocW_cumulative_drift (the two together): any number of members, any amounts
    • property members_capital_never_drifts_a_cent_from_their_share
    • the tax-basis K-1's running split (B-36 with D-38, 2026-10-22), whose splits each carry their own weights, so the exact running share is a sum of quotients and Decimal's division can leave it a hair under the cent it is (tax_capital::RunningSplit takes it to ten places first): property a_running_split_never_drifts_a_cent (ledger-core/tests/tax_capital.rs, checked against the largest-remainder rounding of exact integer shares, and a loss against its gain); its kernel step is apportion_cumulative, proved above. The worksheet keeps one per set of members with a part in an entry, in date order whatever the span (tax_capital::entry_parts; tests a_member_outside_an_entry_never_takes_its_cents, an_entrys_odd_cent_is_the_same_in_every_span, the_split_runs_in_date_order)
22. A member's capital on a day never moves when its period is closed. The statement of members' equity gives each member, of the earnings not yet closed, what the count's next close would give them; closing moves those earnings into capital without changing the sum. When the count's earlier closes gave something else (closes under an earlier rule), the figure moves by exactly the true-up the close posts, never before.
    • Lean statement_after_close, statement_unmoved_by_close
    • property each_members_capital_chains_and_holds_through_closes; three_members_at_a_third_each_over_twelve_months (every day of a year, closed and never closed), the viewer's a_members_page_shows_the_same_capital_before_and_after_a_close

Parties

23. A party's part of an entry is signed as its own account would be, with a direction that is its sign: paid exactly when what counts is positive, received when negative, neither exactly when nothing counts; the money and property in it each carry the whole's sign and never exceed it; a money target is all cash; a contribution counts all of itself; a distribution counts no more money than it paid and no more property than it gave, the rest still owed (rules.md B-35).
    • Kani party_target_direction_is_its_sign · bridge party_target_agrees
24. A reversal is the exact opposite of what it reverses: the target is odd (negating the lines' capital movement, money and own-account movement gives the original's reverse, but for the debits fallback and a member's entry whose cash isn't exactly its money: an expense booked straight to capital, a debt converted, a distribution still owed; the engine never reads those off a reversal's lines: its reversal arm takes the original's target), reversing twice gives the original back, and a reversal's movement over any accounts is the original's negated (B-9).
    • Kani party_target_is_odd, reverse_target_is_an_involution · Lean partyTarget_odd, capitalTarget_odd (with cashIsMoney shown satisfiable), reverseTarget_involutive, sumOver_movement_reversal · property a_reversal_is_the_exact_opposite

1099 payments

25. A payment to a vendor is split, never lost or counted twice: each payment line goes in the bucket rules.md B-19's table names (its 16 cases: with no payment method naming its account, a financing line never counts and a card account's line is always a card's); the buckets are each exactly the credits minus debits of their lines; and netting money moved between the company's own sources keeps the total, leaves no bucket opposite it, and leaves buckets of one sign alone.
    • Kani payment_bucket_is_the_table, payment_split_is_exact, net_buckets_keeps_the_total · bridge payment_buckets_agree · test payment_bucket_is_the_table_in_all_16_cases · properties buckets_partition_each_payment, no_instruments_no_financing_is_the_old_report, a_reversal_nets_every_bucket_to_zero (ledger-core tests/form1099.rs)

Proration by days, catching up, truing up (P3, defects 22 and 9)

Depreciation (rules.md B-15) and daily prepaid and deferred-revenue schedules (B-16) spread a total over a span of days with one kernel function, kernel::prorate_by_days (each month's share through kernel::prorated_through), in exact integer arithmetic over a common unit, MONTH_L = lcm(28, 29, 30, 31) = 377,580 parts of a month, so a day of any month is a whole number of them.

26. The parts of a span sum to its total exactly, none is negative, and the last is the total less the others (plan/served.md P3 defect 9: "parts sum to the total; the last part absorbs the remainder"). Every split whose parts but the last fit in the span is computed; only parts no calendar has are refused.
    • Kani prorate_parts_sum_to_total, prorate_last_part_absorbs_the_remainder (a corollary, kept because the plan names the law) · Lean Prorate.kernel_parts_total, Prorate.kernel_parts_nonneg (the kernel's split, any number of parts and any sizes), Prorate.cum_dvd (a total in whole units is charged, so split, in whole units), from Prorate.prorate_total, Prorate.prorate_nonneg, Prorate.parts_telescope · bridge prorate_agrees_at_i64_and_i128
27. Each part but the last is its days times the monthly rate within one minor unit (P3 defect 9: "each part equals days × rate within 0.01", stated for any currency's minor unit). Each cumulative charge is its exact share rounded half up to a multiple of the unit (a tie goes up; the total itself when that rounds above it): Kani of the kernel at its bounds, Lean of both of the kernel's branches at any size (roundUnit_near, cum_near; chargeMid_eq_cum, chargeLast_eq_cum say the kernel's two formulas are the model's). Two such halves make the part's one unit (part_near, at any size, for any parts).
    • Kani a_months_charge_is_within_half_a_cent, a_months_charge_in_tenths_is_within_half_a_cent, the_last_months_charge_is_within_half_a_cent, the_last_months_charge_in_tenths_is_within_half_a_cent · Lean Prorate.roundUnit_near, Prorate.cum_near, Prorate.part_near, Prorate.part_within_a_unit · bridge prorated_through_agrees_at_i32_and_i128
28. The charge through a day never falls, never exceeds the total, is continuous where one month ends and the next begins, and is the total on the last day; malformed input (a negative total, no months, a unit that isn't positive, a part no month has, a day past the part, a weight outside the span) is refused, never a panic.
    • Lean Prorate.cum_mono, Prorate.cum_le, Prorate.cum_full (the model, any span), Prorate.chargeLast_mono and Prorate.chargeLast_start (the kernel's last month, by days, from where the month before ends: rounding is unchanged when an amount and its denominator are scaled together, Prorate.roundUnit_scale) · unit the_charge_never_falls_and_is_continuous_over_real_calendars (the kernel, exhaustively: every span of 1 to 3 months from every day of a common and a leap year, walked day by day, eight totals, both units) · Kani's four charge harnesses (bounded: never negative, never above the total, the total on the last day), prorated_through_refuses_malformed_input · property prop_depreciation_is_monotone_and_bounded (the engine)
29. A catch-up run never carries the books past the schedule at a month end already posted, and posts everything due through its month when no run comes after it (plan/served.md P3, settled in design: a month skipped is caught up in the month the run is made); every month's figure at once (catch_ups) is each suffix's catch-up. What the books carry at each month end is read entry by entry, each run and each reversal in its own month (assets::depreciation_effects), so the kernel's law is a law of the books' month ends, not of the runs' periods (a run reversed after its month ended is never run twice; a re-instated run never carries the books past the schedule).
    • Kani catch_up_never_overtakes_the_schedule, catch_ups_is_every_suffixs_catch_up · bridge catch_up_and_true_up_agree · unit catch_ups_is_every_suffixs_catch_up · property prop_run_amounts_are_each_months_run_amount · store a_run_reversed_after_its_month_is_caught_up_in_the_reversals_month, reinstating_a_run_a_later_run_caught_up_is_refused
30. A disposal's true-up reaches the schedule through its day from what the books carry, up or down, never both (true_up is columns of the gap).
    • Kani true_up_reaches_the_target · bridge catch_up_and_true_up_agree

Bounds (Kani): the split harnesses, at i64: up to 3 month parts, 1 to 3 months, each month 28 to 31 days with 1 to all of them in the span, totals to 2^16 units (they also passed at 2^20, 2026-10-20), a unit of 1 or 10. The charge harnesses, at i32 (the kernel is generic over Units; i32 so the solver can relate a product to a quotient): 1 or 2 months, any one month part and weight before it, totals to 2,048 units (a month but the last) or 64 (the last month, whose numerator carries the month's days), each unit in its own harness; the malformed-input harness: totals to 2^20 either sign, months 0 to 3, days, month lengths and k 0 to 40, a weight before of up to 4 × MONTH_L either sign, units -10 to 10; catch-up (and every suffix's) over up to 3 month ends, and the true-up, at amounts to 2^40.

What the solver could not do, and what carries it instead: a harness relating two symbolic divisions (a part against days × rate directly; a charge never falling within a month; the charge through a month's last day against the next month's through none of its days) ran past twenty minutes each, at 2^20 and again at 2^16, with CaDiCaL and with Kissat, and was stopped (2026-10-20); so did the one-division charge bound at i64 (a checked 64-bit product is a 128-bit multiplier to the solver). Each such relation is nonlinear in the divisor. So Kani proves the one-division fact at i32 (each charge within half a unit of its exact share: one to seven minutes a harness), the bridge ties the i32 kernel to the engine's i128 one, and Lean proves every one of these relations at any size, of the kernel's own two formulas: the model's charge is cum t unit V w (the total times w/V, rounded half up to a multiple of unit, capped at the total, and the total at w = V), and chargeMid/chargeLast are prorated_through's two branches written out, proved equal to cum over W = months × MONTH_L and over W × the last month's days, with the two meeting where the last month starts (roundUnit_scale). The one hypothesis is the calendar's: every part but the last ends short of the span (e < W), which a walk from any in-service date keeps (B-15: a first month of at most one, then whole months); an exhaustive test walks the kernel itself over every 1-to-3-month span of two calendar years, and the bridge and the exact unit tests check the rest.

An asset's basis figures (P3, defect 13)

The register's tax figures beside book value (rules.md B-25) come from one kernel function, kernel::basis_figures, for every rule:

31. Each figure follows from the rule and the facts, and none overflows: a purchase depreciates from its cost and has no §723 basis or built-in gain; a contribution's §723 basis is the member's adjusted basis and its built-in gain the value less it (a loss exactly when the basis exceeds the value); carryover property depreciates from the basis, personal-use property from the lesser of value and basis (at most each, equal to one). · Kani basis_figures_laws (every rule, costs, bases and values within the bounds) · bridge basis_figures_agree (the Decimal instantiation agrees, rule by rule) · property prop_basis_figures_laws

A project's unrecovered cost (P3, projects)

The "if repaid" figure of work done on spec (rules.md B-37 item 4) is one kernel function, kernel::unrecovered_cost:

32. Never below zero, the shortfall exactly, and no overflow: the result is at least zero; it is expenses less revenue when expenses are at least revenue, and zero otherwise; with revenue not negative it is never above the expenses or zero, whichever is larger (expenses can be negative: a reimbursement credited to the expense above its cost). · Kani unrecovered_cost_laws (every revenue and expense a line could carry) · ledger-core unrecovered_cost_only_for_on_spec_and_never_negative. No Lean model: the function is one subtraction and a max.

Payment terms and document lines (P4b S4.1)

Payment terms (rules.md B-39) give a due date and a discount date by calendar arithmetic in arap::Terms, and the two money figures they touch come from the kernel:

33. A discount never exceeds its stated percentage of the total, and a line's amount is exactly its quantity times its unit price. The bound is total × basis points / 10,000, exact: a result times 10,000 is the total times the basis points, and it is never above the total; when no whole amount can hold the exact bound, or a factor would overflow, the kernel refuses (None) rather than rounding. A line's amount is the exact product, never rounded, and None on overflow. Terms' own due dates (Net n, Net n EOM, due on receipt, custom; the 9999-12 bound) are checked by spec_documents.rs's terms_derive_due_dates, and the parser's round trip by terms_describe_and_parse_round_trip.
    • Kani discount_max_is_bounded (at i32, as the proration charge harnesses are: the law relates a product to a quotient) · line_amount_is_exact (at i64) · bridge discount_max_agrees, discount_max_i32_agrees_with_i64, line_amount_agrees · tests discount_bounds_and_late_reason, qty_times_price_must_equal_amount. No Lean model: these are two arithmetic laws, not a new Ledger command (S4.1 adds fields to the existing document commands).

What the proofs found

The engine already had 190+ tests, property tests, mutation testing, and 11.5M fuzz executions with zero crashes. Writing the laws down precisely still turned up three gaps in it, now closed:

• Negative line amounts were accepted. Only the MCP layer refused them. The engine now rejects them (NegativeAmountLine): direction is the side's job.
• A huge amount could crash the engine. Summing lines near Decimal::MAX panicked instead of returning an error. Lines are now limited to one quadrillion and ten decimal places (AmountOutOfRange), and the kernel's sums are checked.
• Foreign-currency conversion could crash the same way (foreign_amount * fx_rate). It is now a checked multiply.

And three things besides bugs:

• A soundness bug in the verifier. Kani reported a reversal that doesn't net to zero. Tracing it took a native replay of the counterexample (it passed) and a 15-line repro crate: Kani 0.68 mis-models symbolic-length slice copies. See "Trusting the checker" below. Taking every red result seriously is the method.
• Simpler code. credit_line and closing_line are the same function. The model made that obvious, and the code now says so.
• A load-bearing invariant, made explicit. No draft can exist in a closed period (Inv.draftsOpen). That is why the store can journal a post before applying it: the closed-period check can never fail after the journal write. It was true by accident of the checks' design. Now it is a theorem, and breaking it breaks the build.

Each of these shipped past every test we had. That is the case for formal methods here: tests sample, proofs exhaust. AGENTS.md makes growing this coverage part of every change.

Trusting the checker

A model checker is a program too. While building these proofs, Kani reported that an entry plus its reversal could leave an account nonzero. That was not a bookkeeping bug. Kani's own counterexample passes when replayed natively. We narrowed it to a 15-line crate with no wanderbooks code: Kani 0.68 (CBMC 6.11) mis-models copy_from_slice whenever the length is symbolic. It is the known bug model-checking/kani#4904, closed as a duplicate and unfixed in 0.68. It is unsound in both directions: it can also prove false claims. So:

• No harness copies a slice of symbolic length. They write element by element (reversal_cancels says why), and the kernel functions under proof contain no bulk copies.
• A canary watches for the fix. kani_symbolic_copy_canary runs the faulty copy and is marked should_panic. When a Kani upgrade fixes the bug, the canary starts failing, and the workaround can go.
• The proofs are not vacuous. kani::cover! statements make Kani show that the interesting cases are reachable: an accepted four-line entry, a reversal on one account with several lines, three distinct accounts, a balanced three-account chart, a close to two members, a part-cash part-noncash investing entry, cash settling two sections at once, a mixed entry reversed, property contributed for capital; a split of three parts, a half-unit tie rounding up, a charge capped at a total finer than its unit, a catch-up across three month ends and distinct ones for every suffix, a true-up each way. just prove fails if any cover is unsatisfiable.

What is and isn't proved

Be precise about the claims:

• Kani is bounded. It proves the kernel for every input up to 4 lines over 3 accounts and amounts to 2^40 units (the accounting equation end to end: up to 3 accounts; the cash flow entry harnesses: up to 3 lines, each tagged any of 4 ways), and the proration by days within the bounds above. Lean proves the laws for any size, but of a model. The model is a direct restatement of the kernel (for proration, its two formulas written out and proved equal to the model's charge), and the bridge property tests tie the Decimal (and i128) instantiation to the i64 (and i32) one Kani checked.
• Decimal itself is trusted. rust_decimal is exact for these sizes: 96-bit integers scaled by a power of ten. With lines capped at one quadrillion and ten decimal places, every sum is exact while the total of all amounts stays below 7.9 × 10^18. Kani can't explore Decimal arithmetic directly: a single symbolic add runs for more than ten minutes.
• The state machine is a model of Ledger's checks, not a proof about ledger.rs line by line. Its correspondence to the code is checked by review and by the end-to-end property tests in tests/properties.rs (trial balance, balance sheet, reversals, immutability) and the golden files.
• Out of scope: currency (the ledger is single-currency, enforced structurally), A/R and A/P documents, payroll, the calendar walk around the proration kernel (calendar::month_parts, assets::depreciation_schedule, schedules::daily_plan: property tests, tests/properties.rs, P3), and persistence (the journal store's hash chain is tested in ledger-store).
• The cash flow model tags lines per entry with any function meeting the engine's guarantees (the cash tag follows the account; revenue and expense lines are operating or investing; a reversal takes its original's tags); which tag the engine picks for a line (rule 4's disposals, the bill split, the chain root) is checked by the property and example tests, not proved. A line the engine splits between two sections is two lines in the model, the entry's net unchanged.
• Closing entries and the cash balance. The engine leaves closing entries out of the sections but not out of the cash accounts' balances; the two agree because a close moves only revenue, expense and equity (Ledger::validate_close_to) and cash accounts must be assets (rules.md B-14 rule 2). The Lean model's close step lets a target be any balance-sheet account, so Reachable.cashflow_foots takes any selection of entries with the cash over the same selection, and Reachable.cashflow_is_change_in_cash counts every entry, closes included. That a close never moves cash is checked by tests (closing_entries_never_appear, prop_cash_flow_laws law 7), not proved.

P0 guard rails (2026-10-16)

P0 (plan/served.md) added no kernel arithmetic and no new law about balances, so it added no Kani harness and no Lean theorem; nothing here was weakened. What it added is checked by tests and properties (listed in docs/testing.md, "P0 guard rails"): the journal format gate (newer is never called corrupt, damage always is; the envelope and its hash are frozen across formats, rules.md B-27), the server failing closed after a panic, the import roots' lockdown (a property over generated paths, and a component walk that refuses a folder swapped for a link; removed with the import roots in P2 slice 5), files with full TINs kept out of the books (B-26), and the agent text lint. Out of scope for proof today: the format gate and the walk are I/O, and the model in verify/lean stops at the ledger.

P3: the odd cent (2026-10-20)

The cumulative members close (rules.md B-13) adds a kernel function, kernel::apportion_cumulative, which Kani proves exact and refusal-safe for up to three parts and checks against the integer model of periods::allocate_cumulative for bounded drift; Lean proves the drift bound and the true-up laws for any number of members and any amounts. Not proved: the regime query (Ledger::members_regime: which closes count), the Decimal exactness check in allocate_cumulative, and the journal's since_seq. They are checked by the tests in ledger-core tests/odd_cent.rs, ledger-store tests/member_closes.rs and the old-books fixture x_member_closes (docs/testing.md, "P3: odd cents"). Kani times, each harness alone on a busy laptop (Kani 0.68, 2026-10-20): apportion_cumulative_is_exact 257 s, cumulative_close_never_drifts_a_unit_at_halves 17 s, cumulative_close_never_drifts_a_unit_at_tenths 320 s, cumulative_close_never_drifts_a_unit_at_near_thirds 449 s, cumulative_closing_entry_balances 202 s (apportion_is_exact, for scale: 121 s). Two shapes were too slow and were changed, not weakened in what they prove: restating apportion's postconditions on the cumulative parts directly ran past ten minutes, so apportion_cumulative_is_exact proves the parts are apportion's less given on the same inputs (the solver shares the two runs' formulas) and apportion_is_exact supplies the rest; and the drift bound with symbolic weights ran past ten minutes, so it is checked at three fixed sets of shares (the brief's fallback), Lean carrying any weights.

Running it

mise install   # once: Kani, Lean, and the rest, pinned in mise.toml
just prove       # 48 Kani harnesses and Lean
just prove-slow  # the other 8: the justfile's kani_slow
just prove-all   # both

just prove runs every Kani harness but the justfile's kani_slow, in parallel (-j $(nproc)), the whole run under a 30-minute timeout; builds the Lean proofs (seconds); and fails if any headline theorem depends on anything beyond Lean's standard axioms (propext, Quot.sound, Classical.choice). In particular, sorryAx fails it. just prove-slow runs the slow harnesses, $(nproc) at a time, each under its own 30-minute timeout. Both fail if a harness they ask for isn't verified (the count is checked), if any cover is unsatisfiable (a vacuous proof), or if kani_slow names a harness src/proofs.rs doesn't have; a new harness runs in prove until it is listed as slow. CI's weekly run does both, on two runners (.github/workflows/scheduled.yml). Kani downloads its pinned nightly and CBMC into ~/.kani on first use.

Why the split (2026-10-21, the P3 surface review). With all of P3 the suite is 55 harnesses. One just prove at four jobs (a CI runner's cores), on the development laptop under heavy load from other work (a load average near 30 on 16 cores, the run held to 12), could not finish inside its 30 minutes: 52 of the 53 harnesses of the time were verified, all of them proved, and the last, entry_flows_of_a_reversal_mirror at three lines, was still running; alone, under the same load, it passed 30 minutes too. A run is only as safe as its slowest harness under the machine it gets, so: that harness's claim at three lines is now proved in two halves (entry_movements_of_a_reversal_mirror, flows_of_mirrors; law 10) that take a minute or two each, and the end-to-end harness runs at two lines; the eight harnesses that take the longest run in just prove-slow, each capped on its own. Nothing was dropped.

Measured, four jobs: under that load, just prove 1,450 s (48 harnesses then) and just prove-slow 1,365 s (seven then; entry_flows_sum_to_cash 1,228 s); on the same laptop quiet (2026-10-22, the final configuration), just prove 308 s (47 harnesses, about 19 minutes of CPU, and Lean's 83 headline theorems) and just prove-slow 467 s (8 harnesses, the slowest entry_flows_sum_to_cash at 301 s).

P4b S4.1's two harnesses were measured on 2026-10-26 (a busy machine); the rest are the 2026-10-22 run. discount_max_is_bounded's 163 s is Kani's verification time (it runs in prove-slow).

Every harness, the law it proves, the recipe that runs it, and its time in that quiet run (prove: each harness's verification time; prove-slow: each harness's whole run, its compile of about 50 s included):

Harness	Law	Recipe	Seconds
flip_negates	5	prove	0
sums_are_exact	4	prove-slow	82
check_lines_is_exact	1	prove	7
out_of_range_is_rejected	1	prove	0
accepted_entry_nets_to_zero	2	prove	15
movements_are_per_account	3	prove	12
movements_sum_to_the_net	3	prove	58
reversal_mirrors	5	prove	25
reversal_cancels	5	prove	69
normal_balance_is_signed	8	prove	0
accounting_equation	8	prove-slow	176
normal_side_increases	6	prove	0
trial_balance_columns	7	prove	62
closing_line_zeroes	16	prove	0
credit_line_credits	16	prove	0
closing_entry_balances	16	prove	11
payment_bucket_is_the_table	25	prove	0
payment_split_is_exact	25	prove	18
net_buckets_keeps_the_total	25	prove	5
plug_last_sums_exactly	18	prove	4
apportion_is_exact	18	prove	56
apportion_is_fair	18	prove	18
apportion_cumulative_is_exact	20	prove	44
cumulative_close_never_drifts_a_unit_at_halves	21	prove	11
cumulative_close_never_drifts_a_unit_at_tenths	21	prove	149
cumulative_close_never_drifts_a_unit_at_near_thirds	21	prove-slow	216
cumulative_closing_entry_balances	20	prove-slow	150
take_is_odd_and_bounded	10	prove	1
apply_cash_mirrors	10	prove	12
entry_flows_sum_to_cash	10	prove-slow	301
entry_flows_pure_are_movements	10	prove-slow	151
entry_flows_are_bounded	10	prove	20
entry_flows_of_a_reversal_mirror	10	prove	36
entry_movements_of_a_reversal_mirror	10	prove	30
flows_of_mirrors	10	prove	56
no_cash_no_flow	10	prove	75
apply_cash_spends_exactly	10	prove	36
exchanged_is_bounded	10	prove	0
constructive_nets_to_zero	10	prove	26
constructive_mirrors	10	prove	52
party_target_direction_is_its_sign	23	prove	2
party_target_is_odd	24	prove	5
reverse_target_is_an_involution	24	prove	0
prorate_parts_sum_to_total	26	prove-slow	222
prorate_last_part_absorbs_the_remainder	26	prove	33
a_months_charge_is_within_half_a_cent	27	prove	48
a_months_charge_in_tenths_is_within_half_a_cent	27	prove	42
the_last_months_charge_is_within_half_a_cent	27	prove-slow	148
the_last_months_charge_in_tenths_is_within_half_a_cent	27	prove	36
prorated_through_refuses_malformed_input	28	prove	7
catch_up_never_overtakes_the_schedule	29	prove	8
catch_ups_is_every_suffixs_catch_up	29	prove	35
true_up_reaches_the_target	30	prove	0
basis_figures_laws	31	prove	0
unrecovered_cost_laws	32	prove	0
discount_max_is_bounded	33	prove-slow	163
line_amount_is_exact	33	prove	6
kani_symbolic_copy_canary	(the checker: "Trusting the checker")	prove	3

P6: the evidence pipeline

No kernel arithmetic, Ledger command in the formal sense, or Lean step changed (P6 moves no money): just prove is unchanged and stays green. The new Ledger methods (annotate_attachment, set_entry_settles) are replay-side records with validation only, covered by annotations_replay_and_project and reimbursed_is_derived_from_settles_only; the arithmetic-shaped work (the extraction caps and the page scale) is in ledger-import, outside the kernel, and is tested and fuzzed rather than proved. The formal bar for the next unit that touches these paths is unchanged; the P12 paragraph in docs/testing.md lists the mutation targets.