diff --git a/library/std/src/lib.rs b/library/std/src/lib.rs
index a7b1d81d7be28..aa429d3ffedea 100644
--- a/library/std/src/lib.rs
+++ b/library/std/src/lib.rs
@@ -140,25 +140,54 @@ macro_rules! eprintln {
 
 #[macro_export]
 macro_rules! unreachable {
+    // The argument, if present, is a literal that represents the error message, i.e.:
+    // `unreachable!("Error message")` or `unreachable!()`
     ($($msg:literal)? $(,)?) => (
         kani::panic(concat!("internal error: entered unreachable code: ", $($msg)?))
     );
-    ($fmt:expr, $($arg:tt)*) => (
-        kani::panic(concat!("internal error: entered unreachable code: ", $fmt), stringify!($($arg)*)));
+    // The argument is an expression, such as a variable.
+    // ```
+    // let msg = format!("Error: {}", code);
+    // unreachable!(msg);
+    // ```
+    // This was supported for 2018 and older rust editions.
+    // TODO: Is it possible to trigger an error if 2021 and above?
+    // https://github.com/model-checking/kani/issues/1375
+    ($($msg:expr)? $(,)?) => (
+        kani::panic(concat!("internal error: entered unreachable code: ", stringify!($($msg)?)))
+    );
+    // The first argument is the format and the rest contains tokens to be included in the msg.
+    // `unreachable!("Error: {}", code);`
+    ($fmt:literal, $($arg:tt)*) => (
+        kani::panic(concat!("internal error: entered unreachable code: ",
+        stringify!($fmt, $($arg)*))));
 }
 
 #[macro_export]
 macro_rules! panic {
+    // No argument is given.
     () => (
         kani::panic("explicit panic")
     );
+    // The argument is a literal that represents the error message, i.e.:
+    // `panic!("Error message")`
     ($msg:literal $(,)?) => ({
         kani::panic(concat!($msg));
     });
+    // The argument is an expression, such as a variable.
+    // ```
+    // let msg = format!("Error: {}", code);
+    // panic!(msg);
+    // ```
+    // This was supported for 2018 and older rust editions.
+    // TODO: Is it possible to trigger an error if 2021 and above?
+    // https://github.com/model-checking/kani/issues/1375
     ($msg:expr $(,)?) => ({
         kani::panic(stringify!($msg));
     });
-    ($msg:expr, $($arg:tt)*) => ({
-        kani::panic(stringify!($msg, $($arg)*));
+    // The first argument is the format and the rest contains tokens to be included in the msg.
+    // `panic!("Error: {}", code);`
+    ($msg:literal, $($arg:tt)+) => ({
+        kani::panic(stringify!($msg, $($arg)+));
     });
 }
diff --git a/tests/expected/unreachable/expected b/tests/expected/unreachable/expected
new file mode 100644
index 0000000000000..37eb2240fae59
--- /dev/null
+++ b/tests/expected/unreachable/expected
@@ -0,0 +1,6 @@
+Failed Checks: internal error: entered unreachable code: msg
+Failed Checks: internal error: entered unreachable code:
+Failed Checks: internal error: entered unreachable code: Error message
+Failed Checks: internal error: entered unreachable code: "Unreachable message with arg {}", "str"
+Failed Checks: internal error: entered unreachable code: "{}", msg
+
diff --git a/tests/expected/unreachable/unreach_msg.rs b/tests/expected/unreachable/unreach_msg.rs
new file mode 100644
index 0000000000000..14f5755270f66
--- /dev/null
+++ b/tests/expected/unreachable/unreach_msg.rs
@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks that our macro override supports different types of messages.
+#[kani::proof]
+fn check_unreachable() {
+    let msg = "Oops.";
+    match kani::any::<u8>() {
+        0 => unreachable!(),
+        1 => unreachable!("Error message"),
+        2 => unreachable!("Unreachable message with arg {}", "str"),
+        3 => unreachable!("{}", msg),
+        _ => unreachable!(msg),
+    }
+}