RFC: Solana AccountInfo generators for Kani proofs

[mizuki0x]

RFC: Solana AccountInfo generators for Kani proofs (agent-style programs)

Motivation

Solana programs often structure critical logic around solana_program::account_info::AccountInfo and CPI calls.
When writing Kani proofs for these programs, a common first hurdle is creating well-formed AccountInfo<'a> values:

• AccountInfo contains borrowed fields (&Pubkey, &Pubkey) and interior-mutable borrows (Rc<RefCell<&mut u64>>, Rc<RefCell<&mut [u8]>>).
• Proof harnesses frequently need multiple accounts with specific constraints (signer/writable/owner, rent exemption, fixed data sizes).
• Doing this by hand is verbose and easy to get subtly wrong (aliasing, wrong lifetimes, accidentally shared buffers), which slows adoption.

PR #4549 shows Kani can verify patterns that show up in autonomous/agent-style payment flows (timelocks, value conservation, tiered thresholds, FSM transitions). The next practical step is to reduce harness boilerplate so Solana developers can apply Kani to their programs quickly.

Proposal

Add a small helper crate to the Kani repo that provides utilities to construct AccountInfo<'static> values for verification.

Why a helper crate (not kani::solana::* in the injected kani crate)

Kani injects a prebuilt kani crate into the compilation. Adding a Cargo feature to kani (e.g. features = ["solana-agent"]) would not be user-configurable at proof time unless Kani shipped multiple sysroots or rebuilt the injected crate.

A separate crate avoids pulling solana-program into the default Kani sysroot and keeps the integration optional for users.

Sketch

Crate (name bikeshed): kani-solana-agent

• Depends on solana-program.
• Exposes a small builder/config type and an account generator.
• Kani-specific code is behind cfg(kani); outside verification, functions can panic!("requires cargo kani").

Example API:

use kani_solana_agent::{AccountConfig, any_account_info};

#[kani::proof]
fn verify_flow() {
    let payer = any_account_info::<0>(AccountConfig::new().payer());
    let escrow = any_account_info::<128>(AccountConfig::new().writable());

    // call program logic under test ...
}

Possible config knobs (kept minimal):

• signer, writable, executable
• fixed owner: Pubkey
• lamports_range
• rent_exempt (default: assume rent-exempt)

Testing

Add a tests/cargo-kani/... crate that depends on the helper crate via a path dependency and verifies at least one harness.
This ensures the helper crate remains compatible with Kani and doesn’t regress.

Non-goals

• Modeling Solana syscalls / runtime behavior.
• Anchor-specific modeling.
• Token program semantics.
• Protocol-specific “agent” invariants.

Questions

1. Would Kani maintainers accept hosting this helper crate in-repo (as an optional integration), or would you prefer it live externally?
2. If in-repo, where should it live (library/, tools/, or tests/)?
3. Any concerns about the solana-program dependency footprint in CI for cargo-kani tests?

[mizuki0x]

Implementation PR opened: #4551 (helper crate + cargo-kani regression). Feedback welcome on naming/location and whether in-repo solana-program dependency is acceptable.

[feliperodri]

Thank you for the request! RFCs normally are documented in the Kani repo and the discussion to reach consensus happens in a PR. Read the https://model-checking.github.io/kani/rfc/ for all instructions. However, an early assessment:

1. Kani is a general-purpose model checker. AccountInfo is a Solana-specific type. Kani already has analogues for general patterns (kani::any(), kani::assume()) and purposefully avoids encoding domain knowledge. Hosting a Solana-specific builder would be a one-off exception with no principled boundary. What about EVM types? CosmWasm? NEAR?

2. solana-program is a heavyweight, volatile dependency. It pulls in borsh, bs58, crypto crates, and has frequent breaking releases tightly coupled to the Solana toolchain version. This would add CI friction (version pinning, toolchain matrix) with zero benefit to the vast majority of Kani users.

3. Your RFC correctly notes that solana-program shouldn't enter the default sysroot and that the integration should be optional. That's exactly the description of an external crate published independently on crates.io.

4. Kani maintainers would be responsible for keeping kani-solana-agent compatible with every Solana SDK update. That's an ongoing operational cost for a niche domain.

Bottom line: This is a community/ecosystem crate, not a Kani core concern. So I recommend you to publish kani-solana-agent independently on crates.io, so it is maintained by the Solana/Kani community. You can then link it from Kani's documentation as a community integration.

My recommendation is to close this GitHub issue and all PRs related to this change. Let me know your thoughts.