Quint formal verification for Evolve modules

Inizia esaminando l’attuale implementazione Rust di x/token e l’infrastruttura esistente di crates/testing, quindi esamina la disposizione proposta di specs/ e crates/testing/quint-mbt/. Risolvi le questioni aperte relative all’ambito e a CI prima di implementare la specifica Quint, l’integrazione di Driver e la pipeline di trace. Il lavoro è completato quando è definito un ambito iniziale con controlli del modello e test di conformità superati, e sono documentati i comandi just quint-verify e just quint-test.

Summary

Integrate Quint formal verification into the Evolve SDK to enable formally specified, model-checked, and conformance-tested modules. Quint specs would serve as the canonical source of truth for module behavior, with model-based testing (MBT) ensuring Rust implementations conform to their specifications.

Background

Quint is an executable specification language built by Informal Systems, semantically based on TLA+ but with a modern typed syntax. It has a proven track record in blockchain projects:

• Malachite (Tendermint BFT in Rust) -- spec-first development, MBT conformance testing
• ChonkyBFT (zkSync consensus) -- model checking found missing validation bugs before deployment
• Cosmos Interchain Security -- TLA+ specs rewritten in Quint for MBT
• Tendermint Light Client -- 6 lines of TLA+ generated 500+ lines of integration test vectors
• Neutron DEX -- MBT caught a production bug before deployment
• Alpenglow (Solana) -- full Votor consensus specification

Quint's mode system (pure def, action, temporal) maps naturally to Evolve's account model (#[query], #[exec], invariants).

Proposed Architecture

Quint Specs as Module Specifications

Each Evolve module gets a corresponding .qnt spec that defines:

• State variables mapping to storage collections (Item, Map, Vector)
• Actions mapping to #[exec] methods
• Pure defs mapping to #[query] methods
• Invariants (safety properties verified by model checker)
• Temporal properties (liveness, fairness)

Example for a token module:

module Token {
    type Addr = str

    var balances: Addr -> int
    var totalSupply: int
    var allowances: (Addr, Addr) -> int

    action init: bool = all {
        balances' = Map(),
        totalSupply' = 0,
        allowances' = Map(),
    }

    action transfer(from: Addr, to: Addr, amount: int): bool = all {
        require(amount > 0),
        require(balances.getOrElse(from, 0) >= amount),
        balances' = balances
            .setBy(from, old => old - amount)
            .setBy(to, old => old.getOrElse(0) + amount),
        totalSupply' = totalSupply,
        allowances' = allowances,
    }

    // Invariants
    val noNegativeBalances: bool =
        balances.keys().forall(a => balances.get(a) >= 0)

    val supplyConserved: bool =
        totalSupply == balances.keys().fold(0, (sum, a) => sum + balances.get(a))

    // Step for simulation
    action step: bool = {
        nondet sender = ACCOUNTS.oneOf()
        nondet receiver = ACCOUNTS.oneOf()
        nondet amount = 1.to(MAX_AMOUNT).oneOf()
        any {
            transfer(sender, receiver, amount),
            approve(sender, receiver, amount),
            transferFrom(sender, receiver, sender, amount),
        }
    }
}

MBT Pipeline

┌─────────────────┐     ┌──────────────┐     ┌─────────────────┐
│  Quint Spec      │────>│ quint run    │────>│ ITF JSON Traces │
│  (.qnt files)    │     │ --mbt        │     │                 │
└─────────────────┘     └──────────────┘     └────────┬────────┘
                                                       │
        ┌──────────────────────────────────────────────┘
        v
┌─────────────────┐     ┌──────────────────┐
│ quint-connect /  │────>│ Evolve TestApp   │
│ itf-rs (Rust)    │     │ conformance test │
└─────────────────┘     └──────────────────┘

1. Spec -- Write Quint specs alongside Rust modules in a specs/ directory
2. Verify -- quint verify runs Apalache model checker against invariants
3. Generate -- quint run --mbt --n-traces=N produces ITF trace files
4. Conform -- Rust test driver (using quint-connect crate) replays traces against TestApp, asserting implementation state matches spec state after each step

Integration with Evolve Test Infrastructure

The conformance test driver would implement quint-connect's Driver trait, mapping:

Quint Action	Evolve Operation
init	Genesis setup via TestApp::new()
transfer(from, to, amount)	Submit signed Transfer tx to STF
approve(owner, spender, amount)	Submit signed Approve tx to STF
State assertions	Query STF state, compare to spec snapshot

Repository Structure

/specs/
├── README.md              # How to write and run Quint specs
├── token.qnt              # Token module spec
├── scheduler.qnt          # Scheduler module spec
├── stf.qnt                # STF-level properties (block validity, tx ordering)
└── common.qnt             # Shared types, helpers

/crates/testing/
├── quint-mbt/             # New crate: Quint MBT test driver for Evolve
│   ├── Cargo.toml         # deps: quint-connect, itf-rs, evolve-testing
│   └── src/
│       ├── lib.rs         # Driver trait impl, state mapping
│       └── drivers/       # Per-module drivers
└── ...

Tasks

• Add specs/ directory with initial Quint spec for the token module (x/token)
• Set up quint CLI in CI (npm package, or pin binary)
• Write Quint spec for x/token matching current Rust implementation
• Model check token spec invariants with quint verify
• Create quint-mbt testing crate with quint-connect integration
• Implement Driver trait mapping ITF actions to TestApp operations
• Generate trace suite and add to cargo test pipeline
• Add just quint-verify and just quint-test commands to justfile
• Write Quint spec for STF-level properties (block building, tx validation)
• Document spec-writing patterns for Evolve module authors

Key Dependencies

• quint (npm / standalone binary) -- spec language + simulator
• quint-connect (Rust crate) -- MBT framework
• itf-rs (Rust crate) -- ITF trace deserialization
• Apalache (JVM) -- symbolic model checker (auto-downloaded by quint verify)

Open Questions

1. Scope: Start with x/token only, or also spec the STF and mempool?
2. CI integration: Run quint verify on every PR (slow, JVM-based) or only on spec changes?
3. Trace caching: Pre-generate and commit ITF traces, or generate fresh in CI?
4. LLM-assisted spec writing: Use quint-llm-kit to bootstrap specs from existing Rust code?
5. Code generation direction: Long-term, explore building a Quint-to-Evolve codegen (no prior art exists, significant effort) or stay with the MBT conformance pattern?

References

• Quint Language Docs
• Quint Model-Based Testing
• Quint Connect + Emerald Case Study
• ChonkyBFT Specification
• Malachite Consensus Engine
• RVCase25 Paper (Quint for Design and Testing)
• cosmwasm-to-quint (reverse: Rust -> Quint stubs)