The escrow contract's correctness has so far been established by manual CLI testing and a handful of unit tests — real, but not exhaustive. Formally verify that no sequence of lock/release/refund calls, in any order, from any caller, can ever violate the contract's core invariants (funds can't be released without a valid secret; funds can't be double-spent; funds can't be permanently stuck once a timeout passes).
Acceptance criteria: A formal model of the contract's state machine (using a tool appropriate to the task — TLA+, a symbolic execution framework, or equivalent); a machine-checked proof (or a documented, high-confidence bounded model-check) that the stated invariants hold; any invariant violation found is reported as a critical finding, not silently fixed without disclosure.
Why this is hard: this isn't testing — it's proving an absence of bugs across the entire state space, which requires genuine formal methods background, not just Rust/Soroban familiarity.
The escrow contract's correctness has so far been established by manual CLI testing and a handful of unit tests — real, but not exhaustive. Formally verify that no sequence of lock/release/refund calls, in any order, from any caller, can ever violate the contract's core invariants (funds can't be released without a valid secret; funds can't be double-spent; funds can't be permanently stuck once a timeout passes).
Acceptance criteria: A formal model of the contract's state machine (using a tool appropriate to the task — TLA+, a symbolic execution framework, or equivalent); a machine-checked proof (or a documented, high-confidence bounded model-check) that the stated invariants hold; any invariant violation found is reported as a critical finding, not silently fixed without disclosure.
Why this is hard: this isn't testing — it's proving an absence of bugs across the entire state space, which requires genuine formal methods background, not just Rust/Soroban familiarity.