diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9b4acbb284aa..47ae290853a3 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -4,6 +4,44 @@ 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.53.0]
+
+### Major Changes
+* 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.
+
+### Breaking Changes
+* Remove support for the unstable argument `--function` by @celinval in https://github.com/model-checking/kani/pull/3278
+* Remove deprecated `--enable-stubbing` by @celinval in https://github.com/model-checking/kani/pull/3309
+
+### What's Changed
+
+* Change ensures into closures by @pi314mm in https://github.com/model-checking/kani/pull/3207
+* (Re)introduce `Invariant` trait by @adpaco-aws in https://github.com/model-checking/kani/pull/3190
+* Remove empty box creation from contracts impl by @celinval in https://github.com/model-checking/kani/pull/3233
+* Add a new verify-std subcommand to Kani by @celinval in https://github.com/model-checking/kani/pull/3231
+* Inject pointer validity check when casting raw pointers to references by @artemagvanian in https://github.com/model-checking/kani/pull/3221
+* Do not turn trivially diverging loops into assume(false) by @tautschnig in https://github.com/model-checking/kani/pull/3223
+* Fix "unused mut" warnings created by generated code. by @jsalzbergedu in https://github.com/model-checking/kani/pull/3247
+* Refactor stubbing so Kani compiler only invoke rustc once per crate by @celinval in https://github.com/model-checking/kani/pull/3245
+* Use cfg=kani_host for host crates by @tautschnig in https://github.com/model-checking/kani/pull/3244
+* Add intrinsics and Arbitrary support for no_core by @jaisnan in https://github.com/model-checking/kani/pull/3230
+* Contracts: Avoid attribute duplication and `const` function generation for constant function by @celinval in https://github.com/model-checking/kani/pull/3255
+* Fix contract of constant fn with effect feature by @celinval in https://github.com/model-checking/kani/pull/3259
+* Fix typed_swap for ZSTs by @tautschnig in https://github.com/model-checking/kani/pull/3256
+* Add a `#[derive(Invariant)]` macro by @adpaco-aws in https://github.com/model-checking/kani/pull/3250
+* Contracts: History Expressions via "old" monad by @pi314mm in https://github.com/model-checking/kani/pull/3232
+* Function Contracts: remove instances of _renamed by @pi314mm in https://github.com/model-checking/kani/pull/3274
+* Deprecate `--visualize` in favor of concrete playback by @celinval in https://github.com/model-checking/kani/pull/3281
+* Fix operand in fat pointer comparison by @pi314mm in https://github.com/model-checking/kani/pull/3297
+* Function Contracts: Closure Type Inference by @pi314mm in https://github.com/model-checking/kani/pull/3307
+* Add support for f16 and f128 for toolchain upgrade to 6/28 by @jaisnan in https://github.com/model-checking/kani/pull/3306
+* Towards Proving Memory Initialization by @artemagvanian in https://github.com/model-checking/kani/pull/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
+
 ## [0.52.0]
 
 ## What's Changed
diff --git a/Cargo.lock b/Cargo.lock
index 89e393db8b46..cf47e75b0562 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -92,7 +92,7 @@ checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de"
 
 [[package]]
 name = "build-kani"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
@@ -228,7 +228,7 @@ dependencies = [
 
 [[package]]
 name = "cprover_bindings"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "lazy_static",
  "linear-map",
@@ -405,14 +405,14 @@ checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b"
 
 [[package]]
 name = "kani"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "kani_macros",
 ]
 
 [[package]]
 name = "kani-compiler"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "clap",
  "cprover_bindings",
@@ -433,7 +433,7 @@ dependencies = [
 
 [[package]]
 name = "kani-driver"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
@@ -461,7 +461,7 @@ dependencies = [
 
 [[package]]
 name = "kani-verifier"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "anyhow",
  "home",
@@ -470,14 +470,14 @@ dependencies = [
 
 [[package]]
 name = "kani_core"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "kani_macros",
 ]
 
 [[package]]
 name = "kani_macros"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "proc-macro-error",
  "proc-macro2",
@@ -487,7 +487,7 @@ dependencies = [
 
 [[package]]
 name = "kani_metadata"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "clap",
  "cprover_bindings",
@@ -992,7 +992,7 @@ checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67"
 
 [[package]]
 name = "std"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "kani",
 ]
diff --git a/Cargo.toml b/Cargo.toml
index 641cbaf961be..1b4933c5bdcf 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-verifier"
-version = "0.52.0"
+version = "0.53.0"
 edition = "2021"
 description = "A bit-precise model checker for Rust."
 readme = "README.md"
diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml
index 63dfbf6781cd..aced9e5b9b65 100644
--- a/cprover_bindings/Cargo.toml
+++ b/cprover_bindings/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "cprover_bindings"
-version = "0.52.0"
+version = "0.53.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml
index 05002ed1eb27..23389c156302 100644
--- a/kani-compiler/Cargo.toml
+++ b/kani-compiler/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-compiler"
-version = "0.52.0"
+version = "0.53.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml
index 2263e39792e2..d58d686d7d43 100644
--- a/kani-driver/Cargo.toml
+++ b/kani-driver/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-driver"
-version = "0.52.0"
+version = "0.53.0"
 edition = "2021"
 description = "Build a project with Kani and run all proof harnesses"
 license = "MIT OR Apache-2.0"
diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs
index 4c0fe98cc65d..d043035bcab2 100644
--- a/kani-driver/src/args/mod.rs
+++ b/kani-driver/src/args/mod.rs
@@ -282,17 +282,6 @@ pub struct VerificationArgs {
     #[arg(long)]
     pub randomize_layout: Option<Option<u64>>,
 
-    /// Enable the stubbing of functions and methods.
-    // TODO: Stubbing should in principle work with concrete playback.
-    // <https://github.com/model-checking/kani/issues/1842>
-    #[arg(
-        long,
-        hide_short_help = true,
-        requires("enable_unstable"),
-        conflicts_with("concrete_playback")
-    )]
-    enable_stubbing: bool,
-
     /// Enable Kani coverage output alongside verification result
     #[arg(long, hide_short_help = true)]
     pub coverage: bool,
@@ -345,8 +334,7 @@ impl VerificationArgs {
 
     /// Is experimental stubbing enabled?
     pub fn is_stubbing_enabled(&self) -> bool {
-        self.enable_stubbing
-            || self.common_args.unstable_features.contains(UnstableFeature::Stubbing)
+        self.common_args.unstable_features.contains(UnstableFeature::Stubbing)
             || self.is_function_contracts_enabled()
     }
 }
@@ -579,6 +567,13 @@ impl ValidateArgs for VerificationArgs {
                 --output-format=old.",
             ));
         }
+        if self.concrete_playback.is_some() && self.is_stubbing_enabled() {
+            // Concrete playback currently does not work with contracts or stubbing.
+            return Err(Error::raw(
+                ErrorKind::ArgumentConflict,
+                "Conflicting options: --concrete-playback isn't compatible with stubbing.",
+            ));
+        }
         if self.concrete_playback.is_some() && self.jobs() != Some(1) {
             // Concrete playback currently embeds a lot of assumptions about the order in which harnesses get called.
             return Err(Error::raw(
@@ -606,10 +601,6 @@ impl ValidateArgs for VerificationArgs {
             }
         }
 
-        if self.enable_stubbing {
-            print_deprecated(&self.common_args, "--enable-stubbing", "-Z stubbing");
-        }
-
         if self.concrete_playback.is_some()
             && !self.common_args.unstable_features.contains(UnstableFeature::ConcretePlayback)
         {
@@ -880,14 +871,18 @@ mod tests {
 
     #[test]
     fn check_enable_stubbing() {
-        check_unstable_flag!("--enable-stubbing --harness foo", enable_stubbing);
+        let res = parse_unstable_disabled("--harness foo").unwrap();
+        assert!(!res.verify_opts.is_stubbing_enabled());
 
-        check_unstable_flag!("--enable-stubbing", enable_stubbing);
+        let res = parse_unstable_disabled("--harness foo -Z stubbing").unwrap();
+        assert!(res.verify_opts.is_stubbing_enabled());
 
-        // `--enable-stubbing` cannot be called with `--concrete-playback`
-        let err =
-            parse_unstable_enabled("--enable-stubbing --harness foo --concrete-playback=print")
-                .unwrap_err();
+        // `-Z stubbing` cannot be called with `--concrete-playback`
+        let res = parse_unstable_disabled(
+            "--harness foo --concrete-playback=print -Z concrete-playback -Z stubbing",
+        )
+        .unwrap();
+        let err = res.validate().unwrap_err();
         assert_eq!(err.kind(), ErrorKind::ArgumentConflict);
     }
 
diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml
index f9d701018367..816752a58e03 100644
--- a/kani_metadata/Cargo.toml
+++ b/kani_metadata/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani_metadata"
-version = "0.52.0"
+version = "0.53.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml
index c0f783e65315..91fee3dabf30 100644
--- a/library/kani/Cargo.toml
+++ b/library/kani/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani"
-version = "0.52.0"
+version = "0.53.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 6f5230c6d19b..ec12209f0e08 100644
--- a/library/kani_core/Cargo.toml
+++ b/library/kani_core/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani_core"
-version = "0.52.0"
+version = "0.53.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 e0c79a39c105..5917c322729e 100644
--- a/library/kani_macros/Cargo.toml
+++ b/library/kani_macros/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani_macros"
-version = "0.52.0"
+version = "0.53.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml
index fcc2739dc606..ae70767f6781 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.52.0"
+version = "0.53.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/tests/cargo-ui/stubbing-flag/src/main.rs b/tests/cargo-ui/stubbing-flag/src/main.rs
index db26e366005e..1ef312b852ff 100644
--- a/tests/cargo-ui/stubbing-flag/src/main.rs
+++ b/tests/cargo-ui/stubbing-flag/src/main.rs
@@ -1,7 +1,8 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-//! This tests that the `--enable-stubbing` and `--harness` arguments flow from `kani-driver` to `kani-compiler`.
+//! This tests that enabling stubbing and using `--harness` arguments flow from
+//! `kani-driver` to `kani-compiler`.
 
 #[kani::proof]
 fn main() {}
diff --git a/tests/expected/function-stubbing-no-harness/main.rs b/tests/expected/function-stubbing-no-harness/main.rs
index 1819c8dce862..d69192ae2180 100644
--- a/tests/expected/function-stubbing-no-harness/main.rs
+++ b/tests/expected/function-stubbing-no-harness/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness foo --enable-unstable --enable-stubbing
+// kani-flags: --harness foo -Z stubbing
 //
 //! This tests whether we detect missing harnesses during stubbing.
 
diff --git a/tests/expected/stubbing-ambiguous-path/main.rs b/tests/expected/stubbing-ambiguous-path/main.rs
index 7a406d51d227..9ab25b501a44 100644
--- a/tests/expected/stubbing-ambiguous-path/main.rs
+++ b/tests/expected/stubbing-ambiguous-path/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness main --enable-unstable --enable-stubbing
+// kani-flags: --harness main -Z stubbing
 //
 //! This tests that we raise an error if a path in a `kani::stub` attribute can
 //! resolve to multiple functions.
diff --git a/tests/ui/function-stubbing-error/main.rs b/tests/ui/function-stubbing-error/main.rs
index 2f5a10ff18cb..c433e352e740 100644
--- a/tests/ui/function-stubbing-error/main.rs
+++ b/tests/ui/function-stubbing-error/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness main --enable-unstable --enable-stubbing
+// kani-flags: --harness main -Z stubbing
 //
 //! This tests whether we detect syntactically misformed `kani::stub` annotations.
 
diff --git a/tests/ui/stubbing/deprecated-enable-stable/deprecated.rs b/tests/ui/stubbing/deprecated-enable-stable/deprecated.rs
deleted file mode 100644
index a5686af20a35..000000000000
--- a/tests/ui/stubbing/deprecated-enable-stable/deprecated.rs
+++ /dev/null
@@ -1,16 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --enable-unstable --enable-stubbing
-//! Checks that the `kani::stub` attribute is accepted
-
-fn foo() {
-    unreachable!();
-}
-
-fn bar() {}
-
-#[kani::proof]
-#[kani::stub(foo, bar)]
-fn main() {
-    foo();
-}
diff --git a/tests/ui/stubbing/deprecated-enable-stable/expected b/tests/ui/stubbing/deprecated-enable-stable/expected
deleted file mode 100644
index eb05b8cf9812..000000000000
--- a/tests/ui/stubbing/deprecated-enable-stable/expected
+++ /dev/null
@@ -1,2 +0,0 @@
-warning: The `--enable-stubbing` option is deprecated. This option will be removed soon. Consider using `-Z stubbing` instead
-VERIFICATION:- SUCCESSFUL
diff --git a/tests/ui/stubbing/invalid-path/invalid.rs b/tests/ui/stubbing/invalid-path/invalid.rs
index d24c757fd0cd..04d3c786b0d7 100644
--- a/tests/ui/stubbing/invalid-path/invalid.rs
+++ b/tests/ui/stubbing/invalid-path/invalid.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness invalid_stub --enable-unstable --enable-stubbing
+// kani-flags: --harness invalid_stub -Z stubbing
 
 pub mod mod_a {
     use crate::mod_b::noop;
diff --git a/tests/ui/stubbing/stubbing-flag/main.rs b/tests/ui/stubbing/stubbing-flag/main.rs
index f9b788e94d82..a5172ad9d0cd 100644
--- a/tests/ui/stubbing/stubbing-flag/main.rs
+++ b/tests/ui/stubbing/stubbing-flag/main.rs
@@ -1,9 +1,9 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness main --enable-unstable --enable-stubbing
+// kani-flags: --harness main -Z stubbing
 //
-//! This tests that the `--enable-stubbing` and `--harness` arguments flow from `kani-driver` to `kani-compiler`.
+//! This tests that enabling stubbing and `--harness` argument flow from `kani-driver` to `kani-compiler`.
 
 #[kani::proof]
 fn main() {}
diff --git a/tests/ui/stubbing/stubbing-trait-validation/trait_mismatch.rs b/tests/ui/stubbing/stubbing-trait-validation/trait_mismatch.rs
index e934141664bf..c49552d942e2 100644
--- a/tests/ui/stubbing/stubbing-trait-validation/trait_mismatch.rs
+++ b/tests/ui/stubbing/stubbing-trait-validation/trait_mismatch.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness harness --enable-unstable --enable-stubbing
+// kani-flags: --harness harness -Z stubbing
 //
 //! This tests that we catch trait mismatches between the stub and the original
 //! function/method. In particular, this tests the case when the program is
diff --git a/tests/ui/stubbing/stubbing-type-validation/type_mismatch.rs b/tests/ui/stubbing/stubbing-type-validation/type_mismatch.rs
index 9f98ae302a22..bc8343658f9e 100644
--- a/tests/ui/stubbing/stubbing-type-validation/type_mismatch.rs
+++ b/tests/ui/stubbing/stubbing-type-validation/type_mismatch.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness harness --enable-unstable --enable-stubbing
+// kani-flags: --harness harness -Z stubbing
 //
 //! This tests that we catch type mismatches between the stub and the original
 //! function/method.
diff --git a/tools/build-kani/Cargo.toml b/tools/build-kani/Cargo.toml
index 30c2807aa323..7c8e6eef122a 100644
--- a/tools/build-kani/Cargo.toml
+++ b/tools/build-kani/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "build-kani"
-version = "0.52.0"
+version = "0.53.0"
 edition = "2021"
 description = "Builds Kani, Sysroot and release bundle."
 license = "MIT OR Apache-2.0"