Kani Rust verifier release bundle version 0.67.0.

What's Changed

• Gracefully fail when compiling structs with too large array by @tautschnig in #4461
• fix: Make kani attribute nameres work with generic args having :: by @ShoyuVanilla in #4427
• NixOS: patch binaries if the dynamic linker is a stub by @GrigorenkoPV in #4413
• Update charon submodule by 15 commits by @tautschnig in #4464
• Arrays with more than 64 elements no longer cause spurious failures by @tautschnig in #4470
• docs: Correct default-unwind Cargo.toml examples by @hashcatHitman in #4496
• Add a section with recommended setup for Rust Analyzer by @zhassan-aws in #4504
• Upgrade Rust toolchain to 2025-11-21 by @tautschnig, @zhassan-aws

New Contributors

• @hashcatHitman made their first contribution in #4496

Full Changelog: kani-0.66.0...kani-0.67.0

Kani Rust verifier release bundle version 0.66.0.

Breaking Changes

• Fail if stub verified doesn't have a contract harness by @carolynzech in #4295

What's Changed

• Add loop invariant support for while let loop by @thanhnguyen-aws in #4279
• Update README by @carolynzech in #4291
• Kani Book Documentation Improvements by @carolynzech in #4296
• Share body cache between harnesses within a codegen unit by @AlexanderPortland in #4276
• Add loop-contracts support for for loop by @thanhnguyen-aws in #4143
• RFC: Partitioned proofs by @AlexanderPortland in #4228
• Handle const generics in stubbing code by @zhassan-aws in #4323
• Replace fxhash with rustc-hash by @zhassan-aws in #4341
• Fix LLBC regressions by @zhassan-aws in #4338
• Combo of small performance changes by @AlexanderPortland in #4314
• Implement BoundedArbitrary for boxed slices by @zhassan-aws in #4340
• Autoharness: use SHA-1 to produce codegen unit file names by @tautschnig in #4370
• Update attributes.md by @0xsecaas in #4376
• Switch macos-13 CI jobs to macos-15-intel by @tautschnig in #4442
• Incrementally update charon submodule with LLBC backend adaptations by @tautschnig in #4445
• Rust toolchain upgraded to 2025-11-05 by @carolynzech, @tautschnig, @thanhnguyen-aws, @zhassan-aws

New Contributors

• @0xsecaas made their first contribution in #4376

Full Changelog: kani-0.65.0...kani-0.66.0

[0.65.0]

Breaking Changes

• Removed unstable list feature and default memory checks by @carolynzech in #4258

Major Changes

• Added support for a few SMT solvers (bitwuzla, cvc5, and z3) as solver attribute values (not packaged with Kani) by @tautschnig in #4218
• Improved support for contracts and stubs in trait implementations, expanding verification capabilities for trait-based code by @carolynzech in #4250
• Added new --prove-safety-only option for focused safety verification, allowing you to concentrate on memory safety and undefined behavior detection by @tautschnig in #4239
• Extended autoharness support to handle references, making it easier to automatically generate verification harnesses by @tautschnig in #4234
• Multiple performance improvements including parallel goto binary writing, lazy debug info evaluation, and optimized quantifier handling for faster verification times

What's Changed

• Fixed issue related to the handling of contract closures which was preventing writing contracts for functions that return mutable references by @vonaka in #4151
• Relaxed the constraint on the pointer type for Kani's memory predicates by @tautschnig in #4193
• Changed the model for ptr_offset_from to enhance verification performance by @tautschnig in #4180
• Fixed assign clause inference bug for nested loops by @thanhnguyen-aws in #4179
• Fixed crash when using multiple quantifiers in one proof by @thanhnguyen-aws in #4221
• Added support for Cargo.toml's default-members configuration by @tautschnig in #4201
• Improved memset handling to avoid zero-count invocations by @tautschnig in #4205
• Enhanced safety by disabling debug assertions under prove-safety-only by @tautschnig in #4262
• Enhanced performance with parallel goto binary writing by @AlexanderPortland in #4236
• Improved quantifier handling performance by avoiding irrelevant symbol updates by @AlexanderPortland in #4268
• Enhanced performance with lazy debug info evaluation by @AlexanderPortland in #4269
• Improved MIR constant handling by marking them as static constants by @vonaka in #4233

New Contributors

• @vonaka made their first contribution in #4151

Version Updates

• Updated to Rust edition 2024 by @tautschnig in #4197
• Rust toolchain upgraded to 2025-08-06 by @tautschnig and @thanhnguyen-aws
• Updated CBMC dependency to 6.7.1 by @tautschnig in #4178

Full Changelog: kani-0.64.0...kani-0.65.0

[0.64.0]

Major Changes

• Add support for loop modifies in loop contracts by @thanhnguyen-aws in #4174
• Autoharness: Derive Arbitrary for structs and enums by @carolynzech in #4167, #4194
• Remove assess subcommand by @carolynzech in #4111

What's Changed

• Fix static union value crash by @thanhnguyen-aws in #4112
• Fix loop invariant historical variables bug by @thanhnguyen-aws in #4150
• Update quantifiers' documentation by @thanhnguyen-aws in #4142
• Optimize goto binary exporting in cprover_bindings by @AlexanderPortland in #4148
• Add the option to generate performance flamegraphs by @AlexanderPortland in #4138
• Introduce compiler timing script & CI job by @AlexanderPortland in #4154
• Optimize reachability with non-mutating global passes by @AlexanderPortland in #4177
• Stub panics during MIR transformation by @AlexanderPortland in #4169
• BoundedArbitrary: Handle enums with zero or one variants by @zhassan-aws in #4171
• Upgrade toolchain to 2025-07-02 by @carolynzech, @tautschnig in #4195

Full Changelog: kani-0.63.0...kani-0.64.0

Kani Rust verifier release bundle version 0.63.0.

Breaking Changes

• Finish deprecating --enable-unstable, --restrict-vtable, and --write-json-symtab by @carolynzech in #4110

Major Changes

• Add support for quantifiers by @qinheping in #3993

What's Changed

• Improvements to autoharness feature:
  • Autoharness argument validation: only error on --quiet if --list was passed by @carolynzech in #4069
  • Autoharness: change pattern options to accept regexes by @carolynzech in #4144
• Target feature changes:
  • Enable target features: x87 and sse2 by @thanhnguyen-aws in #4062
  • Set target features depending on the target architecture by @zhassan-aws in #4127
• Support for quantifiers:
  • Fix the error that Kani panics when there is no external parameter in quantifier's closure. by @thanhnguyen-aws in #4088
  • Gate quantifiers behind an experimental feature by @thanhnguyen-aws in #4141
• Other:
  • Fix the bug: Loop contracts are not composable with function contracts by @thanhnguyen-aws in #3979
  • Add setup scripts for Ubuntu 20.04 by @zhassan-aws in #4082
  • Use our toolchain when invoking cargo metadata by @carolynzech in #4090
  • Fix a bug codegening SwitchInts with only an otherwise branch by @bkirwi in #4095
  • Update kani::mem pointer validity documentation by @carolynzech in #4092
  • Add support for edition 2018 crates using assert! (Fixes #3717) by @sintemal in #4096
  • Handle generic defaults in BoundedArbitrary derives by @zhassan-aws in #4117
  • ty_mangled_name: only use non-mangled name if -Zcffi is enabled. by @carolynzech in #4114
  • Improve Help Menu by @carolynzech in #4109
  • Start stabilizing --jobs and list; deprecate default memory checks by @carolynzech in #4108
  • Refactor simd_bitmask to reduce the number of iterations by @zhassan-aws in #4129
  • Improve linking error output for #[no_std] crates by @AlexanderPortland in #4126
  • Rust toolchain upgraded to 2025-06-03 by @carolynzech @thanhnguyen-aws @zhassan-aws

Full Changelog: kani-0.62.0...kani-0.63.0

Kani Rust verifier release bundle version 0.62.0.

[0.62.0]

What's Changed

• Disable llbc feature by default by @zhassan-aws in #3980
• Add an option to skip codegen by @zhassan-aws in #4002
• Add support for loop-contract historic values by @thanhnguyen-aws in #3951
• Clarify Rust intrinsic assumption error message by @carolynzech in #4015
• Autoharness: enable function-contracts and loop-contracts features by default by @carolynzech in #4016
• Autoharness: Harness Generation Improvements by @carolynzech in #4017
• Add support for Loop-loops by @thanhnguyen-aws in #4011
• Clarify installation instructions by @zhassan-aws in #4023
• Fix the bug of while loop invariant contains no local variables by @thanhnguyen-aws in #4022
• List Subcommand: include crate name by @carolynzech in #4024
• Autoharness: Update Filtering Options by @carolynzech in #4025
• Introduce BoundedArbitrary trait and macro for bounded proofs by @sgpthomas in #4000
• Support trait_upcasting by @clubby789 in #4001
• Analyze unsafe code reachability by @carolynzech in #4037
• Scanner: log crate-level visibility of functions by @tautschnig in #4041
• Autoharness: exit code 1 upon harness failure by @carolynzech in #4043
• Overflow operators can also be used with vectors by @tautschnig in #4049
• Remove bool typedef by @zhassan-aws in #4058
• Update CBMC dependency to 6.6.0 by @qinheping in #4050
• Automatic toolchain upgrade to nightly-2025-04-24 by @zhassan-aws in #4042

New Contributors

• @sgpthomas made their first contribution in #4000
• @clubby789 made their first contribution in #4001

Full Changelog: kani-0.61.0...kani-0.62.0

Kani Rust verifier release bundle version 0.61.0.

[0.61.0]

What's Changed

• Make is_inbounds public by @rajath-mk in #3958
• Finish adding support for f16 and f128 by @carolynzech in #3943
• Support user overrides of Rust built-ins by @tautschnig in #3945
• Add support for anonymous nested statics by @carolynzech in #3953
• Add support for struct field access in loop contracts by @thanhnguyen-aws in #3970
• Autoharness: Don't panic on _ argument by @carolynzech in #3942
• Autoharness: improve metdata printed to terminal and enable standard library application by @carolynzech in #3948, #3952, #3971
• Upgrade toolchain to nightly-2025-04-03 by @qinheping, @tautschnig, @zhassan-aws, @carolynzech in #3988
• Update CBMC dependency to 6.5.0 by @tautschnig in #3936

Full Changelog: kani-0.60.0...kani-0.61.0

Kani Rust verifier release bundle version 0.60.0.

[0.60.0]

Breaking Changes

• Remove Ubuntu 20.04 CI usage by @tautschnig in #3918

Major Changes

• Autoharness Subcommand by @carolynzech in #3874

What's Changed

• Fast fail option - Stop verification process as soon as one failure is observed by @rajath-mk in #3879
• Fail verification for UB regardless of whether #[should_panic] is enabled by @tautschnig in #3860
• Support concrete playback for arrays of length 65 or greater by @carolynzech in #3888
• Remove isize overflow check for zst offsets by @carolynzech in #3897
• Support concrete playback for arrays of length 65 or greater by @carolynzech in #3888
• Autoharness Misc. Improvements by @carolynzech in #3922
• Update toolchain to 2025-03-02 by @remi-delmas-3000 @carolynzech @thanhnguyen-aws @zhassan-aws and @tautschnig

Full Changelog: kani-0.59.0...kani-0.60.0

Kani Rust verifier release bundle version 0.59.0.

Breaking Changes

• Deprecate --enable-unstable and --restrict-vtable by @celinval in #3859
• Do not report arithmetic overflow for floating point operations that produce +/-Inf by @rajath-mk in #3873

What's Changed

• Fix validity checks for char by @celinval in #3853
• Support verifying contracts/stubs for generic types with multiple inherent implementations by @carolynzech in #3829
• Allow multiple stub_verified annotations, but check for duplicate targets by @remi-delmas-3000 in #3808
• Fix crash if a function pointer is created but never used by @celinval in #3862
• Fix transmute codegen when sizes are different by @celinval in #3861
• Stub linker to avoid missing symbols errors by @celinval in #3858
• Toolchain upgrade to nightly-2025-01-28 by @feliperodri @tautschnig

Full Changelog: kani-0.58.0...kani-0.59.0

Kani Rust verifier release bundle version 0.58.0.

Major/Breaking Changes

• Improve --jobs UI by @carolynzech in #3790
• Generate contracts of dependencies as assertions by @carolynzech in #3802
• Add UB checks for ptr_offset_from* intrinsics by @celinval in #3757

What's Changed

• Include manifest-path when checking if packages are in the workspace by @qinheping in #3819
• Update kissat to v4.0.1 by @remi-delmas-3000 in #3791
• Rust toolchain upgraded to 2025-01-07 by @remi-delmas-3000 @zhassan-aws

Full Changelog: kani-0.57.0...kani-0.58.0