docs: RFC 001 — formal verification of ICS23

[zmanian]

Summary

This PR began as an RFC proposing a formal verification program for the ICS23 verifier and now carries the verification itself: a mechanized Lean 4 model of the verifier with machine-checked soundness theorems, Kani panic/overflow harnesses, an executable model with concrete SHA-256, and a set of findings surfaced by the work.

The verifier is the security boundary of IBC state verification: every byte of a CommitmentProof is attacker-controlled, and a soundness bug means forgeable state proofs across IBC. The hand-written verification core is small, purely functional, and has a crisp cryptographic correctness statement — an unusually good target for formal methods.

What is proved (Lean 4, no Mathlib, ~3,800 lines)

All soundness results conclude by constructively exhibiting a hash collision — there are no axioms about the hash functions. The only cryptographic assumption that remains is FixedHash (a fixed-width digest), and even joint leaf injectivity is now a theorem rather than an assumption.

• Theorem A — existence binding. Two accepted existence proofs for the same key under the same root agree on the value, up to a collision. Proved byte-level (existence_binding_shaped, production-spec shape) and, in the honest-root tree model, as genuine membership in the real tree with no positional-ambiguity arm (membership_sound / membership_sound_tendermint).
• Theorem B — non-existence soundness. A non-existence proof and an existence proof for the same key cannot both verify without a collision, proved in the honest-root tree model for the two-sided neighbor case (nonexistence_sound_tree / nonexistence_sound_tree_tendermint). The chain: membership_sound makes the absent key a genuine member; ensureLeftNeighbor_spec + neighbor_divergence pin the bracketing proofs to a divergence node N; node_gap_no_member shows no member can sit between maxKey N.left and minKey N.right in a sorted tree.
• Joint leaf injectivity, discharged from the encoding. Previously a hypothesis (hLInj), now proved for every shipped spec: leafInj_varProto (IAVL/Tendermint, via varint self-delimiting) and leafInj_noPrefix (SMT, via the fixed-32-byte digest split). The reduction is exactly "encoding framing + collision resistance."
• Implementation safety. Six Kani harnesses (cfg(kani)-gated) over the arithmetic and slice-indexing in the verifier internals — the Dragonberry-class surface — including the i32 prefix bounds, padding offsets, left/right empty-branch slice bounds, and compressed-batch index handling.
• Executable model. A runnable Lean model with concrete SHA-256 (Sha256.lean, Executable.lean) and a regression corpus, with the non-existence verifier exercised end-to-end on a real tree.

One acknowledged sorry remains, by design: the abstract-root nonexistence_sound. It is not provable as stated — an opaque root carries no tree structure linking byte-order to position (findings F3/F4) — which is exactly why the genuine result is the honest-root nonexistence_sound_tree, mirroring how Theorem A's real deliverable is honest-root membership_sound. CI guards the sorry count at exactly one.

Findings surfaced by the work

• F1 — i32 prefix-bound overflow in ensure_inner under an adversarial spec with an enormous child_size. Not reachable with the shipped specs; a Kani harness pins the safe precondition.
• F2 — ternary-spec suffix slice panic. The right empty-branch check guards a single child_size suffix but indexes multiple siblings; latent for any spec with child_order.len() > 2. No shipped store is ternary.
• F3 — positional ambiguity. A node preimage is accepted by ensure_inner under both a left-child and a right-child reading. Binding against an arbitrary hash therefore rests on preimage resistance, not just collision resistance. Machine-checked that the IAVL ensure_inner_prefix (height/size/version) does not disambiguate it. The honest-root tree model resolves this structurally via split_pins: the verifier's suffix % child_size check pins a node split to exactly the two genuine children.
• F4 — non-existence soundness requires the store key-sortedness invariant. The verifier links key order to position adjacency but never checks that positions track key order, so soundness is conditional on a store invariant the verifier does not enforce. The Lean theorem makes this precise by carrying a SortedTree hypothesis.
• F5 — adjacency is hash-structural, not pure lex. "No leaf position strictly between the neighbors" holds only because the left neighbor's leaf is terminal — a fact about the tree's hash structure, reducing to the leaf/inner domain-separation collision, not derivable from the lexicographic order alone.

Repo layout

• docs/rfc/001-formal-verification.md — the RFC.
• docs/verification/properties.md — properties, findings, and a traceability matrix.
• lean/ — the Lean 4 Lake project; lake build checks every proof, and CI runs it.
• rust/src/kani_proofs.rs — the Kani harnesses.

Approach and alternatives

Model-first: a mechanized Lean model of the verifier with machine-checked soundness theorems, intended to connect to both shipped implementations via a differential oracle, with Kani harnesses and fuzz targets on the Rust crate, and an optional refinement proof of ics23-rs (hax / coq-of-rust) as a stretch goal. Alternatives considered (Verus/Creusot, TLA+/Quint, F* end-to-end, more auditing) are discussed and rejected with reasoning in the RFC.

Discussion wanted

The RFC ends with open questions for maintainers — Lean 4 vs. Rocq, whether the refinement proof is in scope, batch proof sequencing, and whether the model should live in this repo or a sibling.

🤖 Generated with Claude Code

[greptile-apps]

PR author is not in the allowed authors list.