Skip to content

tests(cargo-kani): add solana agent escrow example#4549

Open
kamiyo-ai wants to merge 1 commit intomodel-checking:mainfrom
kamiyo-ai:kamiyo/kani-agentic-program-verification-primitives
Open

tests(cargo-kani): add solana agent escrow example#4549
kamiyo-ai wants to merge 1 commit intomodel-checking:mainfrom
kamiyo-ai:kamiyo/kani-agentic-program-verification-primitives

Conversation

@kamiyo-ai
Copy link
Contributor

@kamiyo-ai kamiyo-ai commented Feb 17, 2026

Adds a self-contained cargo-kani example crate under tests/cargo-kani/solana-agent-escrow/ that models a few safety-critical rules common in Solana-style agent payment flows.

Included proof harnesses (all expected to verify successfully):

  • Timelock authorization: only the agent can release funds before expiry; the API can release only after expiry.
  • Value conservation for settlement splits: refund + payment == amount across dispute/inference/expired-escrow paths.
  • Tiered oracle requirements: bounded in {3,4,5} and monotonic in value-at-risk.
  • Escrow FSM: actions respect a simple transition table; terminal states do not transition.

The model is intentionally minimal (no Solana runtime / Anchor modeling) and has no external dependencies, to keep regression cost low while exercising Kani on agentic patterns (FSMs, threshold logic, conservation invariants).

To run locally:

cd tests/cargo-kani/solana-agent-escrow
cargo kani --harness timelock_policy_matches_release_rule
cargo kani --harness settlement_splits_conserve_value
cargo kani --harness required_oracle_count_is_monotonic_and_bounded
cargo kani --harness escrow_fsm_actions_respect_transition_table

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant