What is proven, what is assumed, and exactly where the gap between the two lives. Mechanized in Lean 4 — sorry-free, no mathlib, every cryptographic assumption labeled.
The full tables are below. This is the three-sentence version.
If someone shows you coins, the math — not a server, not trust — proves every unit traces back to a mint the issuer actually signed. If that's ever wrong, the world has a counterfeiting machine, and the mints stream would show it.
Spending the same coin twice produces a visible conflict that resolves deterministically — the first properly anchored spend wins, and a recipient who waits for confirmations can't be fooled into taking the loser. Copying someone's anchor to grief them provably does nothing.
A wallet that follows the verification checklist accepts only coins with a genuine, unbroken history. The checklist is short enough to be verified itself — that's what the theorems below are.
Every proof rests on assumptions. We don't hide them — each is named, and each failure mode is visible rather than silent.
| You trust that… | If it breaks… | Mitigation |
|---|---|---|
| Poseidon2 hashes are collision-resistant | counterfeiting becomes possible | conservative parameters; swap hash without protocol change |
| The FRI proof system is sound | fake validity proofs could pass | transparent setup; audits re-check proofs publicly |
| The issuer keeps its mint key safe | inflation — but visible, never hidden | public mint stream; key rotation cuts off rogue mints |
| At least one of N indexers is honest | a double-spend could be hidden from you | cross-check independent indexers; zero-trust self-scan per receipt |
| Bitcoin isn't reorged past k confirmations | accepted payments can be undone | same assumption as any Bitcoin payment |
Four headline results about the protocol logic — the layer where catastrophic bugs (inflation, double-spend acceptance) would live, independent of any cryptography.
Along any valid trace, per asset: net value in circulation equals
Σ mints − Σ redeems, and every mint carries a valid issuer
signature. Nobody prints money — not the users, not a forger, and not the
issuer beyond its own signed, publicly anchored mints. Paper §5.1.
Every transfer step preserves per-asset totals: outputs sum to inputs, so shielded transfers can neither create nor destroy value — which is what makes the public mint/redeem stream an exact audit of supply. Paper §4.5.
One coin yields exactly one nullifier, so a double-spend is an
observable conflict to anyone holding nf (owner and
consignment recipients), and the first occurrence resolves it
deterministically: two recipients cannot both finally accept. On-chain
payloads are context-bound (P = H(nf, ctx)), and both grief
directions are theorems: a copied record under a different context
is provably invisible (griefer_copy_invisible), and an
adversary who doesn't know nf can forge no occurrence at all
(no_occurrence_without_knowledge). Paper §5.2, §4.7.
The receiver's Accept checklist (verify proof, check anchor,
check no earlier occurrence, check ownership) succeeds only on transactions
that extend a valid trace — recipients can't be fooled into accepting
counterfeit coins, modulo proof-system soundness. Paper §4.8, §5.1.
Every assumption is an explicitly labeled axiom — the build
prints an axiom audit (#print axioms) per theorem. Nothing is
hidden in the proof tactics.
| Assumption | Form | Used by |
|---|---|---|
assetId_injective | collision resistance of the genesis hash | asset binding |
commitHash_injective | binding of coin commitments | coin identity |
ownerKey_injective | collision resistance of owner = H(osk) | T3 |
sig_unforgeable | EUF-CMA of the issuer scheme, abstractly | T1 |
ProofSystem.sound | soundness of Π, as a structure field | T4 |
bindHash_injective | collision resistance of the anchor payload H(nf, ctx) in both arguments | T3 (conflict soundness) |
occurrence_requires_knowledge | preimage resistance: a fresh well-formed entry implies knowledge of nf | T3 (anti-grief) |
Notable by absence: the first-occurrence lemmas are pure list reasoning and depend on no cryptographic axioms at all.
Regenerated weekly by CI from axiom-audit.txt in
opencsv-formal — this block can never drift from the actual proofs.
| Theorem | Axiom dependencies |
|---|---|
OpenCsv.Batch.batch_commit_unique | propext, Classical.choice, OpenCsv.bindHash, OpenCsv.bindHash_injective, Quot.sound |
OpenCsv.Batch.batch_exclusion_sound | propext, OpenCsv.bindHash, Quot.sound |
OpenCsv.Batch.batch_occurrence_iff | OpenCsv.bindHash |
OpenCsv.Batch.chainOccurrence_expandWindow | propext, OpenCsv.bindHash, Quot.sound |
OpenCsv.Batch.coordinator_cannot_forge | OpenCsv.KnowsRawNf, OpenCsv.bindHash, OpenCsv.occurrence_requires_knowledge |
OpenCsv.Batch.coordinator_envelope_no_occurrence | OpenCsv.KnowsRawNf, OpenCsv.bindHash, OpenCsv.occurrence_requires_knowledge |
OpenCsv.Scan.anchor_bearing_is_candidate | propext, Quot.sound |
OpenCsv.Scan.filter_absence_trustless | propext, Quot.sound |
OpenCsv.Scan.filter_no_false_negatives | propext, Quot.sound |
OpenCsv.Scan.marker_zero_authority | OpenCsv.bindHash |
OpenCsv.Scan.scan_exclusion_sound | propext, OpenCsv.bindHash, Quot.sound |
OpenCsv.Scan.served_list_falsifiable | propext, Classical.choice, Quot.sound |
OpenCsv.Value.carry_complete_single | propext, Quot.sound |
OpenCsv.Value.carry_sound | propext, Classical.choice, Quot.sound |
OpenCsv.Value.difference_interval_within_half_field | none |
OpenCsv.Value.no_wrap | propext, Quot.sound |
OpenCsv.Value.range_checked_represents_exactly | propext, Quot.sound |
OpenCsv.accepted_trace_supply | propext, OpenCsv.Sig, OpenCsv.SigVerify, OpenCsv.assetId, OpenCsv.bindHash, OpenCsv.commitHash, OpenCsv.nullHash, OpenCsv.ownerKey, Quot.sound |
OpenCsv.copied_record_not_wellformed | OpenCsv.bindHash, OpenCsv.bindHash_injective |
OpenCsv.double_spend_conflict | OpenCsv.bindHash, OpenCsv.commitHash, OpenCsv.nullHash, OpenCsv.ownerKey, OpenCsv.ownerKey_injective |
OpenCsv.griefer_copy_invisible | propext, OpenCsv.bindHash, OpenCsv.bindHash_injective |
OpenCsv.inflation_soundness | propext, OpenCsv.Sig, OpenCsv.SigVerify, OpenCsv.assetId, OpenCsv.commitHash, OpenCsv.nullHash, OpenCsv.ownerKey, Quot.sound |
OpenCsv.later_occurrence_rejected | OpenCsv.bindHash |
OpenCsv.mints_authorized | propext, OpenCsv.Sig, OpenCsv.SigVerify, OpenCsv.SignedByIssuer, OpenCsv.assetId, OpenCsv.commitHash, OpenCsv.nullHash, OpenCsv.ownerKey, OpenCsv.sig_unforgeable |
OpenCsv.no_occurrence_without_knowledge | OpenCsv.KnowsRawNf, OpenCsv.bindHash, OpenCsv.occurrence_requires_knowledge |
OpenCsv.payload_binds_one_nullifier | OpenCsv.bindHash, OpenCsv.bindHash_injective |
OpenCsv.receiver_correctness | propext, OpenCsv.Sig, OpenCsv.SigVerify, OpenCsv.assetId, OpenCsv.bindHash, OpenCsv.commitHash, OpenCsv.nullHash, OpenCsv.ownerKey |
OpenCsv.transfer_conservation | propext, OpenCsv.Sig, OpenCsv.SigVerify, OpenCsv.assetId, OpenCsv.commitHash, OpenCsv.nullHash, OpenCsv.ownerKey, Quot.sound |
OpenCsv.unknowing_adversary_entry_invisible | propext, OpenCsv.KnowsRawNf, OpenCsv.bindHash, OpenCsv.occurrence_requires_knowledge |
29 theorems, audited 2026-08-02 from axiom-audit.txt @ 2b42286
regenerated 2026-08-02 01:34 UTC · build green · opencsv-formal@2b42286
"Formally verified" always means less than it sounds. Here is precisely what it means here — three layers, stated plainly.
Poseidon2's collision resistance, the signature scheme's unforgeability, and FRI's soundness enter as axioms. Mechanizing them is research-grade work (and, for FRI, an active area elsewhere), not something this project claims.
As of 2026-08-02 the correspondence is machine-checked for the
kernel: formal-aeneas
translates opencsv-kernel (binding, occurrence test,
first-occurrence, supply audit) from Rust into Lean 4 and proves it
equal to this specification — sorry-free, audited. Two honest
remainders: (a) coverage — the trait-heavy accept() driver,
scan engine, and chain backends are not yet translated, and (b)
adoption — production still runs the original core code
(equivalence-tested against the kernel), until Track A4 swaps the
verified kernel in as the shipped implementation.
The deployment moved to scan-first indexing (paper §4.7.1): exclusion
is a local check over a filter-discovered candidate set, verified
against proof-of-work. The formal model now matches the deployment
(OpenCsv.Scan): scan-first exclusion is proven as sound as
full-block scanning, so the old "at least one honest indexer" hypothesis
is eliminated from the default path — indexers are optional,
spot-verifiable accelerators whose fraud is provably publishable.
The off-circuit Ed25519 issuer signature and test-grade FRI parameters are prototype deviations, documented in both repos. The formalization models the paper's target design, not the shortcuts.
Tracked as opencsv-formal#1. One item already shipped; item 1 converts our scariest informal argument into a theorem.
Every headline theorem's #print axioms output is
normalized into a checked-in baseline; CI fails if any assumption set
changes without a human regenerating it in the same commit. The honesty
table on this page is an enforced invariant, not a claim.
The u64 conservation gadget's carry argument (24/24/16-bit limbs, field equality ⟺ integer equality) is mechanized (b036cf3) — wrap-around cannot fake balance. Honest bonus: the general converse is false (completeness, not soundness) — documented.
OpenCsv.Scan
(00edaed):
no-false-negatives of filter discovery, scan-exclusion soundness
(scan-first ≡ full-block scanning), marker zero-authority, accelerator
fraud-provability. The N-of-M honesty hypothesis is eliminated — the
architecture got better, so the assumptions got fewer.
Make the Lean model executable, generate random valid/invalid traces,
and run them against the Rust accept() driver — catches drift
between the verified model and the implementation empirically.
The kernel (opencsv-kernel) is already proved equal to
this specification in formal-aeneas. The remaining step is adoption:
opencsv-core and the FFI call the verified kernel as the production
implementation, and the accept() decision driver gets its own pure
kernel (the big design item, A5). "The model is the code" by
verification-and-adoption, not by extraction.
Upgrade the state machine from linear traces to the tree structure of the real recursion, matching the paper's §5.1 induction.
Rather than verifying hand-written AIR constraints after the fact: define predicates in a Lean-embedded DSL, prove the translation sound once, generate circuits. Every future predicate inherits the proof.