Quint formal verification for Evolve modules

## Summary

Integrate [Quint](https://quint-lang.org/) 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:

```quint
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](https://github.com/informalsystems/quint) (npm / standalone binary) -- spec language + simulator
- [quint-connect](https://quint-lang.org/docs/model-based-testing) (Rust crate) -- MBT framework
- [itf-rs](https://github.com/informalsystems/itf-rs) (Rust crate) -- ITF trace deserialization
- [Apalache](https://github.com/apalache-mc/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](https://github.com/informalsystems/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](https://quint-lang.org/docs/lang)
- [Quint Model-Based Testing](https://quint-lang.org/docs/model-based-testing)
- [Quint Connect + Emerald Case Study](https://quint-lang.org/posts/quint_connect_emerald)
- [ChonkyBFT Specification](https://protocols-made-fun.com/consensus/matterlabs/quint/specification/modelchecking/2024/07/29/chonkybft.html)
- [Malachite Consensus Engine](https://github.com/informalsystems/malachite)
- [RVCase25 Paper (Quint for Design and Testing)](https://seanmk.com/rvcase/RVCase25_paper_5.pdf)
- [cosmwasm-to-quint (reverse: Rust -> Quint stubs)](https://github.com/informalsystems/cosmwasm-to-quint)