Issues

• 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

• 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
  

• Replace-mode stubs drop an owned receiver even when the real body moves it out

  [C] Bug[F] Spurious Failure
  Bug

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

• kani-driver uses ~12 GiB on a single harness while CBMC peaks at ~2.3 GiB

  [C] Bug[E] PerformanceT-User
  Bug

  model-checking/kani#5117 · Filter by author Tiramisu-Cake opened on Nov 3, 2026

• Contract attributes on a specialization default fn fail to parse ("expected fn")

  [C] BugZ-Contracts
  Bug

  model-checking/kani#5116 · Filter by author Tiramisu-Cake opened on Nov 3, 2026 · Contracts

• -Z uninit-checks rejects valid atomic stores to uninitialized memory

  [C] Bug[F] Spurious FailureZ-UnstableFeature
  Bug

  model-checking/kani#5114 · Filter by author v3risec opened on Nov 3, 2026
  

• Loop contracts: loop_modifies is ignored at -Zmir-opt-level>=2, and listing a &mut target moves it

  T-High PriorityZ-Contracts
  Bug

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

• Support concrete playback for the autoharness subcommand

  [C] Feature / EnhancementZ-Autoharness
  Feature

  model-checking/kani#5109 · Filter by author feliperodri opened on Nov 2, 2026 · Concrete Playback
  

• ICE in kani-compiler (body.rs:680 "terminators without a target field") applying loop contracts to a dependency-generated loop (uint 0.9.5 div_mod_knuth)

  [C] Bug[F] CrashZ-Contracts
  Bug

  model-checking/kani#5107 · Filter by author rousjiamo opened on Nov 2, 2026 · Contracts
  

• False counterexample for a conditional pointer read of [u8; 1]

  [C] BugT-High Priority
  Bug

  model-checking/kani#5104 · Filter by author Tiramisu-Cake opened on Nov 1, 2026 · Soundness
  1

  

• cargo kani autoharness's default --default-unwind 20 silently applies to pre-existing manual harnesses too, causing spurious failures

  [C] Bug[F] Spurious FailureT-High PriorityZ-Autoharness
  Bug

  model-checking/kani#5103 · Filter by author feliperodri opened on Oct 31, 2026 · Autoharness

• kani-cov summary panics on any file in the mapfile that has no instrumented coverage regions

  [C] Bug[F] CrashT-Good First Issue
  Bug

  model-checking/kani#5102 · Filter by author feliperodri opened on Oct 31, 2026 · Coverage reports

• Internal compiler error on HashMap/HashSet (RandomState::new): rustc_metadata panics on AnonConst

  [C] Bug[F] CrashT-High PriorityZ-Kani Compiler
  Bug

  model-checking/kani#5101 · Filter by author feliperodri opened on Oct 31, 2026
  1

• --concrete-playback=inplace panics with NotFound when run inside a workspace member

  [C] Bug[F] Crash
  Bug

  model-checking/kani#5100 · Filter by author feliperodri opened on Oct 30, 2026 · Concrete Playback

• Function-contract model validation fails for a constant-returning boolean function — Kani 0.68.0 / CBMC 6.11.0

  [C] BugZ-Contracts
  Bug

  model-checking/kani#5097 · Filter by author Egly443 opened on Oct 29, 2026 · Contracts