Repository Issue Activity (beta)

#4811 Autoharness: support the `MultiCharEq` searcher types in `core::str::pattern`

#4796 `#[kani::loop_invariant]` with a method call lowers the call with "not enough arguments", substituting a non-deterministic value

#4808 Autoharness: support `&Wtf8` arguments under --bounded-arguments

#4807 Autoharness: models for `alloc` types in the `verify-std` flow

#4805 Autoharness: support `&ByteStr` arguments under --bounded-arguments

#4803 Autoharness: support `&CStr` arguments under --bounded-arguments

#4800 Box codegen does not walk the pattern type inside NonNull

#4751 Autoharness: make --bounded-arguments bounds configurable and surface them in the output

#4685 Publish a release whose bundled Rust accepts rust-version = 1.95

#4795 Misleading non-fatal "Failed to find Kani functions" ERROR for optional hooks (SliceValidityAssume) during whole-library runs

#4794 autoharness: E0080 abort when a const-generic fn has a `const {}` precondition on its usize param

#4790 Loop contracts: locals of the builtin `memcmp` model fail the assigns check when the loop body compares slices with `==`

#4786 CBMC aborts with `l2_rename_rvalues case `struct' not handled` when a zero-sized closure is a loop_modifies target

#3682 Failed to `stub_verified` contracts with slices in `kani::modifies`

#4779 `<[u8]>::contains` does not converge even on fully concrete data (memchr specialization); `iter().any` verifies in 0.2s

#4777 proof_for_contract cannot resolve methods on impls defined outside the type's own module when multiple same-named candidates exist

#4748 Verified function contract stubs fail compilation on slice references

#4774 Toolchain upgrade to nightly-2026-08-22 failed

#4773 Add ESBMC as a verification backend

#4770 Unsupported: calls to LLVM intrinsics (InstanceKind::LlvmIntrinsic)

#4769 Toolchain upgrade to nightly-2026-06-02 failed

#4729 `--fail-fast` discards results for harnesses that already completed

#4763 Autoharness --constructor-args: assumed mined invariants may exclude valid values (heuristic under-approximation)

#4761 loop_modifies over a Vec no longer establishes drop_in_place's new reference-creation precondition

#4759 vtable_size_align_drop no longer checks the drop slot holds the right type's drop glue