Issues

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

model-checking/kani#5030 · 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 · opened

on Oct 16, 2026

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

model-checking/kani#5028 · opened

on Oct 16, 2026

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

model-checking/kani#5027 · opened

on Oct 16, 2026

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

model-checking/kani#5026 · opened

on Oct 16, 2026

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

model-checking/kani#5025 · 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 · 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 · opened

on Oct 16, 2026

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

model-checking/kani#5022 · 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 · opened

on Oct 16, 2026

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

model-checking/kani#5020 · opened

on Oct 16, 2026

`write_bytes` / `volatile_set_memory` skip the alignment check when `count == 0`

model-checking/kani#5019 · opened

on Oct 16, 2026

`ptr::swap_nonoverlapping` and `typed_swap_nonoverlapping`: overlap and alignment are not checked

model-checking/kani#5018 · opened

on Oct 16, 2026

`#[kani::recursion]` treats a call to another instantiation of a generic function as recursion, so its unproven contract is assumed

model-checking/kani#5017 · opened

on Oct 16, 2026

Contract check passes vacuously when a recursive function without `#[kani::recursion]` calls itself with arguments that violate `requires`

model-checking/kani#5016 · opened

on Oct 16, 2026

`modifies` contract of a generic function is checked for only one instantiation in a harness

model-checking/kani#5015 · opened

on Oct 16, 2026

`size_of_val` is wrong for a nested struct with a `dyn` tail

model-checking/kani#5014 · opened

on Oct 16, 2026

Float `%` returns wrong values (7.0 % 2.0 == 0.0)

model-checking/kani#5013 · opened

on Oct 16, 2026

Invariant mining checks the wrong field when calling a getter on a nested struct

Bug

model-checking/kani#5011 · opened

on Oct 15, 2026

· Autoharness

Bugs in Quantifier feature

Bug

model-checking/kani#5010 · opened

on Oct 15, 2026

· Contracts

Toolchain upgrade to nightly-2026-10-13 failed

model-checking/kani#5009 · opened

on Oct 15, 2026

False recursion diagnostic despite an explicit Arbitrary replacement

model-checking/kani#5007 · opened

on Oct 14, 2026

`stub_verified` panics the compiler when a `modifies` target's type does not implement `kani::Arbitrary`

model-checking/kani#5005 · opened

on Oct 14, 2026

Quantifier predicates with `&&`, `||` or `if` keep only one branch, so a true `forall!` can fail and `assume(forall!(..))` can make a harness vacuous

Bug

model-checking/kani#5004 · opened

on Oct 14, 2026

· Contracts

Move compiletest off the deprecated serde_yaml

Task

model-checking/kani#5000 · opened

on Oct 13, 2026

Navigation Menu

Repository navigation

Issues

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

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

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

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

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

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

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

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

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

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

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

`write_bytes` / `volatile_set_memory` skip the alignment check when `count == 0`

`ptr::swap_nonoverlapping` and `typed_swap_nonoverlapping`: overlap and alignment are not checked

`#[kani::recursion]` treats a call to another instantiation of a generic function as recursion, so its unproven contract is assumed

Contract check passes vacuously when a recursive function without `#[kani::recursion]` calls itself with arguments that violate `requires`

`modifies` contract of a generic function is checked for only one instantiation in a harness

`size_of_val` is wrong for a nested struct with a `dyn` tail

Float `%` returns wrong values (7.0 % 2.0 == 0.0)

Invariant mining checks the wrong field when calling a getter on a nested struct

Bugs in Quantifier feature

Toolchain upgrade to nightly-2026-10-13 failed

False recursion diagnostic despite an explicit Arbitrary replacement

`stub_verified` panics the compiler when a `modifies` target's type does not implement `kani::Arbitrary`

Quantifier predicates with `&&`, `||` or `if` keep only one branch, so a true `forall!` can fail and `assume(forall!(..))` can make a harness vacuous

Move compiletest off the deprecated serde_yaml