diff --git a/src/Lean/Util.lean b/src/Lean/Util.lean
index f80586041328..3a93462cc123 100644
--- a/src/Lean/Util.lean
+++ b/src/Lean/Util.lean
@@ -23,6 +23,7 @@ import Lean.Util.ForEachExprWhere
 import Lean.Util.ReplaceLevel
 import Lean.Util.FoldConsts
 import Lean.Util.SCC
+import Lean.Util.TestExtern
 import Lean.Util.OccursCheck
 import Lean.Util.HasConstCache
 import Lean.Util.FileSetupInfo
diff --git a/src/Lean/Util/TestExtern.lean b/src/Lean/Util/TestExtern.lean
new file mode 100644
index 000000000000..56437c3636f4
--- /dev/null
+++ b/src/Lean/Util/TestExtern.lean
@@ -0,0 +1,25 @@
+import Lean.Elab.SyntheticMVars
+import Lean.Elab.Command
+import Lean.Meta.Tactic.Unfold
+import Lean.Meta.Eval
+
+open Lean Elab Meta Command Term
+
+syntax (name := testExternCmd) "test_extern " term : command
+
+@[command_elab testExternCmd] unsafe def elabTestExtern : CommandElab
+  | `(test_extern $t:term) => liftTermElabM do
+    let t ← elabTermAndSynthesize t none
+    match t.getAppFn with
+    | .const f _ =>
+      if isExtern (← getEnv) f then
+        let t' := (← unfold t f).expr
+        let r := mkApp (.const ``reduceBool []) (← mkAppM ``BEq.beq #[t, t'])
+        if ! (← evalExpr Bool (.const ``Bool []) r) then
+          throwError
+            ("native implementation did not agree with reference implementation!\n" ++
+            m!"Compare the outputs of:\n#eval {t}\n and\n#eval {t'}")
+      else
+        throwError "test_extern: {f} does not have an @[extern] attribute"
+    | _ => throwError "test_extern: expects a function application"
+  | _ => throwUnsupportedSyntax
diff --git a/tests/lean/test_extern.lean b/tests/lean/test_extern.lean
new file mode 100644
index 000000000000..ff0522fcdd2f
--- /dev/null
+++ b/tests/lean/test_extern.lean
@@ -0,0 +1,9 @@
+import Lean.Util.TestExtern
+
+instance : BEq ByteArray where
+  beq x y := x.data == y.data
+
+test_extern Nat.add 12 37
+test_extern 4 + 5
+
+test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 0 6
diff --git a/tests/lean/test_extern.lean.expected.out b/tests/lean/test_extern.lean.expected.out
new file mode 100644
index 000000000000..0f8649bb222f
--- /dev/null
+++ b/tests/lean/test_extern.lean.expected.out
@@ -0,0 +1,11 @@
+test_extern.lean:7:0-7:17: error: test_extern: HAdd.hAdd does not have an @[extern] attribute
+test_extern.lean:9:0-9:86: error: native implementation did not agree with reference implementation!
+Compare the outputs of:
+#eval ByteArray.copySlice { data := #[1, 2, 3] } 1 { data := #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] } 0 6
+ and
+#eval {
+  data :=
+    Array.extract { data := #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] }.data 0 0 ++
+        Array.extract { data := #[1, 2, 3] }.data 1 (1 + 6) ++
+      Array.extract { data := #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] }.data (0 + 6)
+        (Array.size { data := #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] }.data) }
diff --git a/tests/pkg/test_extern/TestExtern.lean b/tests/pkg/test_extern/TestExtern.lean
new file mode 100644
index 000000000000..4c87ee279614
--- /dev/null
+++ b/tests/pkg/test_extern/TestExtern.lean
@@ -0,0 +1,5 @@
+import Lean.Util.TestExtern
+import TestExtern.BadExtern
+
+test_extern Nat.add 4 5
+test_extern Nat.not_add 4 5
diff --git a/tests/pkg/test_extern/TestExtern/BadExtern.lean b/tests/pkg/test_extern/TestExtern/BadExtern.lean
new file mode 100644
index 000000000000..2cd919940f3a
--- /dev/null
+++ b/tests/pkg/test_extern/TestExtern/BadExtern.lean
@@ -0,0 +1,3 @@
+@[extern "lean_nat_add"]
+protected def Nat.not_add : (@& Nat) → (@& Nat) → Nat
+  | _, _ => 0
diff --git a/tests/pkg/test_extern/expected.txt b/tests/pkg/test_extern/expected.txt
new file mode 100644
index 000000000000..9a02d1407057
--- /dev/null
+++ b/tests/pkg/test_extern/expected.txt
@@ -0,0 +1,7 @@
+error: stdout:
+./././TestExtern.lean:5:0: error: native implementation did not agree with reference implementation!
+Compare the outputs of:
+#eval Nat.not_add 4 5
+ and
+#eval match 4, 5 with
+| x, x_1 => 0
diff --git a/tests/pkg/test_extern/lakefile.lean b/tests/pkg/test_extern/lakefile.lean
new file mode 100644
index 000000000000..4d83d34ed146
--- /dev/null
+++ b/tests/pkg/test_extern/lakefile.lean
@@ -0,0 +1,7 @@
+import Lake
+open System Lake DSL
+
+package test_extern where
+  precompileModules := true
+
+@[default_target] lean_lib TestExtern
diff --git a/tests/pkg/test_extern/test.sh b/tests/pkg/test_extern/test.sh
new file mode 100755
index 000000000000..1f5898cba3e7
--- /dev/null
+++ b/tests/pkg/test_extern/test.sh
@@ -0,0 +1,33 @@
+#!/usr/bin/env bash
+
+# We need a package test because we need multiple files with imports.
+# Currently the other package tests all succeed,
+# but here we need to check for a particular error message.
+# This is just an ad-hoc text mangling script to extract the error message
+# and account for some OS differences.
+# Ideally there would be a more principled testing framework
+# that took care of all this!
+
+rm -rf .lake/build
+
+# Function to process the output
+verify_output() {
+    # Normalize path separators from backslashes to forward slashes
+    sed 's#\\#/#g' |
+    awk '/error: stdout:/, /error: external command/' |
+    sed '/error: external command/d'
+}
+
+lake build 2>&1 | verify_output > produced.txt
+
+# Compare the actual output with the expected output
+if diff --strip-trailing-cr -q produced.txt expected.txt > /dev/null; then
+    echo "Output matches expected output."
+    rm produced.txt
+    exit 0
+else
+    echo "Output differs from expected output:"
+    diff --strip-trailing-cr produced.txt expected.txt
+    rm produced.txt
+    exit 1
+fi