[High] Write a formal Quint (or TLA+) specification of the intent state machine and check conformance

[james2177]

Description:
Specify the intent lifecycle, solver bonding, slashing, escrow, and disputes in Quint. Model-check safety properties (no double payout, bond never negative, no stuck funds) and liveness properties (every intent eventually reaches a terminal state). Then add a conformance test that replays traces from the model against the real contract.

Problem Statement & Context:
The state machine now has 11 states and more than 20 transitions spread across 5,000 lines. A formal model is the only way to reason about it with confidence, and it's a strong signal to auditors.

Scope & Acceptance Criteria:

• spec/vortex.qnt covering every IntentState transition documented in the README diagram.
• At least 6 safety invariants and 2 liveness properties, checked with Apalache or the Quint simulator.
• A trace-conformance harness: Rust tests consume ITF traces exported by Quint and replay them.
• Document each property in plain English.
• Out of scope: cross-chain proof semantics (abstracted as an oracle).

Implementation Guidelines:

1. Key Files/Modules: new spec/, intent_settlement/tests/conformance.rs, docs/formal-spec.md.
2. Design/Architecture: Abstract amounts to small domains, and model time as discrete ticks.
3. Edge Cases/Constraints: State explosion (bound the actors to 2 users and 2 solvers).
4. Testing: The model checker passes, and the conformance replay passes.

Definition of "Done":

• Spec, doc, and conformance tests merged, with model-checker output in the PR.
• Reviewed and approved.

Resources:

• Quint: https://github.com/informalsystems/quint

Complexity: High (200 points)

[VikkyFame01]

@VikkyFame01 has applied to work on this issue as part of the Stellar Wave Program's 9th wave.

Hi Maintainer, please assign me to resolve this issue in due course. Thank you

ℹ️ Repo Maintainers: To accept this application, review their application or assign @VikkyFame01 to this issue.

[She-ge]

@She-ge has applied to work on this issue as part of the Stellar Wave Program's 9th wave.

Can i work on this please

ℹ️ Repo Maintainers: To accept this application, review their application or assign @She-ge to this issue.

[Goodnessoj]

@Goodnessoj has applied to work on this issue as part of the Stellar Wave Program's 9th wave.

Hi @maintainer kindly assign this issue to me

ℹ️ Repo Maintainers: To accept this application, review their application or assign @Goodnessoj to this issue.

[shemaiahdelia03-cmd]

@shemaiahdelia03-cmd has applied to work on this issue as part of the Stellar Wave Program's 9th wave.

i would love to work on this issue please

ℹ️ Repo Maintainers: To accept this application, review their application or assign @shemaiahdelia03-cmd to this issue.

[drips-wave]

Congratulations, @shemaiahdelia03-cmd! 🎉 Your application was accepted by the repo's maintainers, and the issue is due on September 30, 2026.

🧑‍💻 @shemaiahdelia03-cmd: Please resolve the issue such that the repo's maintainers have enough time to review your contribution before the due date. You'll earn Points for completing the issue on-time, which will make you eligible for a share of the Stellar Wave Program's reward pool.

Warning

When opening a PR, please link it to this issue to ensure it gets tracked accurately. Points are awarded when this issue is marked as completed by the maintainer.

🤠 Repo maintainers: Please keep an eye on the contributor's progress and review their work before the due date. You can manage this issue, including adjusting its complexity and points, here.

🌊 Happy Wave 🌊