diff --git a/library/kani_solana_agent/.gitignore b/library/kani_solana_agent/.gitignore
new file mode 100644
index 000000000000..2f7896d1d136
--- /dev/null
+++ b/library/kani_solana_agent/.gitignore
@@ -0,0 +1 @@
+target/
diff --git a/library/kani_solana_agent/Cargo.toml b/library/kani_solana_agent/Cargo.toml
new file mode 100644
index 000000000000..4244703f8b37
--- /dev/null
+++ b/library/kani_solana_agent/Cargo.toml
@@ -0,0 +1,17 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "kani-solana-agent"
+version = "0.1.0"
+edition = "2021"
+license = "MIT OR Apache-2.0"
+publish = false
+
+[dependencies]
+solana-program = "=3.0.0"
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ["cfg(kani)"] }
+
+[workspace]
diff --git a/library/kani_solana_agent/README.md b/library/kani_solana_agent/README.md
new file mode 100644
index 000000000000..3df5990c841e
--- /dev/null
+++ b/library/kani_solana_agent/README.md
@@ -0,0 +1,31 @@
+# Solana AccountInfo Utilities for Kani Proofs
+
+This crate provides small helpers to reduce the boilerplate involved in writing Kani proof harnesses for code that uses Solana's `AccountInfo` API.
+
+Non-goals:
+- Modeling Solana syscalls / runtime behavior
+- Anchor-specific modeling
+- Token program semantics
+
+The primary entry point is `any_account_info::<DATA_LEN>(...)` (alias: `any_agent_account::<DATA_LEN>(...)`), which constructs an `AccountInfo<'static>` backed by leaked allocations so it can be passed into program logic during verification.
+
+## Example
+
+```rust
+#[cfg(kani)]
+mod proofs {
+    use kani_solana_agent::{AccountConfig, LamportSnapshot, any_agent_account};
+
+    #[kani::proof]
+    fn can_build_accounts() {
+        let payer = any_agent_account::<0>(AccountConfig::new().payer());
+        let escrow = any_agent_account::<128>(AccountConfig::new().writable());
+
+        kani::assert(payer.is_signer, "payer must be a signer");
+        kani::assert(escrow.is_writable, "escrow must be writable");
+
+        let before = LamportSnapshot::new(&[&payer, &escrow]);
+        before.assert_unchanged(&[&payer, &escrow], "snapshot must be stable without mutation");
+    }
+}
+```
diff --git a/library/kani_solana_agent/src/account.rs b/library/kani_solana_agent/src/account.rs
new file mode 100644
index 000000000000..de2b494d5203
--- /dev/null
+++ b/library/kani_solana_agent/src/account.rs
@@ -0,0 +1,173 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use solana_program::account_info::AccountInfo;
+use solana_program::pubkey::Pubkey;
+use std::ops::RangeInclusive;
+
+#[cfg(kani)]
+use solana_program::rent::Rent;
+#[cfg(kani)]
+use std::cell::RefCell;
+#[cfg(kani)]
+use std::rc::Rc;
+
+#[derive(Clone, Debug)]
+enum Lamports {
+    Any,
+    Exact(u64),
+    Range(RangeInclusive<u64>),
+}
+
+#[derive(Clone, Debug)]
+pub struct AccountConfig {
+    key: Option<Pubkey>,
+    owner: Option<Pubkey>,
+    lamports: Lamports,
+    rent_exempt: bool,
+
+    pub is_signer: bool,
+    pub is_writable: bool,
+    pub executable: bool,
+    pub rent_epoch: u64,
+}
+
+impl Default for AccountConfig {
+    fn default() -> Self {
+        Self {
+            key: None,
+            owner: None,
+            lamports: Lamports::Any,
+            rent_exempt: true,
+            is_signer: false,
+            is_writable: false,
+            executable: false,
+            rent_epoch: 0,
+        }
+    }
+}
+
+impl AccountConfig {
+    pub fn new() -> Self {
+        Self::default()
+    }
+
+    pub fn key(mut self, key: Pubkey) -> Self {
+        self.key = Some(key);
+        self
+    }
+
+    pub fn owner(mut self, owner: Pubkey) -> Self {
+        self.owner = Some(owner);
+        self
+    }
+
+    pub fn signer(mut self) -> Self {
+        self.is_signer = true;
+        self
+    }
+
+    pub fn writable(mut self) -> Self {
+        self.is_writable = true;
+        self
+    }
+
+    pub fn payer(mut self) -> Self {
+        self.is_signer = true;
+        self.is_writable = true;
+        self
+    }
+
+    pub fn executable(mut self) -> Self {
+        self.executable = true;
+        self
+    }
+
+    pub fn lamports(mut self, lamports: u64) -> Self {
+        self.lamports = Lamports::Exact(lamports);
+        self
+    }
+
+    pub fn lamports_range(mut self, range: RangeInclusive<u64>) -> Self {
+        self.lamports = Lamports::Range(range);
+        self
+    }
+
+    pub fn rent_exempt(mut self, enabled: bool) -> Self {
+        self.rent_exempt = enabled;
+        self
+    }
+
+    pub fn rent_epoch(mut self, epoch: u64) -> Self {
+        self.rent_epoch = epoch;
+        self
+    }
+}
+
+pub fn any_agent_account<const DATA_LEN: usize>(cfg: AccountConfig) -> AccountInfo<'static> {
+    any_account_info::<DATA_LEN>(cfg)
+}
+
+#[cfg(kani)]
+fn any_pubkey() -> Pubkey {
+    Pubkey::new_from_array(kani::any())
+}
+
+#[cfg(kani)]
+fn pick_lamports<const DATA_LEN: usize>(cfg: &AccountConfig) -> u64 {
+    let lamports = match &cfg.lamports {
+        Lamports::Any => kani::any(),
+        Lamports::Exact(v) => *v,
+        Lamports::Range(r) => {
+            let v: u64 = kani::any();
+            kani::assume(r.contains(&v));
+            v
+        }
+    };
+
+    if cfg.rent_exempt {
+        kani::assume(Rent::default().is_exempt(lamports, DATA_LEN));
+    }
+
+    lamports
+}
+
+#[cfg(kani)]
+pub fn any_account_info<const DATA_LEN: usize>(cfg: AccountConfig) -> AccountInfo<'static> {
+    let key = cfg.key.unwrap_or_else(any_pubkey);
+    let owner = cfg.owner.unwrap_or_else(any_pubkey);
+    let lamports = pick_lamports::<DATA_LEN>(&cfg);
+
+    let key: &'static Pubkey = Box::leak(Box::new(key));
+    let owner: &'static Pubkey = Box::leak(Box::new(owner));
+
+    let lamports: &'static mut u64 = Box::leak(Box::new(lamports));
+    let data: &'static mut [u8; DATA_LEN] = Box::leak(Box::new(kani::any()));
+    let data: &'static mut [u8] = data;
+
+    AccountInfo {
+        key,
+        is_signer: cfg.is_signer,
+        is_writable: cfg.is_writable,
+        lamports: Rc::new(RefCell::new(lamports)),
+        data: Rc::new(RefCell::new(data)),
+        owner,
+        executable: cfg.executable,
+        rent_epoch: cfg.rent_epoch,
+    }
+}
+
+#[cfg(not(kani))]
+pub fn any_account_info<const DATA_LEN: usize>(cfg: AccountConfig) -> AccountInfo<'static> {
+    let _ = DATA_LEN;
+    match cfg.lamports {
+        Lamports::Any => {}
+        Lamports::Exact(v) => {
+            let _ = v;
+        }
+        Lamports::Range(r) => {
+            let _ = r;
+        }
+    }
+    panic!("any_account_info is only available under `cargo kani` (cfg(kani))");
+}
diff --git a/library/kani_solana_agent/src/invariants.rs b/library/kani_solana_agent/src/invariants.rs
new file mode 100644
index 000000000000..507c4448d349
--- /dev/null
+++ b/library/kani_solana_agent/src/invariants.rs
@@ -0,0 +1,31 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use solana_program::account_info::AccountInfo;
+
+pub fn lamports(account: &AccountInfo<'_>) -> u64 {
+    **account.lamports.borrow()
+}
+
+pub fn sum_lamports(accounts: &[&AccountInfo<'_>]) -> u128 {
+    accounts.iter().map(|a| lamports(a) as u128).sum()
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub struct LamportSnapshot(pub u128);
+
+impl LamportSnapshot {
+    pub fn new(accounts: &[&AccountInfo<'_>]) -> Self {
+        Self(sum_lamports(accounts))
+    }
+
+    pub fn assert_unchanged(self, accounts: &[&AccountInfo<'_>], msg: &'static str) {
+        let after = sum_lamports(accounts);
+
+        #[cfg(kani)]
+        kani::assert(after == self.0, msg);
+
+        #[cfg(not(kani))]
+        assert!(after == self.0, "{msg}");
+    }
+}
diff --git a/library/kani_solana_agent/src/lib.rs b/library/kani_solana_agent/src/lib.rs
new file mode 100644
index 000000000000..b3e7e5a5f9e2
--- /dev/null
+++ b/library/kani_solana_agent/src/lib.rs
@@ -0,0 +1,10 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+pub mod account;
+pub mod invariants;
+
+pub use account::{AccountConfig, any_account_info, any_agent_account};
+pub use invariants::{LamportSnapshot, lamports, sum_lamports};
+pub use solana_program::account_info::AccountInfo;
+pub use solana_program::pubkey::Pubkey;
diff --git a/tests/cargo-kani/solana-accountinfo/Cargo.toml b/tests/cargo-kani/solana-accountinfo/Cargo.toml
new file mode 100644
index 000000000000..3fc60a445396
--- /dev/null
+++ b/tests/cargo-kani/solana-accountinfo/Cargo.toml
@@ -0,0 +1,16 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "solana-accountinfo"
+version = "0.1.0"
+edition = "2018"
+
+[dependencies]
+kani-solana-agent = { path = "../../../library/kani_solana_agent" }
+solana-program = "=3.0.0"
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ["cfg(kani)"] }
+
+[workspace]
diff --git a/tests/cargo-kani/solana-accountinfo/release_funds_conserves_lamports.expected b/tests/cargo-kani/solana-accountinfo/release_funds_conserves_lamports.expected
new file mode 100644
index 000000000000..34c886c358cb
--- /dev/null
+++ b/tests/cargo-kani/solana-accountinfo/release_funds_conserves_lamports.expected
@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/cargo-kani/solana-accountinfo/src/lib.rs b/tests/cargo-kani/solana-accountinfo/src/lib.rs
new file mode 100644
index 000000000000..787dc64480c4
--- /dev/null
+++ b/tests/cargo-kani/solana-accountinfo/src/lib.rs
@@ -0,0 +1,110 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[cfg(kani)]
+use kani_solana_agent::AccountInfo;
+
+#[cfg(kani)]
+fn authorized(now: i64, expires_at: i64, agent: &AccountInfo<'_>, api: &AccountInfo<'_>) -> bool {
+    agent.is_signer || (api.is_signer && now >= expires_at)
+}
+
+#[cfg(kani)]
+fn transfer(from: &AccountInfo<'_>, to: &AccountInfo<'_>, amount: u64) -> Result<(), ()> {
+    let mut from_lamports = from.lamports.borrow_mut();
+    let Some(new_from) = (**from_lamports).checked_sub(amount) else {
+        return Err(());
+    };
+    **from_lamports = new_from;
+    drop(from_lamports);
+
+    let mut to_lamports = to.lamports.borrow_mut();
+    let Some(new_to) = (**to_lamports).checked_add(amount) else {
+        return Err(());
+    };
+    **to_lamports = new_to;
+    Ok(())
+}
+
+#[cfg(kani)]
+fn release_funds(
+    now: i64,
+    expires_at: i64,
+    agent: &AccountInfo<'_>,
+    api: &AccountInfo<'_>,
+    escrow: &AccountInfo<'_>,
+    payee: &AccountInfo<'_>,
+    amount: u64,
+) -> Result<(), ()> {
+    if !authorized(now, expires_at, agent, api) {
+        return Err(());
+    }
+
+    transfer(escrow, payee, amount)
+}
+
+#[cfg(kani)]
+mod proofs {
+    use super::*;
+    use kani_solana_agent::{AccountConfig, LamportSnapshot, any_agent_account, lamports};
+
+    #[kani::proof]
+    fn timelock_policy_matches_release_rule() {
+        let now: i64 = kani::any();
+        let expires_at: i64 = kani::any();
+
+        let mut agent = any_agent_account::<0>(AccountConfig::new());
+        let mut api = any_agent_account::<0>(AccountConfig::new());
+        agent.is_signer = kani::any();
+        api.is_signer = kani::any();
+
+        let allowed = authorized(now, expires_at, &agent, &api);
+
+        if now < expires_at {
+            kani::assert(allowed == agent.is_signer, "before expiry only agent can release");
+        } else {
+            kani::assert(
+                allowed == (agent.is_signer || api.is_signer),
+                "after expiry agent or api can release",
+            );
+        }
+    }
+
+    #[kani::proof]
+    fn release_funds_conserves_lamports() {
+        let now: i64 = kani::any();
+        let expires_at: i64 = kani::any();
+        let amount: u64 = kani::any::<u32>() as u64;
+
+        let mut agent = any_agent_account::<0>(AccountConfig::new());
+        let mut api = any_agent_account::<0>(AccountConfig::new());
+        agent.is_signer = kani::any();
+        api.is_signer = kani::any();
+
+        let escrow = any_agent_account::<0>(
+            AccountConfig::new().writable().lamports_range(0..=(u32::MAX as u64)),
+        );
+        let payee = any_agent_account::<0>(
+            AccountConfig::new().writable().lamports_range(0..=(u32::MAX as u64)),
+        );
+
+        let escrow_before = lamports(&escrow);
+        let payee_before = lamports(&payee);
+        kani::assume(escrow_before >= amount);
+
+        let total_before = LamportSnapshot::new(&[&escrow, &payee]);
+
+        let res = release_funds(now, expires_at, &agent, &api, &escrow, &payee, amount);
+        let escrow_after = lamports(&escrow);
+        let payee_after = lamports(&payee);
+
+        if res.is_ok() {
+            total_before.assert_unchanged(&[&escrow, &payee], "release must conserve lamports");
+            kani::assert(escrow_after + amount == escrow_before, "escrow must decrease by amount");
+            kani::assert(payee_before + amount == payee_after, "payee must increase by amount");
+        } else {
+            kani::assert(escrow_after == escrow_before, "failed release must not mutate");
+            kani::assert(payee_after == payee_before, "failed release must not mutate");
+        }
+    }
+}
diff --git a/tests/cargo-kani/solana-accountinfo/timelock_policy_matches_release_rule.expected b/tests/cargo-kani/solana-accountinfo/timelock_policy_matches_release_rule.expected
new file mode 100644
index 000000000000..34c886c358cb
--- /dev/null
+++ b/tests/cargo-kani/solana-accountinfo/timelock_policy_matches_release_rule.expected
@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL