feat(v2): add Kani + Miri verification harness#4424

Open

abishekk92 wants to merge 15 commits intosolana-foundation:anchor-nextfrom

QEDGen:feat/v2-verification

Commits on Apr 23, 2026

feat(v2): add Kani + Miri verification harness
abishekk92
committed
fix(v2): address PR review feedback
abishekk92
committed
chore(v2): drop -j on Kani CI step to avoid Z3/CBMC flake
abishekk92
committed
chore(v2): gate testing module behind testing feature flag
abishekk92
committed
fix(v2): AccountBuffer uses UnsafeCell so sibling writes don't Disable AccountView tags
abishekk92
committed
test(v2): skip stale_detection_misses_content_only_out_of_band_mutation under Miri
abishekk92
committed
feat(v2): prove Slab capacity + slice-bounds invariants with Kani
abishekk92
committed
ci(v2): split Kani per-crate with 3x retry to tolerate kani-driver 0.67.0 panic on CBMC ERROR
abishekk92
committed
fix(v2): swap Slab slice-bounds Kani harness for compositional clamp proof
abishekk92
committed
fix(v2): split capacity_fits_within_data_len Kani harness per concrete item_size
abishekk92
committed
ci(v2): drop Kani 3x retry loop
abishekk92
committed
refactor(v2): downgrade concrete Kani harnesses to unit tests
abishekk92
committed
fix(v2): own fresh_lookup Vec on test stack to clear Miri leaks
abishekk92
committed
ci(v2): drop Kani from CI pending kani-verifier 0.68.0
abishekk92
committed

Commits on May 2, 2026

Merge remote-tracking branch 'origin/anchor-next' into feat/v2-verification
abishekk92
committed