This file contains notable changes (e.g. breaking changes, major changes, etc.) in Kani releases.

This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards.

• 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

• @hashcatHitman made their first contribution in #4496

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.66.0...kani-0.67.0

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

• 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

• @0xsecaas made their first contribution in #4376

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.65.0...kani-0.66.0

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

• 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

• 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

• @vonaka made their first contribution in #4151

• 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: https://github.com/model-checking/kani/compare/kani-0.64.0...kani-0.65.0

• 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

• 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: https://github.com/model-checking/kani/compare/kani-0.63.0...kani-0.64.0

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

• Add support for quantifiers by @qinheping in #3993

• 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: https://github.com/model-checking/kani/compare/kani-0.62.0...kani-0.63.0

• 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

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

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.61.0...kani-0.62.0

• 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: https://github.com/model-checking/kani/compare/kani-0.60.0...kani-0.61.0

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

• Autoharness Subcommand by @carolynzech in #3874

• 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: https://github.com/model-checking/kani/compare/kani-0.59.0...kani-0.60.0

• 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

• 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: https://github.com/model-checking/kani/compare/kani-0.58.0...kani-0.59.0

• 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

• 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: https://github.com/model-checking/kani/compare/kani-0.57.0...kani-0.58.0

• kani-cov: A coverage tool for Kani by @adpaco-aws in #3121
• Add a timeout option by @zhassan-aws in #3649
• Loop Contracts Annotation for While-Loop by @qinheping in #3151
• Harness output individual files by @Alexander-Aghili in #3360
• Enable support for Ubuntu 24.04 by @tautschnig in #3758

• Make kani::check private by @celinval in #3614
• Remove symtab json support by @celinval in #3695
• Remove CBMC viewer and visualize option by @zhassan-aws in #3699
• Dropping support for Ubuntu 18.04 / AL2. by @thanhnguyen-aws in #3744

• Remove the overflow checks for wrapping_offset by @zhassan-aws in #3589
• Support fully-qualified --package arguments by @celinval in #3593
• Implement proper function pointer handling for validity checks by @celinval in #3606
• Add fn that checks pointers point to same allocation by @celinval in #3583
• [Lean back-end] Preserve variable names by @zhassan-aws in #3560
• Emit an error when proof_for_contract function is not found by @zhassan-aws in #3609
• [Lean back-end] Rename user-facing options from Aeneas to Lean by @zhassan-aws in #3630
• Fix ICE due to mishandling of Aggregate rvalue for raw pointers to trait objects by @carolynzech in #3636
• Fix loop contracts transformation when loops in branching by @qinheping in #3640
• Move any_slice_from_array to kani_core by @qinheping in #3646
• Implement Arbitrary for Range* by @c410-f3r in #3666
• Add support for float_to_int_unchecked by @zhassan-aws in #3660
• Change same_allocation to accept wide pointers by @celinval in #3684
• Derive Arbitrary for enums with a single variant by @AlgebraicWolf in #3692
• Apply loop contracts only if there exists some usage by @qinheping in #3694
• Add support for f16 and f128 in float_to_int_unchecked intrinsic by @zhassan-aws in #3701
• Fix codegen for rvalue aggregate raw pointer to an adt with slice tail by @carolynzech in #3644
• Improve Kani handling of function markers by @celinval in #3718
• Enable contracts for const generic functions by @qinheping in #3726
• List Subcommand Improvements by @carolynzech in #3729
• [Lean back-end] add support for enum, struct, tuple in llbc backend by @thanhnguyen-aws in #3721
• Fix issues with how we compute DST size by @celinval in #3687
• Fix size and alignment computation for intrinsics by @celinval in #3734
• Add a Kani function that checks if the range of a float is valid for conversion to int by @zhassan-aws in #3742
• Add out of bounds check for offset intrinsics by @celinval in #3755
• Automatic upgrade of CBMC from 6.3.1 to 6.4.1
• Rust toolchain upgraded to nightly-2024-12-15 by @zhassan-aws @carolynzech @qinheping @celinval @tautschnig

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.56.0...kani-0.57.0

• Remove obsolete linker options (--mir-linker and --legacy-linker) by @zhassan-aws in #3559
• List Subcommand by @carolynzech in #3523
• Deprecate kani::check by @celinval in #3557

• Enable stubbing and function contracts for primitive types by @celinval in #3496
• Instrument validity checks for pointer to reference casts for slices and str's by @zhassan-aws in #3513
• Fail compilation if proof_for_contract is added to generic function by @carolynzech in #3522
• Fix storing coverage data in cargo projects by @adpaco-aws in #3527
• Add experimental API to generate arbitrary pointers by @celinval in #3538
• Running verify-std no longer changes Cargo files by @celinval in #3577
• Add an LLBC backend by @zhassan-aws in #3514
• Fix the computation of the number of bytes of a pointer offset by @zhassan-aws in #3584
• Rust toolchain upgraded to nightly-2024-10-03 by @qinheping @tautschnig @celinval
• CBMC upgraded to 6.3.1 by @tautschnig in #3537

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.55.0...kani-0.56.0

• Coverage reporting in Kani is now source-based instead of line-based. Consequently, the unstable -Zline-coverage flag has been replaced with a -Zsource-coverage one. Check the Source-Coverage RFC for more details.
• Several improvements were made to the memory initialization checks. The current state is summarized in #3300. We welcome your feedback!

• Update CBMC build instructions for Amazon Linux 2 by @tautschnig in #3431
• Implement memory initialization state copy functionality by @artemagvanian in #3350
• Make points-to analysis handle all intrinsics explicitly by @artemagvanian in #3452
• Avoid corner-cases by grouping instrumentation into basic blocks and using backward iteration by @artemagvanian in #3438
• Fix ICE due to mishandling of Aggregate rvalue for raw pointers to str by @celinval in #3448
• Basic support for memory initialization checks for unions by @artemagvanian in #3444
• Adopt Rust's source-based code coverage instrumentation by @adpaco-aws in #3119
• Extra tests and bug fixes to the delayed UB instrumentation by @artemagvanian in #3419
• Partially integrate uninit memory checks into verify_std by @artemagvanian in #3470
• Rust toolchain upgraded to nightly-2024-09-03 by @jaisnan @carolynzech

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.54.0...kani-0.55.0

• We added support for slices in the #[kani::modifies(...)] clauses when using function contracts.
• We introduce an #[safety_constraint(...)] attribute helper for the Arbitrary and Invariant macros.
• We enabled support for concrete playback for harness that contains stubs or function contracts.
• We added support for log2*, log10*, powif*, fma*, and sqrt* intrisincs.

• The -Z ptr-to-ref-cast-checks option has been removed, and pointer validity checks when casting raw pointers to references are now run by default.

• Make Kani reject mutable pointer casts if padding is incompatible and memory initialization is checked by @artemagvanian in #3332
• Fix visibility of some Kani intrinsics by @artemagvanian in #3323
• Function Contracts: Modify Slices by @pi314mm in #3295
• Support for disabling automatically generated pointer checks to avoid reinstrumentation by @artemagvanian in #3344
• Add support for global transformations by @artemagvanian in #3348
• Enable an #[safety_constraint(...)] attribute helper for the Arbitrary and Invariant macros by @adpaco-aws in #3283
• Fix contract handling of promoted constants and constant static by @celinval in #3305
• Bump CBMC Viewer to 3.9 by @tautschnig in #3373
• Update to CBMC version 6.1.1 by @tautschnig in #2995
• Define a struct-level #[safety_constraint(...)] attribute by @adpaco-aws in #3270
• Enable concrete playback for contract and stubs by @celinval in #3389
• Add code scanner tool by @celinval in #3120
• Enable contracts in associated functions by @celinval in #3363
• Enable log2*, log10* intrinsics by @tautschnig in #3001
• Enable powif* intrinsics by @tautschnig in #2999
• Enable fma* intrinsics by @tautschnig in #3002
• Enable sqrt* intrinsics by @tautschnig in #3000
• Remove assigns clause for ZST pointers by @carolynzech in #3417
• Instrumentation for delayed UB stemming from uninitialized memory by @artemagvanian in #3374
• Unify kani library and kani core logic by @jaisnan in #3333
• Stabilize pointer-to-reference cast validity checks by @artemagvanian in #3426
• Rust toolchain upgraded to nightly-2024-08-07 by @jaisnan @qinheping @tautschnig @feliperodri

• @carolynzech made their first contribution in #3387

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.53.0...kani-0.54.0

• The --visualize option is being deprecated and will be removed in a future release. Consider using the --concrete-playback option instead.
• The -Z ptr-to-ref-cast-checks option is being introduced to check pointer validity when casting raw pointers to references. The feature is currently behind an unstable flag but is expected to be stabilized in a future release once remaining performance issues have been resolved.
• The -Z uninit-checks option is being introduced to check memory initialization. The feature is currently behind an unstable flag and also requires the -Z ghost-state option.

• Remove support for the unstable argument --function by @celinval in #3278
• Remove deprecated --enable-stubbing by @celinval in #3309

• Change ensures into closures by @pi314mm in #3207
• (Re)introduce Invariant trait by @adpaco-aws in #3190
• Remove empty box creation from contracts impl by @celinval in #3233
• Add a new verify-std subcommand to Kani by @celinval in #3231
• Inject pointer validity check when casting raw pointers to references by @artemagvanian in #3221
• Do not turn trivially diverging loops into assume(false) by @tautschnig in #3223
• Fix "unused mut" warnings created by generated code. by @jsalzbergedu in #3247
• Refactor stubbing so Kani compiler only invoke rustc once per crate by @celinval in #3245
• Use cfg=kani_host for host crates by @tautschnig in #3244
• Add intrinsics and Arbitrary support for no_core by @jaisnan in #3230
• Contracts: Avoid attribute duplication and const function generation for constant function by @celinval in #3255
• Fix contract of constant fn with effect feature by @celinval in #3259
• Fix typed_swap for ZSTs by @tautschnig in #3256
• Add a #[derive(Invariant)] macro by @adpaco-aws in #3250
• Contracts: History Expressions via "old" monad by @pi314mm in #3232
• Function Contracts: remove instances of _renamed by @pi314mm in #3274
• Deprecate --visualize in favor of concrete playback by @celinval in #3281
• Fix operand in fat pointer comparison by @pi314mm in #3297
• Function Contracts: Closure Type Inference by @pi314mm in #3307
• Add support for f16 and f128 for toolchain upgrade to 6/28 by @jaisnan in #3306
• Towards Proving Memory Initialization by @artemagvanian in #3264
• Rust toolchain upgraded to nightly-2024-07-01 by @tautschnig @celinval @jaisnan @adpaco-aws

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.52.0...kani-0.53.0

• New section about linter configuraton checking in the doc by @remi-delmas-3000 in #3198
• Fix {,e}println!() by @GrigorenkoPV in #3209
• Contracts for a few core functions by @celinval in #3107
• Add simple API for shadow memory by @zhassan-aws in #3200
• Upgrade Rust toolchain to 2024-05-28 by @zhassan-aws @remi-delmas-3000 @qinheping

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.51.0...kani-0.52.0

• Do not assume that ZST-typed symbols refer to unique objects by @tautschnig in #3134
• Remove kani::Arbitrary from the modifies contract instrumentation by @feliperodri in #3169
• Emit source locations whenever possible to ease debugging and coverage reporting by @tautschnig in #3173
• Rust toolchain upgraded to nightly-2024-04-21 by @celinval

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.50.0...kani-0.51.0

• Fix compilation issue with proc_macro2 (v1.0.80+) and Kani v0.49.0 (#3138).

• Implement valid value check for write_bytes by @celinval in #3108
• Rust toolchain upgraded to 2024-04-15 by @tautschnig @celinval

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.49.0...kani-0.50.0

• Disable removal of storage markers by @zhassan-aws in #3083
• Ensure storage markers are kept in std code by @zhassan-aws in #3080
• Implement validity checks by @celinval in #3085
• Allow modifies clause for verification only by @feliperodri in #3098
• Add optional scatterplot to benchcomp output by @tautschnig in #3077
• Expand ${var} in benchcomp variant env by @karkhaz in #3090
• Add benchcomp filter command by @karkhaz in #3105
• Upgrade Rust toolchain to 2024-03-29 by @zhassan-aws @celinval @adpaco-aws @feliperodri

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.48.0...kani-0.49.0

• We fixed a soundness bug that in some cases may cause Kani to not detect a use-after-free issue in #3063

• Fix codegen_atomic_binop for atomic_ptr by @qinheping in #3047
• Retrieve info for recursion tracker reliably by @feliperodri in #3045
• Add --use-local-toolchain to Kani setup by @jaisnan in #3056
• Replace internal reverse_postorder by a stable one by @celinval in #3064
• Add option to override --crate-name from kani by @adpaco-aws in #3054
• Rust toolchain upgraded to 2024-03-11 by @adpaco-ws @celinval @zyadh

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.47.0...kani-0.48.0

• Upgrade toolchain to 2024-02-14 by @zhassan-aws in #3036

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.46.0...kani-0.47.0

• modifies Clauses for Function Contracts by @JustusAdam in #2800
• Fix ICEs due to mismatched arguments by @celinval in #2994. Resolves the following issues:
  • #2260
  • #2312
• Enable powf*, exp*, log* intrinsics by @tautschnig in #2996
• Upgrade Rust toolchain to nightly-2024-01-24 by @celinval @feliperodri @qinheping

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.45.0...kani-0.46.0

• Upgrade toolchain to nightly-2024-01-17 by @celinval in #2976

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.44.0...kani-0.45.0

• Rust toolchain upgraded to nightly-2024-01-08 by @adpaco-aws @celinval @zhassan-aws

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.43.0...kani-0.44.0

• Rust toolchain upgraded to nightly-2023-12-14 by @tautschnig and @adpaco-aws

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.42.0...kani-0.43.0

• Build CBMC from source and install as package on non-x86_64 by @bennofs in #2877 and #2878
• Emit suggestions and an explanation when CBMC runs out of memory by @JustusAdam in #2885
• Rust toolchain upgraded to nightly-2023-11-28 by @celinval

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.41.0...kani-0.42.0

• Set minimum python to 3.7 in docker container and release action by @remi-delmas-3000 in #2879
• Delete any_slice which has been deprecated since Kani 0.38.0. by @zhassan-aws in #2860

• Make cover const by @jswrenn in #2867
• Change expect() from taking formatted strings to use unwrap_or_else() by @matthiaskrgr in #2865
• Fix setup for aarch64-unknown-linux-gnu platform by @adpaco-aws in #2864
• Do not override std library during playback by @celinval in #2852
• Rust toolchain upgraded to nightly-2023-11-11 by @zhassan-aws

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.40.0...kani-0.41.0

• Ease setup in Amazon Linux 2 by @adpaco-aws in #2833
• Propagate backend options into goto-synthesizer by @qinheping in #2643
• Update CBMC version to 5.95.1 by @adpaco-aws in #2844
• Rust toolchain upgraded to nightly-2023-10-31 by @jaisnan @adpaco-aws

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.39.0...kani-0.40.0

• Limit --exclude to workspace packages by @tautschnig in #2808
• Fix panic warning and add arbitrary Duration by @celinval in #2820
• Update CBMC version to 5.94 by @celinval in #2821
• Rust toolchain upgraded to nightly-2023-10-17 by @celinval @tautschnig

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.38.0...kani-0.39.0

• Deprecate any_slice by @zhassan-aws in #2789

• Provide better error message for invalid stubs by @JustusAdam in #2787
• Simple Stubbing with Contracts by @JustusAdam in #2746
• Avoid mismatch when generating structs that represent scalar data but also include ZSTs by @adpaco-aws in #2794
• Prevent kani crash during setup for first time by @jaisnan in #2799
• Create concrete playback temp files in source directory by @tautschnig in #2804
• Bump CBMC version by @zhassan-aws in #2796
• Update Rust toolchain to 2023-09-23 by @tautschnig in #2806

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.37.0...kani-0.38.0

• Delete obsolete stubs for Vec and related options by @zhassan-aws in #2770
• Add support for the ARM64 Linux platform by @adpaco-aws in #2757

• Function Contracts: Support for defining and checking requires and ensures clauses by @JustusAdam in #2655
• Force any_vec capacity to match length by @celinval in #2765
• Fix expected value for pref_align_of under aarch64/macos by @remi-delmas-3000 in #2782
• Bump CBMC version to 5.92.0 by @zhassan-aws in #2771
• Upgrade to Kissat 3.1.1 by @zhassan-aws in #2756
• Rust toolchain upgraded to nightly-2023-09-19 by @remi-delmas-3000 @tautschnig

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.36.0...kani-0.37.0

• Enable -Z stubbing and error out instead of ignoring stub by @celinval in #2678
• Enable concrete playback for failure of UB checks by @zhassan-aws in #2727
• Bump CBMC version to 5.91.0 by @adpaco-aws in #2733
• Rust toolchain upgraded to nightly-2023-09-06 by @celinval @jaisnan @adpaco-aws

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.35.0...kani-0.36.0

• Add support to simd_bitmask by @celinval in #2677
• Add integer overflow checking for simd_div and simd_rem by @reisnera in #2645
• Bump CBMC version by @zhassan-aws in #2702
• Upgrade Rust toolchain to 2023-08-19 by @zhassan-aws in #2696

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.34.0...kani-0.35.0

• Change default solver to CaDiCaL by @celinval in #2557 By default, Kani will now run CBMC with CaDiCaL, since this solver has outperformed Minisat in most of our benchmarks. User's should still be able to select Minisat (or a different solver) either by using #[solver] harness attribute, or by passing --solver=<SOLVER> command line option.

• Allow specifying the scheduling strategy in #[kani_proof] for async functions by @fzaiser in #1661
• Support for stubbing out foreign functions by @feliperodri in #2658
• Coverage reporting without a need for cbmc-viewer by @adpaco-aws in #2609
• Add support to array-based SIMD by @celinval in #2633
• Add unchecked/SIMD bitshift checks and disable CBMC flag by @reisnera in #2630
• Fix codegen of constant byte slices to address spurious verification failures by @zhassan in #2663
• Bump CBMC to v5.89.0 by @remi-delmas-3000 in #2662
• Update Rust toolchain to nightly 2023-08-04 by @remi-delmas-3000 in #2661

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.33.0...kani-0.34.0

• Add support for sysconf by @feliperodri in #2557
• Print Kani version by @adpaco-aws in #2619
• Upgrade Rust toolchain to nightly-2023-07-01 by @qinheping in #2616
• Bump CBMC version to 5.88.1 by @zhassan-aws in #2623

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.32.0...kani-0.33.0

• Add kani::spawn and an executor to the Kani library by @fzaiser in #1659
• Add "kani" configuration key to enable conditional compilation in build scripts by @celinval in #2297
• Adds posix_memalign to the list of supported builtins by @feliperodri in #2601
• Upgrade rust toolchain to nightly-2023-06-20 by @celinval in #2551
• Update rust toolchain to 2023-06-22 by @celinval in #2588
• Automatic toolchain upgrade to nightly-2023-06-24 by @github-actions in #2600
• Bump CBMC version to 5.87.0 by @adpaco-aws in #2598

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.31.0...kani-0.32.0

• Add --exact flag by @jaisnan in #2527
• Build the verification libraries using Kani compiler by @celinval in #2534
• Verify all Kani attributes in all crate items upfront by @celinval in #2536
• Update README.md - fix link locations for badge images in markdown by @phayes in #2537
• Bump CBMC version to 5.86.0 by @zhassan-aws in #2561

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.30.0...kani-0.31.0

• Remove --harness requirement from stubbing by @celinval in #2495
• Add target selection for cargo kani by @celinval in #2507
• Generate Multiple playback harnesses when multiple crashes exist in a single harness. by @YoshikiTakashima in #2496
• Escape Zero-size types in playback by @YoshikiTakashima in #2508
• Do not crash when rustfmt fails. by @YoshikiTakashima in #2511
• De-duplicate same input injections for the same harness. by @YoshikiTakashima in #2513
• Update Cbmc version by @celinval in #2512
• Upgrade rust toolchain to 2023-04-30 by @zhassan-aws in #2456

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.29.0...kani-0.30.0

• Create a playback command to make it easier to run Kani generated tests (pull request by @celinval)

• Fix symtab json file removal and reduce regression scope (pull request by @celinval)
• Fix regression on concrete playback inplace (pull request by @celinval)
• Fix static variable initialization when they have the same value (pull request by @celinval)
• Improve assess and regression time (pull request by @celinval)
• Fix playback with build scripts (pull request by @celinval)
• Delay printing playback harness until after verification status (pull request by @YoshikiTakashima)
• Update rust toolchain to 2023-04-29 (pull request by @zhassan-aws)
• Bump CBMC version to 5.84.0 (pull request by @tautschn)

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.28.0...kani-0.29.0

• The unstable --c-lib option now requires -Z c-ffi to enable C-FFI support by @celinval in #2425

• Enforce unstable APIs can only be used if the related feature is enabled by @celinval in #2386
• Get rid of the legacy mode by @celinval in #2427
• Limit FFI calls by default to explicitly supported ones by @celinval in #2428
• Fix the order of operands for generator structs by @zhassan-aws in #2436
• Add a few options to dump the reachability graph (debug only) by @celinval in #2433
• Perform reachability analysis on a per-harness basis by @celinval in #2439
• Bump CBMC version to 5.83.0 by @zhassan-aws in #2441
• Upgrade the toolchain to nightly-2023-04-16 by @celinval in #2406

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.27.0...kani-0.28.0

• Allow excluding packages from verification with --exclude by @adpaco-aws in #2399
• Add size_of annotation to help CBMC's allocator by @tautschnig in #2395
• Implement kani::Arbitrary for Box<T> by @adpaco-aws in #2404
• Use optimized overflow operation everywhere by @celinval in #2405
• Print compilation stats in verbose mode by @celinval in #2420
• Bump CBMC version to 5.82.0 by @adpaco-aws in #2417

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.26.0...kani-0.27.0

• The Kani reference now includes an "Attributes" section that describes each of the attributes available in Kani (pull request by @adpaco-aws)
• Users' choice of SAT solver, specified by the solver attribute, is now propagated to the loop-contract synthesizer (pull request by @qinheping)
• Unit tests generated by the concrete playback feature now compile correctly when using RUSTFLAGS="--cfg=kani" (pull request by @jaisnan)
• The Rust toolchain is updated to 2023-02-18 (pull request by @tautschnig)

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.25.0...kani-0.26.0

• Add implementation for the #[kani::should_panic] attribute by @adpaco-aws in #2315
• Upgrade Rust toolchain to nightly-2023-02-04 by @tautschnig in #2324
• Bump CBMC version to 5.80.0 by @zhassan-aws in #2336

Full Changelog: https://github.com/model-checking/kani/compare/kani-0.24.0...kani-0.25.0

• Remove the second parameter in the kani::any_where function by @zhassan-aws in #2257 We removed the second parameter in the kani::any_where function (_msg: &'static str) to make the function more ergonomic to use. We suggest moving the explanation for why the assumption is introduced into a comment. For example, the following code:

    let len: usize = kani::any_where(|x| *x < 5, "Restrict the length to a value less than 5");

should be replaced by:

    // Restrict the length to a value less than 5
    let len: usize = kani::any_where(|x| *x < 5);

• Enable the build cache to avoid recompiling crates that haven't changed, and introduce --force-build option to compile all crates from scratch by @celinval in #2232.