Formal methods

Protocol rules: proven.
Whole wallet: no.

OpenCSV machine-checks the rules that prevent inflation, value creation, and quiet double spends. It does not pretend that Lean has proved Bitcoin, Poseidon2, the AIR prover, storage, networking, or application software.

72Lean specification declarations
audited separately

15Aeneas translated-Rust refinements
narrow kernel only

0Tracked sorry or admit
enforced by CI

6+Runtime and cryptographic surfaces
not mechanized

01 / COVERAGE

Coverage by layer

Select a layer to see its exact status, proof boundary, pinned source, and receipt.

Machine-checked

The protocol state machine and its load-bearing invariants.

Seventy-two separately audited declarations cover genesis→mint→transfer→redeem, supply, conservation, first occurrence, receiver acceptance, value arithmetic, scan exclusion, batching, one-input forwarding, and recursive lineage. The project is dependency-free Lean 4 and CI rejects sorry, admit, or axiom drift.

Open the evidence

SPECIFICATION @ dc7e8eb ↗T1–T4 SOURCE ↗72-DECLARATION AXIOM AUDIT ↗GREEN DEFAULT-BRANCH CI ↗

Narrow direct refinement

Four families of pure Rust decisions are connected to Lean.

Aeneas translates the pure opencsv-kernel implementation and proves binding, well-formed occurrence, first occurrence, and supply audit refine their specifications. Fifteen declarations support that bridge. Proof verification, chain I/O, storage, concurrency, and the account registry are outside it.

Open the evidence

AENEAS PROJECT @ 3bcafed ↗BINDING + WELL-FORMED REFINEMENT ↗FIRST-OCCURRENCE REFINEMENT ↗SUPPLY REFINEMENT ↗GREEN REPRODUCIBILITY CI ↗

External security boundary

Bitcoin supplies ordering and probabilistic settlement.

Lean proves scan-first exclusion relative to a verified ordered chain view. Rust validates proof-of-work headers, BIP158 candidates, Merkle inclusion, confirmations, and reorgs. The security of Bitcoin consensus, sufficient honest hashpower, network availability, and the meaning of k confirmations remain external assumptions.

Open the evidence

SCAN SOUNDNESS SOURCE ↗BITCOIN WHITEPAPER ↗BIP158 COMPACT FILTERS ↗OPENCSV CHAIN VERIFIER ↗SCAN-SOUNDNESS FILM ↗

02 / EXTERNAL FOUNDATIONS

External assumptions

The protocol theorems depend on these named security assumptions, which are not mechanized.

Assumed cryptographic security

Poseidon2

Provides commitment, owner/nullifier, anchor-binding, and proof-system hashing. Lean reasons from injectivity, binding, and preimage-resistance hypotheses; it does not mechanize cryptanalysis of the concrete permutation.

POSEIDON2 PAPER ↗
LEAN HASH AXIOMS ↗

Assumed proof-system soundness

FRI + recursion

The receiver theorem calls an abstract sound proof system. FRI parameters, predecessor-key binding, version boundaries, and adversarial rejection are implemented and tested; Lean does not prove the concrete verifier. D5 remains open: the v4 root key is self-described by proof common data and is not independently authenticated, so v4 cannot activate mainnet.

PINNED PROVER SOURCE ↗
D5 ROOT-KEY GATE ↗
PAPER BOUNDARY ↗

External consensus security

Bitcoin

Orders anchors and gives confirmations. OpenCSV verifies its local view and proves scan semantics, but assumes Bitcoin's proof-of-work security and a chosen confirmation depth against reorganizations.

BITCOIN SECURITY MODEL ↗
SCAN MODEL ↗

Operational key boundary

Issuer authority

The theorem proves that accepted mint lineage carries issuer authorization. It cannot protect an issuer seed that is stolen, misused, or backed up incorrectly. Inflation would be public, not impossible.

MINT AUTHORIZATION THEOREMS ↗
TEST USD ISSUER DISCLOSURE ↗

03 / THREE LOAD-BEARING CLAIMS

The three main guarantees

The full ledgers are below. These are the three claims a receiver needs.

Proven: no inflation without issuer authorization.
Every accepted unit traces back to a mint the issuer authorized (T1). A violation would appear in the public mints stream, which anyone can audit.
Proven: a double-spend can't quietly succeed.
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 cannot accept the loser (T3). Copying someone's anchor record under a different context creates no occurrence (griefer_copy_invisible).
Proven: the checklist protects the receiver.
A wallet that follows the Accept checklist accepts only coins that extend a valid trace (T4), modulo proof-system soundness.

04 / FAILURE-MODE TABLE

Assumptions and failure modes

Each assumption is listed with what breaks if it fails and the mitigation.

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 seed safe	inflation — but visible, never hidden	public mint stream; explicit asset migration/rotation
Your verified Bitcoin header/filter/block view is current	a spend or reorg could be missed	multi-peer proof-of-work validation; explorers are hints only
Bitcoin isn't reorged past k confirmations	accepted payments can be undone	same assumption as any Bitcoin payment

05 / HEADLINE THEOREMS

Headline theorems

Four results about the protocol logic — the layer where catastrophic bugs (inflation, double-spend acceptance) would live, independent of any cryptography. Each links to its Lean source and paper section; each video is from the same generated formal series.

T1Inflation soundness

Along any valid trace, per asset: net value in circulation equals Σ mints − Σ redeems, and every mint carries valid issuer authorization. Nobody prints money — not the users, not a forger, and not the issuer beyond its own signed, publicly anchored mints. Paper §5.1.

LEAN SOURCE ↗PAPER §5.1 ↗AXIOM LEDGER ↓

T2Conservation

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.

LEAN SOURCE ↗LIMB ARITHMETIC ↗AXIOM LEDGER ↓

T3Nullifier uniqueness & first occurrence

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.

LEAN SOURCE ↗SCAN MODEL ↗AXIOM LEDGER ↓

T4Receiver correctness

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.

LEAN SOURCE ↗RECEIVER CHECKLIST ↗AXIOM LEDGER ↓

06 / MACHINE-GENERATED LEDGERS

Axiom ledger

Every assumption is an explicitly labeled axiom; the build prints an axiom audit (#print axioms) per theorem.

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`	unforgeability of the abstract issuer authorization; v3 refines this with in-circuit seed knowledge	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)

The first-occurrence lemmas are pure list reasoning and depend on no cryptographic axioms. The scan-soundness argument has a short animated explainer: Scan-soundness film.

Specification audit — live from the build

The site checks opencsv-formal every 15 minutes. When its default branch moves, CI rebuilds Lean, reruns the axiom audit, and regenerates this block before publishing. An event hook can refresh it immediately, and a weekly forced rebuild remains as a backstop.

72 / 72 visible

72-declaration specification ledger

Theorem	Axiom dependencies
`OpenCsv.Batch.allocated_charge_base`	`propext`
`OpenCsv.Batch.allocated_charge_high`	`propext`
`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.batch_v2_exclusion_sound`	`propext`, `OpenCsv.bindHash`, `Quot.sound`
`OpenCsv.Batch.batch_v2_occurrence_iff`	`OpenCsv.bindHash`
`OpenCsv.Batch.c1_two_party_initial_valid`	`propext`, `Quot.sound`
`OpenCsv.Batch.c1_two_party_replacement_conforms`	`propext`, `Quot.sound`
`OpenCsv.Batch.c1_two_party_replacement_valid`	`propext`, `Quot.sound`
`OpenCsv.Batch.canonical_adjacent_swap_rejected`	`propext`
`OpenCsv.Batch.chainOccurrence_expandWindow`	`propext`, `OpenCsv.bindHash`, `Quot.sound`
`OpenCsv.Batch.chainOccurrence_expandWindow_v2`	`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.Batch.manifest_c1_guards`	none
`OpenCsv.Batch.manifest_fixed_positions`	`propext`, `OpenCsv.bindHash`
`OpenCsv.Batch.manifest_participant_alignment`	`propext`, `OpenCsv.bindHash`
`OpenCsv.Batch.manifest_value_conservation`	`propext`, `Quot.sound`
`OpenCsv.Batch.manifest_vector_lengths`	`propext`, `OpenCsv.bindHash`
`OpenCsv.Batch.max_signed_weight_at_cap`	none
`OpenCsv.Batch.participant_funding_conservation`	`propext`, `Quot.sound`
`OpenCsv.Batch.proposal_id_unique`	`propext`, `OpenCsv.bindHash`, `OpenCsv.bindHash_injective`
`OpenCsv.Batch.replacement_monotone`	none
`OpenCsv.Batch.replacement_preserves_header`	`OpenCsv.bindHash`
`OpenCsv.Batch.replacement_preserves_marker`	none
`OpenCsv.Batch.replacement_preserves_stock`	none
`OpenCsv.Batch.replacement_requires_unanimity`	none
`OpenCsv.Batch.signer_receipt_fresh`	none
`OpenCsv.Batch.versioned_commit_no_fallback`	`propext`, `OpenCsv.bindHash`, `OpenCsv.bindHash_injective`
`OpenCsv.Batch.versioned_commit_unique`	`propext`, `Classical.choice`, `OpenCsv.bindHash`, `OpenCsv.bindHash_injective`, `Quot.sound`
`OpenCsv.EdgesMatch.lengths`	`propext`, `OpenCsv.Sig`, `Quot.sound`
`OpenCsv.Encoding.canonical_digest_injective`	`Quot.sound`
`OpenCsv.Encoding.canonical_limb_unique`	none
`OpenCsv.Encoding.decode_limb_accepts_canonical`	none
`OpenCsv.Encoding.decode_limb_rejects_noncanonical`	none
`OpenCsv.Encoding.modular_reduction_has_noncanonical_twins`	`propext`
`OpenCsv.Exec.run_sound`	`propext`, `OpenCsv.Sig`, `OpenCsv.SigVerify`, `OpenCsv.assetId`, `OpenCsv.commitHash`, `OpenCsv.nullHash`, `OpenCsv.ownerKey`, `Quot.sound`
`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.legacy_redeem_lineage_impossible`	`propext`, `OpenCsv.Sig`, `OpenCsv.SigVerify`, `OpenCsv.assetId`, `OpenCsv.commitHash`, `OpenCsv.nullHash`, `OpenCsv.ownerKey`, `Quot.sound`
`OpenCsv.legacy_transfer_lineage_impossible`	`propext`, `OpenCsv.Sig`, `OpenCsv.SigVerify`, `OpenCsv.assetId`, `OpenCsv.commitHash`, `OpenCsv.nullHash`, `OpenCsv.ownerKey`
`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.one_input_forwarding_anchor_exact`	`OpenCsv.Sig`, `OpenCsv.bindHash`
`OpenCsv.one_input_forwarding_conservation`	`propext`, `OpenCsv.Sig`, `OpenCsv.SigVerify`, `OpenCsv.assetId`, `OpenCsv.commitHash`, `OpenCsv.nullHash`, `OpenCsv.ownerKey`, `Quot.sound`
`OpenCsv.one_input_forwarding_pool_unchanged`	`propext`, `OpenCsv.Sig`, `OpenCsv.SigVerify`, `OpenCsv.assetId`, `OpenCsv.commitHash`, `OpenCsv.nullHash`, `OpenCsv.ownerKey`, `Quot.sound`
`OpenCsv.one_input_forwarding_valid_iff`	`propext`, `OpenCsv.Sig`, `OpenCsv.SigVerify`, `OpenCsv.assetId`, `OpenCsv.commitHash`, `OpenCsv.nullHash`, `OpenCsv.ownerKey`, `Quot.sound`
`OpenCsv.one_input_forwarding_value_equation`	`propext`, `OpenCsv.Sig`, `OpenCsv.SigVerify`, `OpenCsv.assetId`, `OpenCsv.commitHash`, `OpenCsv.nullHash`, `OpenCsv.ownerKey`, `Quot.sound`
`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.transfer_lineage_conservation`	`OpenCsv.Sig`, `OpenCsv.SigVerify`, `OpenCsv.assetId`, `OpenCsv.commitHash`, `OpenCsv.nullHash`, `OpenCsv.ownerKey`
`OpenCsv.transfer_lineage_current`	`OpenCsv.Sig`, `OpenCsv.SigVerify`, `OpenCsv.assetId`, `OpenCsv.commitHash`, `OpenCsv.nullHash`, `OpenCsv.ownerKey`
`OpenCsv.transfer_lineage_edges_match`	`OpenCsv.Sig`, `OpenCsv.SigVerify`, `OpenCsv.assetId`, `OpenCsv.commitHash`, `OpenCsv.nullHash`, `OpenCsv.ownerKey`
`OpenCsv.transfer_lineage_inputs_nodup`	`OpenCsv.Sig`, `OpenCsv.SigVerify`, `OpenCsv.assetId`, `OpenCsv.commitHash`, `OpenCsv.nullHash`, `OpenCsv.ownerKey`
`OpenCsv.transfer_lineage_nullifiers_nodup`	`OpenCsv.Sig`, `OpenCsv.SigVerify`, `OpenCsv.assetId`, `OpenCsv.commitHash`, `OpenCsv.nullHash`, `OpenCsv.ownerKey`
`OpenCsv.transfer_lineage_predecessors_valid`	`OpenCsv.Sig`, `OpenCsv.SigVerify`, `OpenCsv.assetId`, `OpenCsv.commitHash`, `OpenCsv.nullHash`, `OpenCsv.ownerKey`
`OpenCsv.two_input_lineage_distinct`	`propext`, `OpenCsv.Sig`, `OpenCsv.SigVerify`, `OpenCsv.assetId`, `OpenCsv.commitHash`, `OpenCsv.nullHash`, `OpenCsv.ownerKey`
`OpenCsv.unknowing_adversary_entry_invisible`	`propext`, `OpenCsv.KnowsRawNf`, `OpenCsv.bindHash`, `OpenCsv.occurrence_requires_knowledge`
`OpenCsv.v4_one_input_lineage_valid_iff`	`propext`, `OpenCsv.Sig`, `OpenCsv.SigVerify`, `OpenCsv.assetId`, `OpenCsv.commitHash`, `OpenCsv.nullHash`, `OpenCsv.ownerKey`
`OpenCsv.v4_one_input_slots_distinct`	`OpenCsv.commitHash`
`OpenCsv.v4_one_input_statement_exact`	`propext`, `OpenCsv.commitHash`

78 theorems, audited 2026-08-16 from axiom-audit.txt @ 4fa63a3

regenerated 2026-09-15 10:24 UTC · build green · opencsv-formal@4fa63a3

Translated Rust audit — merged reproducibility receipt

A separate audit of the Aeneas-translated opencsv-kernel. These 15 declarations do not inflate the 72 specification-theorem count above. The exact green commit was fast-forwarded without rewriting history and is now the default formal-aeneas branch.

15-declaration translated-Rust refinement ledger

Rust refinement declaration	Axiom dependencies
`opencsv_kernel.array_eq_decide_spec`	`propext`, `Classical.choice`, `Quot.sound`
`opencsv_kernel.audit_equation`	`propext`, `Classical.choice`, `Quot.sound`
`opencsv_kernel.binding_eq_spec`	`propext`, `Classical.choice`, `Quot.sound`, `hash.hash_bind`
`opencsv_kernel.first_occurrence_iff_isFirstOccurrence`	`propext`, `Classical.choice`, `Quot.sound`, `hash.hash_bind`
`opencsv_kernel.first_occurrence_none_no_occurrence`	`propext`, `Classical.choice`, `Quot.sound`, `hash.hash_bind`
`opencsv_kernel.first_occurrence_spec`	`propext`, `Classical.choice`, `Quot.sound`, `hash.hash_bind`
`opencsv_kernel.specFirstOccList_bridge`	`propext`, `Classical.choice`, `Quot.sound`
`opencsv_kernel.specFirstOccList_none`	`propext`, `Classical.choice`, `Quot.sound`
`opencsv_kernel.supply_fold_split`	`propext`, `Classical.choice`, `Quot.sound`
`opencsv_kernel.supply_loop_spec`	`propext`, `Classical.choice`, `Quot.sound`, `I128.Insts.CoreConvertFromU64.from`
`opencsv_kernel.supply_spec`	`propext`, `Classical.choice`, `Quot.sound`, `I128.Insts.CoreConvertFromU64.from`
`opencsv_kernel.truncate24_loop_spec`	`propext`, `Classical.choice`, `Quot.sound`
`opencsv_kernel.truncate24_spec`	`propext`, `Classical.choice`, `Quot.sound`
`opencsv_kernel.well_formed_pure_spec`	`propext`, `Classical.choice`, `Quot.sound`, `hash.hash_bind`
`opencsv_kernel.well_formed_spec`	`propext`, `Classical.choice`, `Quot.sound`, `hash.hash_bind`

15 audited declarations · green hosted run 30765043746 · formal-aeneas@3bcafed

07 / GAPS

Known gaps

These surfaces are outside the machine-checked claim.

1. The cryptography is assumed, not proven.
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.
2. The model/code gap is closed only for the pure kernel.
As of 2026-08-03 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 and audited. The remaining coverage boundary is large: proof verification, scan orchestration, storage, concurrency, and chain I/O are not translated. A4 adopts the four verified families on opencsv-rs/main; A5 projects receiver decisions through a pure accept boundary on that same line.
3. The chain-view assumption is explicit.
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.
4. D5: the recursive root key is not yet independently authenticated.
Legacy off-circuit Ed25519 records and the two-query/no-grinding FRI profile are inspectable but cannot create or verify v3 proofs. V3 binds issuer-seed knowledge and predecessor keys in-circuit and enforces its 94-bit floor. But D4 authenticates predecessor keys only inside their successors; v4 still rebuilds the root verifier from proof-carried common data. A static tag is not enough. Mainnet writes fail closed until a canonical v5 root policy and adversarial custom-root regression pass independent review.
5. Crash safety and runtime orchestration are tested, not proved.
The durable operation journal, SQLite transactions, attachment delivery, backup, notifications, memory ownership, and concurrency are validated by adversarial and end-to-end tests. They are not included in the 72 or 15 declaration ledgers.

08 / RELATED PAGES

This page covers only what is proved. Delivery status and throughput are documented on their own receipt-backed pages.

Delivery

Protocol rules: proven.
Whole wallet: no.

Coverage by layer

The protocol state machine and its load-bearing invariants.

The model now includes the recursive tree and batch semantics.

Four families of pure Rust decisions are connected to Lean.

The circuit shape is pinned; the AIR implementation is not mechanized.

Bitcoin supplies ordering and probabilistic settlement.

External assumptions

Poseidon2

FRI + recursion

Bitcoin

Issuer authority

The three main guarantees

Assumptions and failure modes

Headline theorems

T1Inflation soundness

T2Conservation

T3Nullifier uniqueness & first occurrence

T4Receiver correctness

Axiom ledger

Specification audit — live from the build

Translated Rust audit — merged reproducibility receipt

Known gaps

Related pages

Roadmap

Bitcoin performance

Paper