kani-0.64.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-0.63.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-0.62.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-0.61.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-0.60.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-0.59.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-0.58.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

kani-0.57.0

Major Changes

• 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

Breaking Changes

• 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

What's Changed

• 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: kani-0.56.0...kani-0.57.0

kani-0.56.0

Major/Breaking Changes

• 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

What's Changed

• 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: kani-0.55.0...kani-0.56.0

kani-0.55.0

Kani Rust verifier release bundle version 0.55.0.

Major/Breaking Changes

• 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!

What's Changed

• 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: kani-0.54.0...kani-0.55.0