diff --git a/CHANGELOG.md b/CHANGELOG.md
index e35af4c8fa24..23d740f534a9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -4,6 +4,27 @@ This file contains notable changes (e.g. breaking changes, major changes, etc.)
 
 This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards.
 
+## [0.56.0]
+
+### Breaking Changes
+
+* Remove obsolete linker options (`--mir-linker` and `--legacy-linker`) by @zhassan-aws in https://github.com/model-checking/kani/pull/3559
+* Deprecate `kani::check` by @celinval in https://github.com/model-checking/kani/pull/3557
+
+### What's Changed
+
+* Enable stubbing and function contracts for primitive types by @celinval in https://github.com/model-checking/kani/pull/3496
+* Instrument validity checks for pointer to reference casts for slices and str's by @zhassan-aws in https://github.com/model-checking/kani/pull/3513
+* Fail compilation if `proof_for_contract` is added to generic function by @carolynzech in https://github.com/model-checking/kani/pull/3522
+* Fix storing coverage data in cargo projects by @adpaco-aws in https://github.com/model-checking/kani/pull/3527
+* Add experimental API to generate arbitrary pointers by @celinval in https://github.com/model-checking/kani/pull/3538
+* Running `verify-std` no longer changes Cargo files by @celinval in https://github.com/model-checking/kani/pull/3577
+* Add an LLBC backend by @zhassan-aws in https://github.com/model-checking/kani/pull/3514
+* Rust toolchain upgraded to nightly-2024-10-03 by @qinheping @tautschnig @celinval
+* CBMC upgraded to 6.3.1 by @tautschnig in https://github.com/model-checking/kani/pull/3537
+
+**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.55.0...kani-0.56.0
+
 ## [0.55.0]
 
 ### Major/Breaking Changes
diff --git a/Cargo.lock b/Cargo.lock
index 41fb02073f6a..21997d7bc332 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -2,21 +2,6 @@
 # It is not intended for manual editing.
 version = 4
 
-[[package]]
-name = "addr2line"
-version = "0.24.2"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "dfbe277e56a376000877090da837660b4427aad530e3028d44e0bffe4f89a1c1"
-dependencies = [
- "gimli",
-]
-
-[[package]]
-name = "adler2"
-version = "2.0.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "512761e0bb2578dd7380c6baaa0f4ce03e84f95e960231d1dec8bf4d7d6e2627"
-
 [[package]]
 name = "ahash"
 version = "0.8.11"
@@ -39,15 +24,6 @@ dependencies = [
  "memchr",
 ]
 
-[[package]]
-name = "ansi_term"
-version = "0.12.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d52a9bb7ec0cf484c551830a7ce27bd20d67eac647e1befb56b0be4ee39a55d2"
-dependencies = [
- "winapi",
-]
-
 [[package]]
 name = "anstream"
 version = "0.6.15"
@@ -131,59 +107,12 @@ dependencies = [
  "wait-timeout",
 ]
 
-[[package]]
-name = "assert_tokens_eq"
-version = "0.1.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6b21f4c5ba5c8b55031306325f196df925939bcc2bd7188ce68fabd93fb4f149"
-dependencies = [
- "ansi_term",
- "ctor",
- "difference",
- "output_vt100",
- "snafu",
-]
-
 [[package]]
 name = "autocfg"
 version = "1.4.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "ace50bade8e6234aa140d9a2f552bbee1db4d353f69b8217bc503490fc1a9f26"
 
-[[package]]
-name = "backtrace"
-version = "0.3.74"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8d82cb332cdfaed17ae235a638438ac4d4839913cc2af585c3c6746e8f8bee1a"
-dependencies = [
- "addr2line",
- "cfg-if",
- "libc",
- "miniz_oxide",
- "object",
- "rustc-demangle",
- "windows-targets 0.52.6",
-]
-
-[[package]]
-name = "bincode"
-version = "2.0.0-rc.3"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f11ea1a0346b94ef188834a65c068a03aec181c94896d481d7a0a40d85b0ce95"
-dependencies = [
- "bincode_derive",
- "serde",
-]
-
-[[package]]
-name = "bincode_derive"
-version = "2.0.0-rc.3"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7e30759b3b99a1b802a7a3aa21c85c3ded5c28e1c83170d82d70f08bbf7f3e4c"
-dependencies = [
- "virtue",
-]
-
 [[package]]
 name = "bitflags"
 version = "2.6.0"
@@ -221,7 +150,7 @@ dependencies = [
 
 [[package]]
 name = "build-kani"
-version = "0.55.0"
+version = "0.56.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
@@ -295,14 +224,11 @@ dependencies = [
  "derive-visitor",
  "env_logger",
  "hashlink",
- "hax-frontend-exporter",
- "ignore",
  "im",
  "index_vec",
  "indoc",
  "itertools 0.13.0",
  "lazy_static",
- "libtest-mimic",
  "log",
  "macros",
  "nom",
@@ -315,15 +241,12 @@ dependencies = [
  "serde-map-to-array",
  "serde_json",
  "serde_stacker",
- "snapbox",
  "stacker",
  "take_mut",
- "tempfile",
  "toml",
  "tracing",
  "tracing-subscriber",
  "tracing-tree 0.3.1",
- "walkdir",
  "which",
 ]
 
@@ -356,8 +279,8 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "4ac6a0c7b1a9e9a5186361f67dfa1b88213572f427fb9ab038efb2bd8c582dab"
 dependencies = [
  "heck",
- "proc-macro2 1.0.86",
- "quote 1.0.37",
+ "proc-macro2",
+ "quote",
  "syn 2.0.79",
 ]
 
@@ -442,7 +365,7 @@ dependencies = [
 
 [[package]]
 name = "cprover_bindings"
-version = "0.55.0"
+version = "0.56.0"
 dependencies = [
  "lazy_static",
  "linear-map",
@@ -523,16 +446,6 @@ dependencies = [
  "memchr",
 ]
 
-[[package]]
-name = "ctor"
-version = "0.1.26"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6d2301688392eb071b0bf1a37be05c469d3cc4dbbd95df672fe28ab021e6a096"
-dependencies = [
- "quote 1.0.37",
- "syn 1.0.109",
-]
-
 [[package]]
 name = "deranged"
 version = "0.3.11"
@@ -548,8 +461,8 @@ version = "2.2.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "fcc3dd5e9e9c0b295d6e1e4d811fb6f157d5ffd784b8d202fc62eac8035a770b"
 dependencies = [
- "proc-macro2 1.0.86",
- "quote 1.0.37",
+ "proc-macro2",
+ "quote",
  "syn 1.0.109",
 ]
 
@@ -570,17 +483,11 @@ checksum = "427b39a85fecafea16b1a5f3f50437151022e35eb4fe038107f08adbf7f8def6"
 dependencies = [
  "convert_case 0.4.0",
  "itertools 0.10.5",
- "proc-macro2 1.0.86",
- "quote 1.0.37",
+ "proc-macro2",
+ "quote",
  "syn 1.0.109",
 ]
 
-[[package]]
-name = "difference"
-version = "2.0.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "524cbf6897b527295dff137cec09ecf3a05f4fddffd7dfcd1585403449e74198"
-
 [[package]]
 name = "difflib"
 version = "0.4.0"
@@ -593,12 +500,6 @@ version = "0.3.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "fea41bba32d969b513997752735605054bc0dfa92b4c56bf1189f2e174be7a10"
 
-[[package]]
-name = "dyn-clone"
-version = "1.0.17"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0d6ef0072f8a535281e4876be788938b528e9a1d43900b82c2569af7da799125"
-
 [[package]]
 name = "either"
 version = "1.13.0"
@@ -650,41 +551,6 @@ dependencies = [
  "windows-sys 0.52.0",
 ]
 
-[[package]]
-name = "escape8259"
-version = "0.5.3"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5692dd7b5a1978a5aeb0ce83b7655c58ca8efdcb79d21036ea249da95afec2c6"
-
-[[package]]
-name = "ext-trait"
-version = "1.0.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d772df1c1a777963712fb68e014235e80863d6a91a85c4e06ba2d16243a310e5"
-dependencies = [
- "ext-trait-proc_macros",
-]
-
-[[package]]
-name = "ext-trait-proc_macros"
-version = "1.0.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1ab7934152eaf26aa5aa9f7371408ad5af4c31357073c9e84c3b9d7f11ad639a"
-dependencies = [
- "proc-macro2 1.0.86",
- "quote 1.0.37",
- "syn 1.0.109",
-]
-
-[[package]]
-name = "extension-traits"
-version = "1.0.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a296e5a895621edf9fa8329c83aa1cb69a964643e36cf54d8d7a69b789089537"
-dependencies = [
- "ext-trait",
-]
-
 [[package]]
 name = "fastrand"
 version = "2.1.1"
@@ -717,31 +583,12 @@ dependencies = [
  "wasi",
 ]
 
-[[package]]
-name = "gimli"
-version = "0.31.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "07e28edb80900c19c28f1072f2e8aeca7fa06b23cd4169cefe1af5aa3260783f"
-
 [[package]]
 name = "glob"
 version = "0.3.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "d2fabcfbdc87f4758337ca535fb41a6d701b65693ce38287d856d1674551ec9b"
 
-[[package]]
-name = "globset"
-version = "0.4.15"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "15f1ce686646e7f1e19bf7d5533fe443a45dbfb990e00629110797578b42fb19"
-dependencies = [
- "aho-corasick",
- "bstr",
- "log",
- "regex-automata 0.4.8",
- "regex-syntax 0.8.5",
-]
-
 [[package]]
 name = "graph-cycles"
 version = "0.1.0"
@@ -778,59 +625,12 @@ dependencies = [
  "serde",
 ]
 
-[[package]]
-name = "hax-adt-into"
-version = "0.1.0-alpha.1"
-source = "git+https://github.com/hacspec/hax?branch=main#496e381186de242f46ee2fd2b4b8971c70aa07a4"
-dependencies = [
- "itertools 0.11.0",
- "proc-macro2 1.0.86",
- "quote 1.0.37",
- "syn 1.0.109",
-]
-
-[[package]]
-name = "hax-frontend-exporter"
-version = "0.1.0-alpha.1"
-source = "git+https://github.com/hacspec/hax?branch=main#496e381186de242f46ee2fd2b4b8971c70aa07a4"
-dependencies = [
- "bincode",
- "extension-traits",
- "hax-adt-into",
- "hax-frontend-exporter-options",
- "itertools 0.11.0",
- "lazy_static",
- "paste",
- "schemars",
- "serde",
- "serde_json",
- "tracing",
-]
-
-[[package]]
-name = "hax-frontend-exporter-options"
-version = "0.1.0-alpha.1"
-source = "git+https://github.com/hacspec/hax?branch=main#496e381186de242f46ee2fd2b4b8971c70aa07a4"
-dependencies = [
- "bincode",
- "hax-adt-into",
- "schemars",
- "serde",
- "serde_json",
-]
-
 [[package]]
 name = "heck"
 version = "0.5.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea"
 
-[[package]]
-name = "hermit-abi"
-version = "0.3.9"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d231dfb89cfffdbc30e7fc41579ed6066ad03abda9e567ccafae602b97ec5024"
-
 [[package]]
 name = "home"
 version = "0.5.9"
@@ -846,22 +646,6 @@ version = "2.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4"
 
-[[package]]
-name = "ignore"
-version = "0.4.23"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6d89fd380afde86567dfba715db065673989d6253f42b88179abd3eae47bda4b"
-dependencies = [
- "crossbeam-deque",
- "globset",
- "log",
- "memchr",
- "regex-automata 0.4.8",
- "same-file",
- "walkdir",
- "winapi-util",
-]
-
 [[package]]
 name = "im"
 version = "15.1.0"
@@ -922,15 +706,6 @@ dependencies = [
  "either",
 ]
 
-[[package]]
-name = "itertools"
-version = "0.11.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b1c173a5686ce8bfa551b3563d0c2170bf24ca44da99c7ca4bfdab5418c3fe57"
-dependencies = [
- "either",
-]
-
 [[package]]
 name = "itertools"
 version = "0.13.0"
@@ -954,7 +729,7 @@ checksum = "72167d68f5fce3b8655487b8038691a3c9984ee769590f93f2a631f4ad64e4f5"
 
 [[package]]
 name = "kani"
-version = "0.55.0"
+version = "0.56.0"
 dependencies = [
  "kani_core",
  "kani_macros",
@@ -962,7 +737,7 @@ dependencies = [
 
 [[package]]
 name = "kani-compiler"
-version = "0.55.0"
+version = "0.56.0"
 dependencies = [
  "charon",
  "clap",
@@ -972,7 +747,7 @@ dependencies = [
  "kani_metadata",
  "lazy_static",
  "num",
- "quote 1.0.37",
+ "quote",
  "regex",
  "serde",
  "serde_json",
@@ -987,7 +762,7 @@ dependencies = [
 
 [[package]]
 name = "kani-driver"
-version = "0.55.0"
+version = "0.56.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
@@ -1016,7 +791,7 @@ dependencies = [
 
 [[package]]
 name = "kani-verifier"
-version = "0.55.0"
+version = "0.56.0"
 dependencies = [
  "anyhow",
  "home",
@@ -1025,24 +800,24 @@ dependencies = [
 
 [[package]]
 name = "kani_core"
-version = "0.55.0"
+version = "0.56.0"
 dependencies = [
  "kani_macros",
 ]
 
 [[package]]
 name = "kani_macros"
-version = "0.55.0"
+version = "0.56.0"
 dependencies = [
  "proc-macro-error2",
- "proc-macro2 1.0.86",
- "quote 1.0.37",
+ "proc-macro2",
+ "quote",
  "syn 2.0.79",
 ]
 
 [[package]]
 name = "kani_metadata"
-version = "0.55.0"
+version = "0.56.0"
 dependencies = [
  "clap",
  "cprover_bindings",
@@ -1063,18 +838,6 @@ version = "0.2.159"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "561d97a539a36e26a9a5fad1ea11a3039a67714694aaa379433e580854bc3dc5"
 
-[[package]]
-name = "libtest-mimic"
-version = "0.7.3"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "cc0bda45ed5b3a2904262c1bb91e526127aa70e7ef3758aba2ef93cf896b9b58"
-dependencies = [
- "clap",
- "escape8259",
- "termcolor",
- "threadpool",
-]
-
 [[package]]
 name = "linear-map"
 version = "1.2.0"
@@ -1111,9 +874,8 @@ checksum = "a7a70ba024b9dc04c27ea2f0c0548feb474ec5c54bba33a7f72f873a39d07b24"
 name = "macros"
 version = "0.1.0"
 dependencies = [
- "assert_tokens_eq",
- "proc-macro2 1.0.86",
- "quote 1.0.37",
+ "proc-macro2",
+ "quote",
  "syn 2.0.79",
 ]
 
@@ -1144,15 +906,6 @@ version = "0.2.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a"
 
-[[package]]
-name = "miniz_oxide"
-version = "0.8.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e2d80299ef12ff69b16a84bb182e3b9df68b5a91574d3d4fa6e41b65deec4df1"
-dependencies = [
- "adler2",
-]
-
 [[package]]
 name = "nom"
 version = "7.1.3"
@@ -1176,12 +929,6 @@ dependencies = [
  "nom",
 ]
 
-[[package]]
-name = "normalize-line-endings"
-version = "0.3.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "61807f77802ff30975e01f4f071c8ba10c022052f98b3294119f3e615d13e5be"
-
 [[package]]
 name = "nu-ansi-term"
 version = "0.46.0"
@@ -1280,25 +1027,6 @@ dependencies = [
  "autocfg",
 ]
 
-[[package]]
-name = "num_cpus"
-version = "1.16.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4161fcb6d602d4d2081af7c3a45852d875a03dd337a6bfdd6e06407b61342a43"
-dependencies = [
- "hermit-abi",
- "libc",
-]
-
-[[package]]
-name = "object"
-version = "0.36.5"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "aedf0a2d09c573ed1d8d85b30c119153926a2b36dce0ab28322c09a117a4683e"
-dependencies = [
- "memchr",
-]
-
 [[package]]
 name = "once_cell"
 version = "1.20.2"
@@ -1315,15 +1043,6 @@ dependencies = [
  "windows-sys 0.52.0",
 ]
 
-[[package]]
-name = "output_vt100"
-version = "0.1.3"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "628223faebab4e3e40667ee0b2336d34a5b960ff60ea743ddfdbcf7770bcfb66"
-dependencies = [
- "winapi",
-]
-
 [[package]]
 name = "overload"
 version = "0.1.1"
@@ -1353,12 +1072,6 @@ dependencies = [
  "windows-targets 0.52.6",
 ]
 
-[[package]]
-name = "paste"
-version = "1.0.15"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "57c0d7b74b563b49d38dae00a0c37d4d6de9b432382b2892f0574ddcae73fd0a"
-
 [[package]]
 name = "pathdiff"
 version = "0.2.1"
@@ -1440,8 +1153,8 @@ version = "2.0.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "96de42df36bb9bba5542fe9f1a054b8cc87e172759a1868aa05c1f3acc89dfc5"
 dependencies = [
- "proc-macro2 1.0.86",
- "quote 1.0.37",
+ "proc-macro2",
+ "quote",
 ]
 
 [[package]]
@@ -1451,20 +1164,11 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "11ec05c52be0a07b08061f7dd003e7d7092e0472bc731b4af7bb1ef876109802"
 dependencies = [
  "proc-macro-error-attr2",
- "proc-macro2 1.0.86",
- "quote 1.0.37",
+ "proc-macro2",
+ "quote",
  "syn 2.0.79",
 ]
 
-[[package]]
-name = "proc-macro2"
-version = "0.4.30"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "cf3d2011ab5c909338f7887f4fc896d35932e29146c12c8d01da6b22a80ba759"
-dependencies = [
- "unicode-xid",
-]
-
 [[package]]
 name = "proc-macro2"
 version = "1.0.86"
@@ -1483,22 +1187,13 @@ dependencies = [
  "cc",
 ]
 
-[[package]]
-name = "quote"
-version = "0.6.13"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6ce23b6b870e8f94f81fb0a363d65d86675884b34a09043c81e5562f11c1f8e1"
-dependencies = [
- "proc-macro2 0.4.30",
-]
-
 [[package]]
 name = "quote"
 version = "1.0.37"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af"
 dependencies = [
- "proc-macro2 1.0.86",
+ "proc-macro2",
 ]
 
 [[package]]
@@ -1674,30 +1369,6 @@ dependencies = [
  "strum_macros",
 ]
 
-[[package]]
-name = "schemars"
-version = "0.8.21"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "09c024468a378b7e36765cd36702b7a90cc3cba11654f6685c8f233408e89e92"
-dependencies = [
- "dyn-clone",
- "schemars_derive",
- "serde",
- "serde_json",
-]
-
-[[package]]
-name = "schemars_derive"
-version = "0.8.21"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b1eee588578aff73f856ab961cd2f79e36bc45d7ded33a7562adba4667aecc0e"
-dependencies = [
- "proc-macro2 1.0.86",
- "quote 1.0.37",
- "serde_derive_internals",
- "syn 2.0.79",
-]
-
 [[package]]
 name = "scopeguard"
 version = "1.2.0"
@@ -1737,19 +1408,8 @@ version = "1.0.210"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "243902eda00fad750862fc144cea25caca5e20d615af0a81bee94ca738f1df1f"
 dependencies = [
- "proc-macro2 1.0.86",
- "quote 1.0.37",
- "syn 2.0.79",
-]
-
-[[package]]
-name = "serde_derive_internals"
-version = "0.29.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "18d26a20a969b9e3fdf2fc2d9f21eda6c40e2de84c9408bb5d3b05d499aae711"
-dependencies = [
- "proc-macro2 1.0.86",
- "quote 1.0.37",
+ "proc-macro2",
+ "quote",
  "syn 2.0.79",
 ]
 
@@ -1827,12 +1487,6 @@ version = "1.3.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64"
 
-[[package]]
-name = "similar"
-version = "2.6.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1de1d4f81173b03af4c0cbed3c898f6bff5b870e4a7f5d6f4057d62a7a4b686e"
-
 [[package]]
 name = "sized-chunks"
 version = "0.6.5"
@@ -1849,50 +1503,6 @@ version = "1.13.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67"
 
-[[package]]
-name = "snafu"
-version = "0.4.4"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b028158eb06caa8345bee10cccfb25fa632beccf0ef5308832b4fd4b78a7db48"
-dependencies = [
- "backtrace",
- "doc-comment",
- "snafu-derive",
-]
-
-[[package]]
-name = "snafu-derive"
-version = "0.4.4"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "bf50aaef500c248a590e2696e8bf8c7620ca2235b9bb90a70363d82dd1abec6a"
-dependencies = [
- "proc-macro2 0.4.30",
- "quote 0.6.13",
- "syn 0.15.44",
-]
-
-[[package]]
-name = "snapbox"
-version = "0.6.18"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7ba434818a8a9b1b106404288d6bd75a94348aae8fc9a518b211b609a36a54bc"
-dependencies = [
- "anstream",
- "anstyle",
- "normalize-line-endings",
- "similar",
- "snapbox-macros",
-]
-
-[[package]]
-name = "snapbox-macros"
-version = "0.3.10"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "16569f53ca23a41bb6f62e0a5084aa1661f4814a67fa33696a79073e03a664af"
-dependencies = [
- "anstream",
-]
-
 [[package]]
 name = "stacker"
 version = "0.1.17"
@@ -1908,7 +1518,7 @@ dependencies = [
 
 [[package]]
 name = "std"
-version = "0.55.0"
+version = "0.56.0"
 dependencies = [
  "kani",
 ]
@@ -1943,31 +1553,20 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "4c6bee85a5a24955dc440386795aa378cd9cf82acd5f764469152d2270e581be"
 dependencies = [
  "heck",
- "proc-macro2 1.0.86",
- "quote 1.0.37",
+ "proc-macro2",
+ "quote",
  "rustversion",
  "syn 2.0.79",
 ]
 
-[[package]]
-name = "syn"
-version = "0.15.44"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9ca4b3b69a77cbe1ffc9e198781b7acb0c7365a883670e8f1c1bc66fba79a5c5"
-dependencies = [
- "proc-macro2 0.4.30",
- "quote 0.6.13",
- "unicode-xid",
-]
-
 [[package]]
 name = "syn"
 version = "1.0.109"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237"
 dependencies = [
- "proc-macro2 1.0.86",
- "quote 1.0.37",
+ "proc-macro2",
+ "quote",
  "unicode-ident",
 ]
 
@@ -1977,8 +1576,8 @@ version = "2.0.79"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "89132cd0bf050864e1d38dc3bbc07a0eb8e7530af26344d3d2bbbef83499f590"
 dependencies = [
- "proc-macro2 1.0.86",
- "quote 1.0.37",
+ "proc-macro2",
+ "quote",
  "unicode-ident",
 ]
 
@@ -2001,15 +1600,6 @@ dependencies = [
  "windows-sys 0.59.0",
 ]
 
-[[package]]
-name = "termcolor"
-version = "1.4.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "06794f8f6c5c898b3275aebefa6b8a1cb24cd2c6c79397ab15774837a0bc5755"
-dependencies = [
- "winapi-util",
-]
-
 [[package]]
 name = "termtree"
 version = "0.4.1"
@@ -2031,8 +1621,8 @@ version = "1.0.64"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "08904e7672f5eb876eaaf87e0ce17857500934f4981c4a0ab2b4aa98baac7fc3"
 dependencies = [
- "proc-macro2 1.0.86",
- "quote 1.0.37",
+ "proc-macro2",
+ "quote",
  "syn 2.0.79",
 ]
 
@@ -2046,15 +1636,6 @@ dependencies = [
  "once_cell",
 ]
 
-[[package]]
-name = "threadpool"
-version = "1.8.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d050e60b33d41c19108b32cea32164033a9013fe3b46cbd4457559bfbf77afaa"
-dependencies = [
- "num_cpus",
-]
-
 [[package]]
 name = "time"
 version = "0.3.36"
@@ -2137,8 +1718,8 @@ version = "0.1.27"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7"
 dependencies = [
- "proc-macro2 1.0.86",
- "quote 1.0.37",
+ "proc-macro2",
+ "quote",
  "syn 2.0.79",
 ]
 
@@ -2249,12 +1830,6 @@ version = "0.1.14"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "7dd6e30e90baa6f72411720665d41d89b9a3d039dc45b8faea1ddd07f617f6af"
 
-[[package]]
-name = "unicode-xid"
-version = "0.1.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "fc72304796d0818e357ead4e000d19c9c174ab23dc11093ac919054d20a6a7fc"
-
 [[package]]
 name = "unsafe-libyaml"
 version = "0.2.11"
@@ -2279,12 +1854,6 @@ version = "0.9.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
 
-[[package]]
-name = "virtue"
-version = "0.0.13"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9dcc60c0624df774c82a0ef104151231d37da4962957d691c011c852b2473314"
-
 [[package]]
 name = "wait-timeout"
 version = "0.2.0"
@@ -2532,7 +2101,7 @@ version = "0.7.35"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e"
 dependencies = [
- "proc-macro2 1.0.86",
- "quote 1.0.37",
+ "proc-macro2",
+ "quote",
  "syn 2.0.79",
 ]
diff --git a/Cargo.toml b/Cargo.toml
index ee9848b578dc..42c6f2c722b6 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-verifier"
-version = "0.55.0"
+version = "0.56.0"
 edition = "2021"
 description = "A bit-precise model checker for Rust."
 readme = "README.md"
@@ -56,6 +56,7 @@ default-members = [
 
 exclude = [
   "build",
+  "charon",
   "target",
   # dependency tests have their own workspace
   "tests/kani-dependency-test/dependency3",
diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml
index 008c81aef2ad..e26f23d5c081 100644
--- a/cprover_bindings/Cargo.toml
+++ b/cprover_bindings/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "cprover_bindings"
-version = "0.55.0"
+version = "0.56.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml
index 0360763f9068..7b17e6073bb3 100644
--- a/kani-compiler/Cargo.toml
+++ b/kani-compiler/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-compiler"
-version = "0.55.0"
+version = "0.56.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml
index 7485d2279ad6..555534959474 100644
--- a/kani-driver/Cargo.toml
+++ b/kani-driver/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-driver"
-version = "0.55.0"
+version = "0.56.0"
 edition = "2021"
 description = "Build a project with Kani and run all proof harnesses"
 license = "MIT OR Apache-2.0"
diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml
index 18eadc4095ed..2a0a03401c40 100644
--- a/kani_metadata/Cargo.toml
+++ b/kani_metadata/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani_metadata"
-version = "0.55.0"
+version = "0.56.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml
index fa50783516f4..3ad1b286ebe6 100644
--- a/library/kani/Cargo.toml
+++ b/library/kani/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani"
-version = "0.55.0"
+version = "0.56.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/library/kani_core/Cargo.toml b/library/kani_core/Cargo.toml
index 447cd0b3f298..df55e6278282 100644
--- a/library/kani_core/Cargo.toml
+++ b/library/kani_core/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani_core"
-version = "0.55.0"
+version = "0.56.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml
index 6930366b84fc..a7876176adb2 100644
--- a/library/kani_macros/Cargo.toml
+++ b/library/kani_macros/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani_macros"
-version = "0.55.0"
+version = "0.56.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml
index 12c923e9b655..e1e353704723 100644
--- a/library/std/Cargo.toml
+++ b/library/std/Cargo.toml
@@ -5,7 +5,7 @@
 # Note: this package is intentionally named std to make sure the names of
 # standard library symbols are preserved
 name = "std"
-version = "0.55.0"
+version = "0.56.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/tools/build-kani/Cargo.toml b/tools/build-kani/Cargo.toml
index 41095f1d7c3c..25e022e70d3f 100644
--- a/tools/build-kani/Cargo.toml
+++ b/tools/build-kani/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "build-kani"
-version = "0.55.0"
+version = "0.56.0"
 edition = "2021"
 description = "Builds Kani, Sysroot and release bundle."
 license = "MIT OR Apache-2.0"