diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs
index af9d025e22b0..f20dd8318fe6 100644
--- a/kani-compiler/src/args.rs
+++ b/kani-compiler/src/args.rs
@@ -65,6 +65,10 @@ pub struct Arguments {
     /// Option used for suppressing global ASM error.
     #[clap(long)]
     pub ignore_global_asm: bool,
+    /// Compute verification results under the assumption that no panic occurs.
+    /// This feature is unstable, and it requires `-Z unstable-options` to be used
+    #[clap(long)]
+    pub prove_safety_only: bool,
     /// Option name used to select which reachability analysis to perform.
     #[clap(long = "reachability", default_value = "none")]
     pub reachability_analysis: ReachabilityType,
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
index a9649cab6e6b..907edf954065 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
@@ -133,11 +133,18 @@ impl GotocCtx<'_> {
         message: &str,
         loc: Location,
     ) -> Stmt {
-        let property_name = property_class.as_str();
-        Stmt::block(
-            vec![Stmt::assert(cond.clone(), property_name, message, loc), Stmt::assume(cond, loc)],
-            loc,
-        )
+        if property_class == PropertyClass::Assertion && self.queries.args().prove_safety_only {
+            Stmt::assume(cond, loc)
+        } else {
+            let property_name = property_class.as_str();
+            Stmt::block(
+                vec![
+                    Stmt::assert(cond.clone(), property_name, message, loc),
+                    Stmt::assume(cond, loc),
+                ],
+                loc,
+            )
+        }
     }
 
     /// Generate code to cover the given condition at the current location
diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs
index ef413e228939..52f621c2f027 100644
--- a/kani-driver/src/args/mod.rs
+++ b/kani-driver/src/args/mod.rs
@@ -330,6 +330,11 @@ pub struct VerificationArgs {
     #[arg(long, hide = true)]
     pub print_llbc: bool,
 
+    /// Compute verification results under the assumption that no panic occurs.
+    /// This feature is unstable, and it requires `-Z unstable-options` to be used
+    #[arg(long, hide_short_help = true)]
+    pub prove_safety_only: bool,
+
     /// Randomize the layout of structures. This option can help catching code that relies on
     /// a specific layout chosen by the compiler that is not guaranteed to be stable in the future.
     /// If a value is given, it will be used as the seed for randomization
@@ -726,6 +731,12 @@ impl ValidateArgs for VerificationArgs {
                 UnstableFeature::FunctionContracts,
             )?;
 
+            self.common_args.check_unstable(
+                self.prove_safety_only,
+                "prove-safety-only",
+                UnstableFeature::UnstableOptions,
+            )?;
+
             Ok(())
         };
 
diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs
index bdd9fdf52314..dc962b0b1063 100644
--- a/kani-driver/src/call_single_file.rs
+++ b/kani-driver/src/call_single_file.rs
@@ -175,6 +175,10 @@ impl KaniSession {
             flags.extend(args.into_iter().map(KaniArg::from));
         }
 
+        if self.args.prove_safety_only {
+            flags.push("--prove-safety-only".into());
+        }
+
         flags.extend(self.args.common_args.unstable_features.as_arguments().map(KaniArg::from));
 
         flags
diff --git a/tests/kani/Panic/prove_safety_only.rs b/tests/kani/Panic/prove_safety_only.rs
new file mode 100644
index 000000000000..76d9d6b31cca
--- /dev/null
+++ b/tests/kani/Panic/prove_safety_only.rs
@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z unstable-options --prove-safety-only
+//! Test that --prove-safety-only works
+
+#[kani::proof]
+fn div0() -> i32 {
+    let x: i32 = kani::any();
+    let y: i32 = kani::any();
+    x / y
+}
+
+#[kani::proof]
+fn assert_hides_ub() {
+    let arr: [u8; 5] = kani::any();
+    let mut bytes = kani::slice::any_slice_of_array(&arr);
+    let slice_offset = unsafe { bytes.as_ptr().offset_from(&arr as *const u8) };
+    let offset: usize = kani::any();
+    assert!(offset <= 4 && (slice_offset as usize) + offset <= 4);
+    let _ = unsafe { *bytes.as_ptr().add(offset) };
+}