diff --git a/lakefile.lean b/lakefile.lean
index 4a03a08..6d927e6 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -87,3 +87,12 @@ lean_lib Blake3Rust where
   roots := #[`Blake3.Rust]
   moreLinkObjs := #[blake3_rs]
 
+/-- The `blake3-rs` shared library. Produced by the same `cargo build` as
+`blake3_rs`; this target selects the `cdylib` output for downstream tooling
+that loads the raw `rs_blake3_*` symbols at runtime rather than linking them
+statically — e.g. supplying the BLAKE3 backend to Lean's native evaluator for
+`native_decide` proofs. -/
+target blake3_rs_shared pkg : System.FilePath := do
+  proc { cmd := "cargo", args := #["build", "--release"], cwd := pkg.dir / "rust" } (quiet := true)
+  inputBinFile $ pkg.dir / "rust" / "target" / "release" / nameToSharedLib "blake3_rs"
+
diff --git a/rust/Cargo.toml b/rust/Cargo.toml
index deaa12c..aaf2a36 100644
--- a/rust/Cargo.toml
+++ b/rust/Cargo.toml
@@ -8,7 +8,11 @@ version = "0.1.0"
 edition = "2024"
 
 [lib]
-crate-type = ["staticlib"]
+# `staticlib` is linked into final Lean executables. `cdylib` additionally
+# builds a position-independent shared object exporting the raw `rs_blake3_*`
+# symbols, so they can be loaded at runtime — e.g. by Lean's native evaluator
+# for `native_decide` proofs elaborated before any executable is linked.
+crate-type = ["staticlib", "cdylib"]
 
 [dependencies]
 blake3 = "1.8.4"