Kani + proptest, not Halmos, for formal verification

Context

Earlier drafts cited "Halmos" for the 5-invariant CI. The Halmos README confirms it is EVM/Solidity-only.

Decision

Kani for Rust pure-function invariants; proptest for contract-level state behavior.

Alternatives

Certora (rejected: expensive, mainnet only). Manticore (rejected: Solidity bytecode focus). Coq/Lean proofs (rejected: too heavy for the team).

Consequences

Atrium publishes its Kani harnesses publicly. Honest signal: this was a lesson in not citing tools without verifying capability.