diff --git a/library/std/src/lib.rs b/library/std/src/lib.rs
index e7160266e5d99..79bbd509bd0ca 100644
--- a/library/std/src/lib.rs
+++ b/library/std/src/lib.rs
@@ -45,3 +45,34 @@ macro_rules! assert {
         kani::assert($cond, concat!(stringify!($($arg)+)));
     };
 }
+
+// Override the assert_eq and assert_ne macros to
+// 1. Bypass the formatting-related code in the standard library implementation,
+//    which is not relevant for verification (see
+//    /~https://github.com/model-checking/kani/issues/14)
+// 2. Generate a suitable message for the assert of the form:
+//        assertion failed: $left == $right
+//    instead of the uninformative:
+//        a panicking function core::panicking::assert_failed is invoked
+//    (see /~https://github.com/model-checking/kani/issues/13)
+// 3. Call kani::assert so that any instrumentation that it does (e.g. injecting
+//    reachability checks) is done for assert_eq and assert_ne
+#[macro_export]
+macro_rules! assert_eq {
+    ($left:expr, $right:expr $(,)?) => ({
+        assert!($left == $right);
+    });
+    ($left:expr, $right:expr, $($arg:tt)+) => ({
+        assert!($left == $right, $($arg)+);
+    });
+}
+
+#[macro_export]
+macro_rules! assert_ne {
+    ($left:expr, $right:expr $(,)?) => ({
+        assert!($left != $right);
+    });
+    ($left:expr, $right:expr, $($arg:tt)+) => ({
+        assert!($left != $right, $($arg)+);
+    });
+}
diff --git a/tests/expected/assert-eq/expected b/tests/expected/assert-eq/expected
index e753deb8ab096..729835dd2ec3f 100644
--- a/tests/expected/assert-eq/expected
+++ b/tests/expected/assert-eq/expected
@@ -1,3 +1,3 @@
-a panicking function core::panicking::assert_failed is invoked: SUCCESS
-a panicking function core::panicking::assert_failed is invoked: FAILURE
-a panicking function core::panicking::assert_failed is invoked: SUCCESS
+line 15 assertion failed: x + 1 == y: SUCCESS
+line 16 assertion failed: x == y: FAILURE
+line 17 assertion failed: x != y: SUCCESS