RFC: Solana AccountInfo generators for Kani proofs

[kamiyo-ai]

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?

[kamiyo-ai]

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