Formal verification: let's start with the challenge protocol and see

Motivation

The economic security of the system rests on one claim: an honest provider is never slashed, and a provider that lost data cannot escape slashing. This claim depends on interleavings of extrinsics, deadlines, and on_finalize sweeps — exactly the class of bugs unit tests are weakest at, and model checkers are built for. Quint (Informal Systems' TLA+ successor) lets us specify the challenge state machine, check invariants exhaustively over small instances, and later replay generated traces against the real pallet.

Current state

• The challenge flow was recently overhauled (#125) and now has three entry points (challenge_checkpoint, challenge_offchain, challenge_replica), a single respond_to_challenge with four response variants, and a timeout path in on_finalize (pallet/src/impls/challenges.rs).
• Challenges are deadline-bucketed via ChallengeId { deadline, index } with a MaxChallengesPerDeadline cap (primitives/src/lib.rs).
• Four slash reasons exist (Timeout, InvalidProof, InvalidDeletionClaim, InvalidSupersededClaim) — each represents a known escape hatch that was closed manually; nothing systematically searches for the next one.
• Test coverage is example-based (pallet/src/tests/); no formal spec of the protocol exists anywhere in the repo.

Proposed solution

Add a Quint spec specs/quint/challenges.qnt modeling the challenge lifecycle as a state machine:

• State: providers (stake, ghost flag hasData), one bucket, open challenges by deadline, balances. Crypto is abstracted — "proof verifies" becomes a nondeterministic boolean tied to the ghost flag; MMR/Merkle internals stay out of scope.
• Actions: the three challenge extrinsics, respond_to_challenge (all four variants), and advanceBlock modeling the on_finalize timeout sweep.
• Invariants:
  • honestNeverSlashed — a provider with the data that responds before the deadline is never slashed.
  • challengeResolvesOnce — no challenge is both defended and timed out.
  • dishonestAlwaysSlashable — a provider without the data has no move sequence (respond Deleted, claim Superseded, stall, deregister) that keeps full stake.
  • depositConservation — challenger deposits are always either refunded or accounted for, never leaked.

Small instances (2 providers, ~3-block timeout) are sufficient — the bugs this finds are logical, not scale-dependent. Checked via quint run (simulation) and quint verify (bounded model checking / Apalache), wired into CI.

Follow-up (out of scope here): extend the spec to funds conservation across agreements/checkpoints, provider deregistration vs. open challenges, and ITF trace replay against the pallet mock as a model-based test.

TODO

• specs/quint/challenges.qnt — state, actions, invariants above
• quint run + quint verify passing on a small instance
• CI job running the spec
• Document any invariant violations found as separate issues

Related issues

• #125 — challenge flow overhaul (the protocol being specified)
• #44 — production readiness