feat(v2): add Kani + Miri verification harness

[abishekk92]

Kani + Miri verification harness for anchor-lang-v2, anchor-spl-v2

Summary

• Add 108 Kani proof harnesses (151 after macro expansion) across anchor-lang-v2 and anchor-spl-v2
• Add 59 Miri tests under -Zmiri-tree-borrows + 19 runtime correctness tests
• Wire a Makefile and GitHub Actions workflow to run the suite
• Migrate AccountCursor::next's alignment step to strict-provenance form (required for Tree Borrows)

All 108 Kani harnesses pass under Kani 0.67.0; all 78 Miri + runtime tests pass.

Verification coverage

Lane	Count	Passed	Failed
Kani	108 (151 expanded)	108	0
Miri (Tree Borrows)	59	59	0
Runtime tests	19	19	0

What's verified

anchor-lang-v2 — Kani (89 harnesses)

• Pod{U,I}{16,32,64} — roundtrip, ord, checked/saturating arithmetic, bitwise ops, shifts all match native
• Pod{U,I}128 — add/sub/mul/saturating under Z3; PodU128 div/rem unbounded; PodI128 rem with bounded divisor
• PodBool — roundtrip, not involution, non-zero-byte semantics
• Logic invariants — Ord transitivity/reflexivity/antisymmetry, DeMorgan, XOR/AND commutativity, Neg involution
• Adversarial edges — iN::MIN boundary, div-by-zero, shift-by-width, should-panic witnesses for debug overflow
• AccountBitvec — set/get, bit preservation, idempotence
• System program Transfer wire format — variant constant pinned, layout byte-identity via shared encode_system_transfer helper
• rent_exempt_lamports — overflow guard, boundary, monotonicity
• PDA — rejects >16 seeds (length guard only)

anchor-spl-v2 — Kani (19 harnesses)

• All 14 SPL Token discriminant values pinned against protocol (DISC_TRANSFER == 3, …, DISC_SYNC_NATIVE == 17)
• Layout harnesses for amount-style instructions (transfer, mint_to, burn, transfer_checked) via shared encode_amount_ix / encode_amount_decimals_ix helpers
• Pairwise distinctness across all 14 discriminants

anchor-lang-v2 — Miri (52 tests)

• AccountView Copy-aliasing — alias, interleaved writes, reference stability
• AccountCursor::next — non-dup walk, dup resolution, chained dups, lookup cache, short-circuit
• PodVec — push/pop/extend, bytemuck roundtrip, corrupted-len adversarial (OOB panics, not UB)
• Slab — header_ptr write provenance, ITEMS_OFFSET align-up math, swap_remove correctness
• Wrapper types — SystemAccount, UncheckedAccount, Program<T>, Signer load/reject paths

anchor-spl-v2 — Miri (7 tests)

• Mint / TokenAccount — size/align guards, zero-init, byte roundtrip, wrong-size rejection

Runtime tests (19 tests)

• sha256 discriminator formula (account:{name} → first 8 bytes)
• Derived error codes — no Custom(u32) collisions, reserved ranges
• Program-ID goldens — System, Token, Token2022, Associated Token, Memo
• PodVec corrupted-len contract — panic points pinned as #[should_panic]

AccountCursor::next strict-provenance migration

Tree Borrows rejects the existing int-to-ptr alignment mask:

self.ptr = (((self.ptr as usize) + 7) & !7) as *mut u8;

Sound on today's compiler + SBF; the as *mut u8 round-trip exposes provenance under Rust's strict-provenance contract. Migrated to .addr() + .add(delta):

let addr = self.ptr.addr();
let aligned = (addr + (BPF_ALIGN_OF_U128 - 1)) & !(BPF_ALIGN_OF_U128 - 1);
self.ptr = self.ptr.add(aligned - addr);

Same generated code; miri_cursor_walk passes under Tree Borrows after the change.

CI changes

• New workflow .github/workflows/verify-v2.yaml with three jobs (kani, miri, unit) — path-filtered to v2 crates + Makefile + the workflow file.
  • PRs run miri + unit only (~5 min).
  • Push to anchor-next / workflow_dispatch runs all three including kani (~8-10 min on 4 vCPU with -j --output-format=terse).
• Action SHAs pinned (actions/checkout@de0fac2e… # v6.0.2, dtolnay/rust-toolchain@e97e2d8c… # v1) to match the publish-* / build-cli workflows.
• Split caches — cargo home, cargo target, Kani solver bundle (~2 GB), rustup nightly toolchain — so cold-start cost is paid once per key.

How to test

All harnesses gated behind #[cfg(kani)] — no runtime behavior changes.

# One-shot install: Kani 0.67.0 + nightly Rust with miri
make install-verify-tools

# Run all lanes
make verify

# Individual lanes
make kani       # bounded model checking (~2 min local)
make miri       # UB + Tree Borrows (~5 min)
make unit-v2    # native-speed cargo test (~10 s)

# Toolchain version check / help
make check-kani
make help-kani
`

[vercel]

@abishekk92 is attempting to deploy a commit to the Solana Foundation Team on Vercel.

A member of the Team first needs to authorize it.

[jamie-osec]

I have a few comments about some parts of this PR, and I have my doubts about the usefulness of some of these Kani tests, but generally looks nice to have - Miri verification for the AccountCursor machinery is great 🙂

[abishekk92]

Thanks a lot for your review @jamie-osec, the feedback is very helpful (addressed them in the fix commit). I've taken the liberty to extract some of the test scaffold in to anchor_lang_v2::testing since the miri tests need AccountView (and to avoid dead-code), happy to remove them or put them in a different place on your suggestion.