diff --git a/tests/pkg/user_plugin/UserPlugin.lean b/tests/pkg/user_plugin/UserPlugin.lean
new file mode 100644
index 000000000000..73eb08c18c0d
--- /dev/null
+++ b/tests/pkg/user_plugin/UserPlugin.lean
@@ -0,0 +1 @@
+builtin_initialize IO.println "Ran builtin initializer"
diff --git a/tests/pkg/user_plugin/clean.sh b/tests/pkg/user_plugin/clean.sh
new file mode 100755
index 000000000000..69f5a551a5c1
--- /dev/null
+++ b/tests/pkg/user_plugin/clean.sh
@@ -0,0 +1,2 @@
+rm -rf .lake/build
+rm -f lake-manifest.json
diff --git a/tests/pkg/user_plugin/lakefile.toml b/tests/pkg/user_plugin/lakefile.toml
new file mode 100644
index 000000000000..901faa2a258f
--- /dev/null
+++ b/tests/pkg/user_plugin/lakefile.toml
@@ -0,0 +1,6 @@
+name = "user_plugin"
+defaultTargets = ["UserPlugin"]
+
+[[lean_lib]]
+name = "UserPlugin"
+defaultFacets = ["shared"]
diff --git a/tests/pkg/user_plugin/test.lean b/tests/pkg/user_plugin/test.lean
new file mode 100644
index 000000000000..43d50388c4f0
--- /dev/null
+++ b/tests/pkg/user_plugin/test.lean
@@ -0,0 +1,8 @@
+import Lean.LoadDynlib
+
+def main (args : List String) : IO UInt32 := do
+  let plugin :: [] := args
+    | IO.println "Usage: lean --run test.lean <plugin>"
+      return 1
+  Lean.loadPlugin plugin
+  return 0
diff --git a/tests/pkg/user_plugin/test.sh b/tests/pkg/user_plugin/test.sh
new file mode 100755
index 000000000000..71092c212662
--- /dev/null
+++ b/tests/pkg/user_plugin/test.sh
@@ -0,0 +1,42 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+# Deermine shared library extension
+if [ "${OS:-}" = Windows_NT ]; then
+LIB_PREFIX=
+SHLIB_EXT=dll
+elif [ "`uname`" = Darwin ]; then
+LIB_PREFIX=lib
+SHLIB_EXT=dylib
+else
+LIB_PREFIX=lib
+SHLIB_EXT=so
+fi
+
+# Reset test
+./clean.sh
+lake update -q
+
+# Build plugin
+lake build
+LIB_DIR=.lake/build/lib
+SHLIB=$LIB_DIR/${LIB_PREFIX}UserPlugin.$SHLIB_EXT
+test -f $SHLIB || {
+  echo "Plugin library not found; $LIB_DIR contains:"
+  ls $LIB_DIR
+  exit 1
+}
+PLUGIN=$LIB_DIR/UserPlugin.$SHLIB_EXT
+mv $SHLIB $PLUGIN
+
+# Expected test output
+EXPECTED_OUT="Ran builtin initializer"
+
+# Test plugin via `lean`
+echo | lean --plugin=$PLUGIN --stdin | diff <(echo "$EXPECTED_OUT") -
+
+# Test plugin via `Lean.loadPlugin`
+lean --run test.lean $PLUGIN | diff <(echo "$EXPECTED_OUT") -
+
+# Print success
+echo "Tests completed successfully."