feat: formal Quint spec and Kani proofs (#414, #415)

[shemaiahdelia03-cmd]

Issue #414 — Formal Quint specification of the intent state machine:

• spec/vortex.qnt: covers all 11 IntentState variants and every transition documented in the README lifecycle diagram (submit, accept, fill, partial fill, cancel, expire, slash, begin_fill, release_fill, open_dispute, resolve_dispute, arbiter timeout)
• 8 safety invariants (INV-1..INV-8) checked with Apalache / Quint simulator: no double payout, bond never negative, no stuck intents, accepted has solver, filled amount sufficient, treasury monotone, cancel only from Open, resolved has outcome
• 2 liveness properties: every intent eventually reaches a terminal state; a solver can always eventually accept an open intent
• 6 named traces (happyPath, cancelPath, expirePath, slashPath, disputeUpheldPath, disputeDismissedPath) exported as ITF witnesses
• intent_settlement/tests/conformance.rs: Rust integration tests replay each trace against the real contract, asserting the safety invariants on-chain
• docs/formal-spec.md: plain-English property documentation and usage guide
• Bounding strategy: 2 users, 2 solvers, 2 intents, ticks 0..30
• spec/traces/README.md + .gitignore entry for *.itf.json

Issue #415 — Kani proofs for pure arithmetic helpers:

• intent_settlement/src/math.rs: Env-free pure functions extracted from lib.rs (compute_slash_amount, compute_slash_amount_tiered, tier_fill_window, compute_fee, apply_discount, dutch_decay, slash_bps_for_tier, fill_window_bonus_bps_for_tier, decode_i128_be, decode_u32_be, decode_u16_be, decode_payload_chain_id, decode_payload_src_amount) with 25 unit tests (no Soroban env required)
• intent_settlement/src/kani_proofs.rs: 12 Kani harnesses with documented properties (slash never negative, slash never exceeds bond, slash floor 1, fill window monotone, fill window no overflow, fee never exceeds amount, fee rounds down, dutch decay bounds, discount in range, decode payload roundtrip, slash bps monotone, decode bounds safe)
• Makefile: make kani target runs all 12 harnesses
• lib.rs: pub mod math and #[cfg(kani)] mod kani_proofs declarations

Closes #414
Closes #415

Summary

Related issue

Type of change

• Bug fix
• New feature
• Refactor
• Documentation
• CI / tooling

Component

• Contract (vortex-contract)
• Backend (vortex-backend)
• Frontend (vortex-frontend)

Checklist

• My code follows the project's style and conventions
• I ran lint / type-check / build locally and they pass
• I added or updated tests where appropriate
• I updated documentation where appropriate
• My commits follow Conventional Commits

Screenshots / notes

[drips-wave]

@shemaiahdelia03-cmd Great news! 🎉 Based on an automated assessment of this PR, the linked Wave issue(s) no longer count against your application limits.

You can now already apply to more issues while waiting for a review of this PR. Keep up the great work! 🚀

Learn more about application limits