Issues

• valid-value-checks misses discriminant values inside the tag range of a enum

  [C] Bug
  model-checking/kani#5156 · Filter by author zhouxt1 opened on Nov 11, 2026

• Out-of-bounds get_unchecked_mut on a slice is not reported

  [C] Bug
  model-checking/kani#5155 · Filter by author zhouxt1 opened on Nov 11, 2026

• Models for process-global OS state used by std::sys (environment, execve, signal alt stacks)

  model-checking/kani#5150 · Filter by author feliperodri opened on Nov 11, 2026

• -Z uninit-checks: arrays of MaybeUninit<T> with non-trivial T are unsupported

  model-checking/kani#5151 · Filter by author feliperodri opened on Nov 11, 2026

• Support thread-local destructors and std::process::exit / libc exit semantics

  model-checking/kani#5149 · Filter by author feliperodri opened on Nov 11, 2026

• Quantifiers with a non-constant bound (forall!(|j in (0, i)| ...)) are dropped in loop invariants, and the suggested #[kani::solver(z3)] fails because z3 is not installed

  [F] Spurious FailureZ-Quantifiers
  Bug

  model-checking/kani#5148 · Filter by author feliperodri opened on Nov 10, 2026 · Contracts
  

• Loop contracts: a write to a variable captured by a closure is missing from the inferred write set, reported as Check that *var_18 is assignable

  [F] Spurious FailureZ-Contracts
  Bug

  model-checking/kani#5147 · Filter by author feliperodri opened on Nov 10, 2026 · Contracts

• compare_exchange_weak never fails spuriously

  [F] SoundnessZ-Kani Compiler
  Bug

  model-checking/kani#5146 · Filter by author 0xalpharush opened on Nov 10, 2026 · Soundness
  

• Pointer-to-integer casts: Kani proves heap and stack addresses are page-aligned

  [C] Bug[F] Soundness
  Bug

  model-checking/kani#5145 · Filter by author 0xalpharush opened on Nov 10, 2026 · Soundness
  

• Loop contracts: loop_modifies with a non-pointer argument crashes Kani (ICE expr.rs:737); &*r gives a misleading E0423

  [F] CrashZ-Contracts
  Bug

  model-checking/kani#5144 · Filter by author feliperodri opened on Nov 9, 2026 · Contracts

• Writes through an integer-cast pointer that equals a live object's address are dropped (false VERIFICATION SUCCESSFUL); this makes stub_verified unsound for pointer-holding modifies targets and results

  [C] Bug[F] SoundnessT-CBMC
  Bug

  model-checking/kani#5143 · Filter by author c-grellois opened on Nov 9, 2026 · Soundness
  

• Non-nested quantifier predicates can silently discard default checks

  [C] Bug[F] SoundnessZ-Quantifiers
  Bug

  model-checking/kani#5141 · Filter by author v3risec opened on Nov 9, 2026 · Contracts
  

• Autoharness: types that should be supported (no Arbitrary, trait objects, fn pointers, HashMap, Option<&T>, Pin, tuples with &str)

  [C] Feature / Enhancement[E] Unsupported ConstructT-High PriorityZ-Autoharness
  Feature

  model-checking/kani#5137 · Filter by author feliperodri opened on Nov 7, 2026 · Autoharness
  1

  

• Compiler crashes on two custom_mir programs from Miri's test suite

  [F] Crash
  Bug

  model-checking/kani#5132 · Filter by author feliperodri opened on Nov 6, 2026
  

• Compiler panic on explicit tail calls (become)

  [E] Unsupported Construct[F] Crash
  Bug

  model-checking/kani#5131 · Filter by author feliperodri opened on Nov 6, 2026
  1

• Compiler panic on async closures (rustc_public: Lower these to SMIR)

  [F] CrashZ-Kani Compiler
  Bug

  model-checking/kani#5130 · Filter by author feliperodri opened on Nov 6, 2026

• Misaligned accesses that depend on where an allocation is placed are not detected

  Bug

  model-checking/kani#5129 · Filter by author feliperodri opened on Nov 6, 2026
  

• Alignment check is dropped when debug assertions are off

  [F] Soundness
  Bug

  model-checking/kani#5128 · Filter by author feliperodri opened on Nov 6, 2026 · Soundness
  

• Performance: common std constructs (padded integer formatting, str::parse, recursive drop, Backtrace::capture) time out

  [E] Performance
  Feature

  model-checking/kani#5127 · Filter by author feliperodri opened on Nov 6, 2026
  

• assert! and panic! become ambiguous under cargo kani when the crate glob-imports its own prelude

  [C] Bug
  Bug

  model-checking/kani#5126 · Filter by author feliperodri opened on Nov 6, 2026
  

• Spurious failure: ptr.map_addr(|a| a & 0).addr() is not 0

  [C] Bug[F] Spurious Failure
  Bug

  model-checking/kani#5125 · Filter by author feliperodri opened on Nov 6, 2026

• cargo kani list --format json writes kani-list.json into the package root

  [C] Feature / Enhancement[E] User Experience
  Feature

  model-checking/kani#5124 · Filter by author feliperodri opened on Nov 6, 2026
  

• cargo kani list rejects --target-dir, which cargo kani accepts

  [C] BugT-Good First Issue
  Bug

  model-checking/kani#5123 · Filter by author feliperodri opened on Nov 6, 2026

• cargo kani prints an unstable-feature warning for the injected #![feature(register_tool)] on every run

  [E] User Experience
  Bug

  model-checking/kani#5122 · Filter by author feliperodri opened on Nov 6, 2026

• Unwinding failure is reported inside <builtin-library-memcmp> instead of at the user code that compares slices

  [E] User Experience
  Bug

  model-checking/kani#5121 · Filter by author feliperodri opened on Nov 6, 2026