Issues

• -Z valid-value-checks reports invalid values during initialization and raw field-address formation

  [C] Bug
  model-checking/kani#5056 · Filter by author v3risec opened on Oct 23, 2026
  1

• Support libc strlen through CBMC's built-in model without -Z c-ffi

  model-checking/kani#5055 · Filter by author feliperodri opened on Oct 23, 2026

• Loop contracts: a write missing from loop_modifies is accepted at -Zmir-opt-level=2 (the kani_loop_modifies binding is optimized out)

  [C] Bug
  model-checking/kani#5053 · Filter by author kasimte opened on Oct 23, 2026

• Use a Lean proof of a generic invariant from Kani harnesses

  model-checking/kani#5052 · Filter by author feliperodri opened on Oct 22, 2026 · Charon front end (LLBC)

• Keep the Charon pin compatible with an Aeneas release

  model-checking/kani#5051 · Filter by author feliperodri opened on Oct 22, 2026 · Charon front end (LLBC)

• LLBC backend: translate a crate's generic items without a proof harness

  model-checking/kani#5050 · Filter by author feliperodri opened on Oct 22, 2026 · Charon front end (LLBC)

• LLBC backend: name the output file after the crate

  model-checking/kani#5049 · Filter by author feliperodri opened on Oct 22, 2026 · Charon front end (LLBC)

• LLBC backend: translate promoted MIR, so Lean models have no drop flags

  model-checking/kani#5048 · Filter by author feliperodri opened on Oct 22, 2026 · Charon front end (LLBC)

• LLBC backend: generic functions with trait bounds abort translation

  model-checking/kani#5047 · Filter by author feliperodri opened on Oct 22, 2026 · Charon front end (LLBC)

• LLBC backend: uses of const items produce LLBC that Charon and Aeneas reject

  model-checking/kani#5046 · Filter by author feliperodri opened on Oct 22, 2026 · Charon front end (LLBC)

• Faster standard-library verification runs: load-independent timeouts, largest-first starts, a memory check and a faster --dfcc

  model-checking/kani#5043 · Filter by author srivatsansamraj opened on Oct 22, 2026

• Verify generic code once for an abstract T (symbolic size, alignment and trait behaviour)

  model-checking/kani#5041 · Filter by author feliperodri opened on Oct 21, 2026

• Contracts: flag writes to memory behind a live &T argument

  model-checking/kani#5040 · Filter by author feliperodri opened on Oct 21, 2026

• Proof coverage: report which assumptions and code a successful proof depends on

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

• Autoharness: &str arguments can be invalid UTF-8 under verify-std, causing spurious failures

  [C] Bug
  model-checking/kani#5030 · Filter by author CYJ904 opened on Oct 16, 2026

• modifies with a zero-sized target before another target makes valid writes fail the assigns check

  model-checking/kani#5029 · Filter by author JeroenRobben opened on Oct 16, 2026

• mul_add with an infinite addend or 0 * inf fails with "floating-point exception"

  model-checking/kani#5028 · Filter by author JeroenRobben opened on Oct 16, 2026

• Compiler panic: padding component emitted after the slice tail of an unsized struct

  model-checking/kani#5027 · Filter by author JeroenRobben opened on Oct 16, 2026

• Compiler panic on a pointer to a tuple with an unsized tail, *const (u32, [u32])

  model-checking/kani#5026 · Filter by author JeroenRobben opened on Oct 16, 2026

• Compiler panic on a constant of a #[repr(align(N))] newtype around a scalar

  model-checking/kani#5025 · Filter by author JeroenRobben opened on Oct 16, 2026

• Compiler panic reading the discriminant of a niche-encoded enum whose niche value does not fit in u64

  model-checking/kani#5024 · Filter by author JeroenRobben opened on Oct 16, 2026

• -Z valid-value-checks: invalid enum discriminant not reported when the enum is not a scalar or scalar pair

  model-checking/kani#5023 · Filter by author JeroenRobben opened on Oct 16, 2026

• -Z valid-value-checks: reading an invalid element through a slice pointer is not reported

  model-checking/kani#5022 · Filter by author JeroenRobben opened on Oct 16, 2026

• -Z valid-value-checks: writing an invalid bool through a *const round-trip or a transmuted &mut u8 is not reported

  model-checking/kani#5021 · Filter by author JeroenRobben opened on Oct 16, 2026

• -Z uninit-checks can miss uninitialized bytes in nonzero-offset NonNull / Box fields

  model-checking/kani#5020 · Filter by author JeroenRobben opened on Oct 16, 2026