kani-0.68.0

Kani Rust verifier release bundle version 0.68.0.

What's Changed

New Features

• Add #[kani::loop_decreases] for proving loop termination by @feliperodri in #4564
• Add --export-json for structured verification results by @yimingyinqwqq in #4472
• Emit SARIF output for Code Scanning by @mizuki0x in #4547
• Add progress indicator and log file output for concise terminal output by @tautschnig in #4528
• Add git revision and rustc version info to verbose version output by @tautschnig in #4466
• Warn when the CBMC on PATH does not match the pinned version by @ivmat in #4723
• Force-load the kani crate so no_std crates work out of the box by @tautschnig in #4682
• Add --no-assert-overrides escape hatch for macro-override conflicts by @tautschnig in #4687
• Keep completed results when --fail-fast aborts a run by @ivmat in #4744
• Fail a zero-match harness filter before codegen and export by @ivmat in #4743

Stubbing

• Towards stubbing stabilization by @feliperodri in #4566
• Support stubbing trait method implementations by @feliperodri in #4587
• Implement stub sets for reusable stub groups by @feliperodri in #4594
• Detect stub_verified/Arbitrary recursion at compile time by @feliperodri in #4571

Contracts and Quantifiers

• Support arithmetic in quantifier predicates via pure expression inlining by @feliperodri in #4578
• Support pointer arithmetic in quantifier predicates by @feliperodri in #4583
• Warn when quantifier range exceeds SAT solver threshold by @feliperodri in #4579
• Reject mutual recursion with #[kani::recursion] by @feliperodri in #4580
• Emit explicit contract:: symbols for functions with contracts by @tautschnig in #4612

Autoharness

• Assume safety invariants of generated values by @tautschnig in #4677
• Assume layout niches of generated scalar values by @tautschnig in #4716
• Support raw pointer arguments by @tautschnig in #4678
• Support generic functions by @tautschnig in #4679
• Support slice and string arguments (bounded) by @tautschnig in #4691
• Support unbounded slice, mutable slice and Vec arguments by @tautschnig in #4721
• Support BoundedArbitrary argument types by @tautschnig in #4693
• Support smart pointers of compiler-derivable pointees by @tautschnig in #4698
• Do not synthesize Arbitrary for structs with reference fields by @tautschnig in #4694
• Verify Debug and Display implementations by @tautschnig in #4701
• Verify harnesses in parallel by default by @tautschnig in #4705
• Per-parameter and trait-impl-derived generic instantiation by @tautschnig in #4706
• Instantiate Fn-bounded type parameters with nondet closures by @tautschnig in #4726
• Constructor-based value generation (--constructor-args) by @tautschnig in #4717
• Mine constructor assertions into value filters by @tautschnig in #4718
• Mine type invariants from a type's own assertions by @tautschnig in #4722

Intrinsics and Arbitrary

• Add support for volatile_copy_memory, volatile_copy_nonoverlapping_memory and volatile_set_memory by @ivmat in #4672
• Add support for unaligned_volatile_load and unaligned_volatile_store by @ivmat in #4673
• Implement Arbitrary for Rc<T> and Arc<T> by @tautschnig in #4697
• Implement BoundedArbitrary for BTreeMap and BTreeSet by @hz2 in #4626

Performance

• Add a unified codegen cache by @AlexanderPortland in #4313
• Add heuristic to order harness codegen by @AlexanderPortland in #4257
• Link independent harness models in parallel by @M00NLIG7 in #4762

Major Bug Fixes

Soundness

• Fail verification when the solver backend drops quantifiers by @tautschnig in #4719
• Fix unsound f128 -> i128 lower bound in float-to-int range check by @tautschnig in #4663
• Fix floating-point remainder soundness and add soundness documentation by @feliperodri in #4570
• Fix OffsetModel missing UB for offsets wrapping CBMC's pointer encoding by @tautschnig in #4671
• Check that fast math intrinsic results are finite by @feliperodri in #4730
• Fix float-to-int saturating cast bug by @tautschnig in #4541
• Fix saturating float-to-int cast by @Rexicon226 in #4573
• Fix atomic compare_exchange to return correct failure status by @tautschnig in #4542

Contracts

• Fix the bug of moving (instead of cloning) the expression inside old of function contract by @thanhnguyen-aws in #4513
• Do not assert dependency contracts for calls made by contract clauses by @tautschnig in #4710
• Dispatch clause-context calls to the check target to the original body by @tautschnig in #4709
• Elide vacuous pointer checks on contract-closure capture loads by @tautschnig in #4715
• Fix loop-contract transform for post-#145513 deref temporaries by @tautschnig in #4659
• Skip ZST targets in loop_modifies assigns clause by @feliperodri in #4792
• Fix compiler crash on slice-modifies verified stubs by @feliperodri in #4749
• Fix stubbing bugs: FFI name resolution and generic parameter validation by @feliperodri in #4565

Crashes and ICEs

• Fix codegen panic for calls through a function pointer returning ! by @MavenRain in #4647
• Fix ICE on ConstantIndex projection of DST trailing slice field by @tautschnig in #4681
• Fix ICE on non-literal cover/assert/check message expressions by @ivmat in #4711
• Fix three constructor-discovery ICEs from the crates.io sweep by @tautschnig in #4725
• Degrade constant fat pointers to unsupported DSTs instead of crashing by @tautschnig in #4704
• Codegen single-non-ZST-field constants with name-keyed struct fields by @tautschnig in #4724
• Fix CBMC output parser panic when using SMT solvers by @tautschnig in #4540
• Emit a diagnostic for a misapplied checked size/align intrinsic marker by @MavenRain in #4648

Dependency Bumps

• Automatic upgrade of CBMC dependency to 6.11.0 in #4754
• Upgrade Rust toolchain to nightly-2026-08-21 by @feliperodri in #4768

New Contributors

• @nmanthey made their first contribution in #4535
• @mizuki0x made their first contribution in #4547
• @Rexicon226 made their first contribution in #4573
• @ivmat made their first contribution in #4672
• @MavenRain made their first contribution in #4647
• @hz2 made their first contribution in #4626
• @yimingyinqwqq made their first contribution in #4472
• @lovesegfault made their first contribution in #4601
• @M00NLIG7 made their first contribution in #4762
• @Tianshu-Huang made their first contribution in #4785

Full Changelog: kani-0.67.0...kani-0.68.0