Verification

bivium-protocol-lean4 holds Lean 4 models of the series ledger, machine-checked proofs about them, and a harness that replays the same operation streams through the model and through the real Solidity and compares every field.

Those are three different artifacts making three different claims, and the value is in how they chain — and in the gap they leave, which the repository states rather than papers over.

Three artifacts, three claims

Chained, they give: the model has property P (proved) plus the Solidity agrees with the model wherever we looked (tested) ⟹ evidence that the Solidity has P on that domain. Not proof.

The gap is exactly the domain nobody generated, and it is the harness's own Domain and limitations section — not an unstated assumption. That is the honest shape of this kind of work: the proofs make the model trustworthy, the harness makes the model relevant, and neither on its own says the contract is correct.

The models

Standalone Lean 4 (pinned to 4.14.0 by lean-toolchain), namespace BiviumProtocol, standard library only — no Mathlib, and no dependency on the older bivium-lean4 or any legacy credit/debt model.

Organised by subject rather than by Solidity file: Series (dynamic shares, holder checkpoints, pre-expiry A traces, fixed-epoch B bounds), Settlement (frozen-A redemption and its rounding), Session and SessionLifecycle (the flash-accounting session, receipt and count invariants, committed physical solvency, rollback), FeeLedger, GlobalLedger (multi-holder B potential across all lifecycle transitions) and CoreAdmission, each with a companion module of executable regressions.

CoreAdmission is the one to understand structurally: it checks exactly two admission conditions — the mint cutoff (the MIN_A_PER_SHARE price floor, computed at Core's WAD scale, not the accumulator's) and lazy creation — and then delegates all accounting arithmetic to Global.step. The broader ledger model is left unchanged, and the layer's theorems are about the projection.

What the proofs claim, and what they do not

These are proofs about explicit mathematical models, not Solidity/EVM equivalence and not a security certificate.

That sentence is the repository's own, repeated here rather than softened. Applying a theorem to the Solidity requires the call to succeed, divisors to be positive, every stored value and result to be in uint256 range, and no underflow — the models use unbounded Nat, and Nat subtraction does not model Solidity's reverting subtraction, so transition guards and theorem hypotheses have to supply those bounds.

Explicitly outside the arithmetic proofs: fees in the aggregate trace, token balance mismatches, reentrancy, controllers, external callbacks, approvals, transaction rollback, gas, and timestamp validation. Exact-transfer ERC-20 behaviour is an environmental assumption. The nested model is one-level parent-long custody accounting, not recursive look-through solvency.

The README carries a theorem-to-source map: every theorem, the Solidity operation it corresponds to, and the scope and assumptions attached to it. Read a theorem's row before citing it.

The negative results are load-bearing

Two proofs establish that something is not true, and they are more useful than most of the positive ones because they pre-empt a reasonable but wrong assumption:

• individual_order_counterexample — pool = 1, shares = 2: the first one-share redemption gets 0 and the second gets 1. Aggregate order-independence does not imply individual fairness or MEV resistance.
• positive_B_dust — at the real ACC_SCALE of 10^36, three one-share holders and one unit of B input: all three receive zero and one B remains in the series. There is no zero-dust claim.

Neither is a bug. Each is a property of integer division that a reader would otherwise discover the hard way.

The conformance harness

conformance/ replays generated operation streams through both sides and compares them field by field. Three suites, each with its own model, corpus, runner and results file:

Why the comparison is worth anything

A differential test is only as good as its inability to agree with itself, and the design is built around that:

• The corpus generates inputs only. It calculates no expected accounting. Neither side is handed an answer, so the suite cannot be satisfied by two implementations agreeing with a hand-written expectation.
• Python compares and never reimplements ledger arithmetic. It enforces the output schema and checks every field, so there is no third implementation to accidentally agree with.
• The Solidity side is the real Core — actual unlock, actual debt, actual ERC-20 settlement. The observer adds only read-only access to a few internals and overrides no state-changing method; counters come from actual token balance movements, not from model formulas.
• Mutation controls corrupt the accumulator, checkpoint, status, creation and cashflow fields to confirm each is rejected, and unit tests catch both traces being truncated or both omitting required fields. The comparison is itself tested.
• Guard witnesses assert exact Core custom-error bytes without providing expected state to either oracle, and every rejected attempt additionally requires unchanged state and zero flows.
• No expected-divergence exemption. Earlier divergence probes were converted into ordinary all-fields-equal cases rather than kept as known exceptions.
• Python is rejected under -O, because optimized execution could strip the validation gates. The report is written only after every check passes, and a stale report is removed before a run.

What is compared is not a summary: status and action identity, locked A, nominal longs, frozen and live supply, the B accumulator, redeemed shares, the lazy created flag, every holder's short balance, checkpoint, stored claimable B and previewCollect, the cumulative counters, and the Core's actual ERC-20 balances with per-attempt inflows and outflows.

Its domain, stated up front

One plain ERC-20-backed series at a time, standard exact-transfer tokens, a permissionless controller, known holders, centralised long custody, successful session settlement, exercise from zero, mint and exercise ending together. Values deliberately include fractional strike ratios, rounding dust, and mulDiv intermediate products exceeding 256 bits while results stay in range.

Not validated: nested collateral, multiple series sharing assets, permission policies, arbitrary individual long ownership, recipients' individual balances, callback and reentrancy attacks, incomplete settlement, all window combinations, uint256 overflow bounds, gas, or the option and lending integration. Passing finite traces establishes correspondence for the tested domain.

The axiom gate

python3 scripts/check_axioms.py inspects every named theorem against AxiomAudit.lean and rejects incomplete output, sorryAx, or any axiom beyond Lean's standard propext, Classical.choice and Quot.sound. A proof cannot quietly become an assumption.

Adding a model file means registering it in check_axioms.py and extending the root imports and audit entries, so a new file cannot skip the gate. CI runs lake build, the Python unit tests and the gate on every push and pull request.

The source pins, and their drift

The repository pins the exact revisions it modelled, and for the Core that pin is mechanically enforced: conformance/solidity/vendor/protocol/ holds byte-identical Core.sol and ICore.sol from the pinned commit, with a source.json recording SHA-256 and Git blob hashes that the runner checks before replaying anything. Vendoring those two files is also what lets CI run without a cross-private-repository token. As the harness puts it, a matching hash is a version check, not proof that future Core changes correspond.

As of 2026-10-03:

The contrast is instructive. The Core pin has a harness that will refuse to run if the vendored source stops matching, so it can only fall behind — visibly. The hedge pin has no such harness, and it is the one that drifted: the hedge responsibility now sits in bivium-lending's HedgeDesk, so those proofs describe a design that was reorganised after they were written. Whether the pinned branch is still in flight or the model should be re-pointed is a question for whoever owns that work, not something to infer from the pin.

The general rule holds both ways: a pin does not imply coverage of later revisions, and a theorem about a function that has since moved is evidence about the old location until it is re-extracted. See Integration for where this sits among the stack's other drift surfaces.