intrepidshape/elm-web3 3.0.0 · elm-web3-ui 3.0.0

What is actually proved

Most libraries tell you they are correct. This one shows you the machine output. Every claim below is graded by what a checker actually did — not by what a document says — and CI re-runs every checker on every change.

Four checkers, one honest ledger

A claim earns its grade from the strongest machine that has actually verified it. A Lean proof that does not compile is not a proof; a TLA+ property absent from the model-checker's config was never checked; a test that never ran is a comment. The grades, strongest first:

Each checker runs in CI on every pull request. The ledger records only what they report.

The fourth checker is the gallery: every state machine rendered, clicked, and redeployed on each release. Formal tools verify what a claim says; a pixel verifies what a user gets — the stack needs both, so we run both.

The coverage, counted

Every invariant in the ledger, bucketed by the strongest verification it has actually received. No bucket borrows from a stronger one — an open obligation stays in its own row until the checker closes it.

Lean and fuzz counts as of 2026-07-02: all ten Lean proof files check clean on the pinned toolchain and the corpus is sorry-free — every stated theorem is proved. The TLC row was recounted 2026-07-27, when WalletSpec.tla was rewritten against the 2.0.0 wallet: the five new rows are the request-id properties that machine did not have before. The chart moves only when a checker's exit code does.

The state machines, drawn from the specs

Four state machines run every dapp built on this stack. Each diagram below is drawn from its TLA+ specification, and every labelled invariant is one that TLC verified over the full reachable state space of the model. The same guards exist in the Elm code — the conformance audit maps every update branch to its spec action, one to one.

Wallet WalletSpec.tla · Web3.Wallet

TLC verified: Connected/WrongChain always carry an address and chain · a session always returns to a resting state (Disconnected or ReadOnly) · Connected exits only to WrongChain, Disconnected, or Error · ReadOnly exits only via a wallet announcement · while an attempt is in flight, a response naming any other request id leaves the machine completely unchanged · a rejection, failure or timeout only ever resolves the request it names · re-entering Connecting only ever installs a strictly newer id. The ✓ edge means a user who switches chains by hand in the wallet UI recovers instantly — no app round-trip required. Connecting id carries the request id that makes the last three properties statable: clicking Connect again supersedes the attempt in flight instead of being swallowed, and the superseded attempt can no longer clobber the new one.

Transaction TransactionSpec.tla · Web3.Transaction

TLC verified: no port message moves a terminal state · Submitted is reachable only from AwaitingSignature · Confirming always carries a valid hash · the confirmation count strictly increases · every pending transaction eventually terminates. The n′ > n guard drops stale or reordered port messages on the floor — the counter can only move forward. Failure edges drawn once for legibility; every non-terminal state has one.

Sign SignSpec.tla · Web3.Sign

TLC verified: terminal states absorb · every terminal state was entered from SignPending · a response for a different correlation id never completes the pending signature. Run the spec's UnguardedSpec and TLC shows that last property breaking — the id guard is load-bearing, not decorative.

ApprovalFlow ApprovalSpec.tla · Web3.Ui.ApprovalFlow

TLC verified: Acting is unreachable without a verified allowance · Completed comes only from a confirmed action and absorbs · a confirmed approval re-reads the chain rather than trusting itself (tokens lie; the chain doesn't). The same invariants hold under fuzzing in ApprovalFlowTest. Failure edges to Blocked omitted for legibility — every in-flight state has one.

How the grades stay true

Every row in the coverage ledger is backed by a command you can run yourself — lean on the proof files, check-tla.sh on the specs, elm-test on the properties — and CI re-runs all of them on every pull request, so a claim cannot outlive the thing it claims.

The rules are strict by design: a proof that doesn't compile counts for nothing; a spec property absent from the model-checker's config was never checked; and when a checker and a claim disagree, the claim changes — graded down the same hour, promoted back only when the checker says so. The gallery is the fourth checker: every state machine rendered and clickable, because a pixel is the one reviewer that never extends good faith.