diff --git a/crates/proof-pilot/Cargo.toml b/crates/proof-pilot/Cargo.toml
index 92f016a..b183da8 100644
--- a/crates/proof-pilot/Cargo.toml
+++ b/crates/proof-pilot/Cargo.toml
@@ -3,7 +3,14 @@ name = "proof-pilot"
 version.workspace = true
 edition.workspace = true
 license.workspace = true
-description = "LLM-driven Lean proof completion loop via Claude CLI"
+description = "Kernel-arbitrated LLM proof completion for Lean 4, with anti-cheat and deterministic replay"
+repository = "https://github.com/LucidSamuel/scribe"
+homepage = "https://github.com/LucidSamuel/scribe/tree/main/crates/proof-pilot"
+documentation = "https://docs.rs/proof-pilot"
+readme = "README.md"
+keywords = ["lean", "theorem-proving", "llm", "formal-verification", "agent"]
+categories = ["development-tools", "mathematics", "science"]
+exclude = ["*.log"]
 
 [dependencies]
 serde = { version = "1", features = ["derive"] }
diff --git a/crates/proof-pilot/README.md b/crates/proof-pilot/README.md
new file mode 100644
index 0000000..687ffde
--- /dev/null
+++ b/crates/proof-pilot/README.md
@@ -0,0 +1,69 @@
+# proof-pilot
+
+**A kernel-arbitrated LLM proof-completion loop for Lean 4, with anti-cheat and
+deterministic replay.**
+
+Point it at a Lean file with a `sorry` and an LLM backend. The loop edits the
+proof body, compiles the exact target file with `lake build`, feeds the errors
+(or structured LSP goal states) back to the model, and repeats until the **Lean
+kernel** accepts or the budget runs out. The model writes the proof; the kernel
+decides.
+
+```sh
+proof-pilot MyProject/Theorem.lean --lake-dir MyProject --max-iters 10
+```
+
+## Why trust the output
+
+- **The kernel is the oracle.** Success is `lake build` exiting clean on the
+  exact target file — never the model's claim of success.
+- **Anti-cheat.** The patcher structurally cannot modify the theorem statement:
+  everything up to `:= by` comes from the file, the model only fills the body,
+  and the splice is bounded by the next top-level command. A token-aware scan
+  (comment- and string-skipping) rejects `sorry`, `axiom`, and `native_decide`
+  in anything that would be spliced.
+- **Deterministic replay.** Every session produces a journal (optionally saved
+  as versioned JSON) recording each iteration — prompt, response, patch, build
+  output, and under best-of-n every candidate plus which one was accepted.
+  `--replay transcript.json` re-applies a session without calling any LLM, and
+  refuses on Lean-toolchain or Mathlib-revision mismatch unless you pass
+  `--allow-toolchain-mismatch`.
+- **Best-of-n sampling, soundness-free.** `--samples-per-iter K` fires K
+  attempts per iteration and lets the kernel filter: candidates are hash-
+  deduplicated, tried shortest-first, and the first to build wins. A wrong
+  candidate costs a build, never a false acceptance.
+
+## Backends
+
+`claude` (Claude CLI, default) · `anthropic` (Messages API) · `openai` ·
+any OpenAI-compatible endpoint (`openai-compat`, vLLM, ollama, hosted provers)
+via `--backend`, `--model`, `--api-key`, `--base-url`.
+
+## Feedback modes
+
+Default is raw `lake build` output. `--lsp` switches to structured Lean
+language-server feedback — goal states, hypotheses, tactic probes, and lemma
+search — via a bundled Python bridge over
+[`leanclient`](https://pypi.org/project/leanclient/). Final verification always
+uses `lake build` regardless of mode.
+
+## Extras
+
+- `--notes NOTES.md` — a human-readable debugging report mapping common Lean
+  error shapes to concrete guidance (embedders can attach their own
+  worked-example citations via `notes::NotesStyle`).
+- `--save-transcript session.json` — versioned JSON transcript with toolchain
+  and Mathlib-revision pinning.
+
+## Provenance
+
+Extracted from [scribe](https://github.com/LucidSamuel/scribe), where this loop
+proves soundness theorems for zero-knowledge circuit gadgets — and runs
+*adversarially* (proving negations to hunt counterexamples), which works
+unchanged because refutations answer to the same kernel. The loop itself is
+domain-agnostic: it needs a Lake project and a theorem, not any particular
+mathematics.
+
+## License
+
+MIT
diff --git a/crates/proof-pilot/examples/prove_sum_comm.rs b/crates/proof-pilot/examples/prove_sum_comm.rs
new file mode 100644
index 0000000..b2292b8
--- /dev/null
+++ b/crates/proof-pilot/examples/prove_sum_comm.rs
@@ -0,0 +1,50 @@
+//! Non-ZK example: complete an ordinary Mathlib-flavoured proof.
+//!
+//! Demonstrates that proof-pilot is domain-agnostic — the target here is a
+//! plain arithmetic lemma, not a circuit-soundness theorem. Requires:
+//! - a Lake project directory (pass as argv[1]) whose `lakefile` can build
+//!   files in its root, with Mathlib available if your theorem needs it;
+//! - the `claude` CLI on PATH (or edit `make_backend` below).
+//!
+//! ```sh
+//! cargo run -p proof-pilot --example prove_sum_comm -- path/to/lake-project
+//! ```
+
+use proof_pilot::backend::make_backend;
+use proof_pilot::session::{self, SessionConfig, SessionResult};
+
+const SCAFFOLD: &str = r#"import Mathlib.Tactic.Ring
+
+/-- An ordinary lemma with a `sorry` for the loop to fill. -/
+theorem sum_sq_comm (a b : ℕ) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by
+  sorry
+"#;
+
+fn main() {
+    let lake_dir = std::env::args()
+        .nth(1)
+        .expect("usage: prove_sum_comm <lake-project-dir>");
+    let lean_file = format!("{lake_dir}/ProofPilotExample.lean");
+    std::fs::write(&lean_file, SCAFFOLD).expect("write scaffold");
+
+    let backend = make_backend("claude", None, None, None).expect("backend");
+    let config = SessionConfig {
+        lean_file: lean_file.clone(),
+        lake_dir,
+        max_iterations: 5,
+        system_prompt: None,
+        transcript: None,
+        use_lsp: false,
+        samples_per_iter: 1,
+    };
+
+    match session::run(&config, backend.as_ref()).0 {
+        SessionResult::Proven { iterations } => {
+            println!("kernel accepted after {iterations} iteration(s): {lean_file}")
+        }
+        SessionResult::Exhausted { iterations, .. } => {
+            println!("no proof in {iterations} iteration(s)")
+        }
+        SessionResult::Failed(msg) => eprintln!("error: {msg}"),
+    }
+}
diff --git a/crates/proof-pilot/scripts/lsp-server.py b/crates/proof-pilot/scripts/lsp-server.py
new file mode 100755
index 0000000..c922ec9
--- /dev/null
+++ b/crates/proof-pilot/scripts/lsp-server.py
@@ -0,0 +1,316 @@
+#!/usr/bin/env python3
+"""Long-running LSP feedback server for proof-pilot.
+
+Communicates via newline-delimited JSON on stdin/stdout.
+
+Commands:
+  {"cmd": "feedback", "file": "ZkGadgets/Foo.lean"}
+    → Get diagnostics + goal states (opens file if needed).
+
+  {"cmd": "update", "file": "ZkGadgets/Foo.lean"}
+    → Close & reopen file to pick up disk changes, then get feedback.
+
+  {"cmd": "search", "query": "sub_eq_zero", "num_results": 5}
+    → Search Mathlib via loogle for relevant lemmas.
+
+  {"cmd": "probe", "file": "ZkGadgets/Foo.lean", "line": 12, "col": 2,
+   "tactics": ["ring", "simp", "linear_combination h"]}
+    → Try each tactic at a position and report which ones make progress.
+
+  {"cmd": "quit"}
+    → Shut down cleanly.
+
+File paths are relative to the Lean project root.
+"""
+import sys
+import json
+import re
+from leanclient import LeanLSPClient
+
+
+def gather_feedback(client, file_path):
+    """Get diagnostics and goal states for a Lean file."""
+    result = client.get_diagnostics(file_path)
+
+    diagnostics = []
+    for d in result.diagnostics:
+        rng = d.get("range", {})
+        start = rng.get("start", {})
+        diagnostics.append({
+            "line": start.get("line", 0),
+            "col": start.get("character", 0),
+            "severity": d.get("severity", 1),
+            "message": d.get("message", ""),
+        })
+
+    # Collect positions to query for goal state:
+    # 1. Error diagnostic positions
+    # 2. Actual `sorry` token positions in the file content
+    query_positions = set()
+    for d in diagnostics:
+        if d["severity"] == 1:  # errors
+            query_positions.add((d["line"], d["col"]))
+
+    # Find sorry tokens in the file to get their tactic state
+    try:
+        content = client.get_file_content(file_path)
+        for i, line_text in enumerate(content.splitlines()):
+            col = line_text.find("sorry")
+            if col >= 0:
+                query_positions.add((i, col))
+    except Exception:
+        pass
+
+    goals = []
+    for (line, col) in sorted(query_positions):
+        try:
+            goal = client.get_goal(file_path, line, col)
+            if goal and isinstance(goal, dict):
+                goal_list = goal.get("goals", [])
+                if goal_list:
+                    goals.append({
+                        "line": line,
+                        "col": col,
+                        "goals": goal_list,
+                    })
+        except Exception:
+            pass
+
+    # Also check for forbidden tactic warnings (sorry, axiom, native_decide)
+    has_forbidden = any(
+        "sorry" in d["message"].lower() or
+        "axiom" in d["message"].lower() or
+        "native_decide" in d["message"].lower()
+        for d in diagnostics
+        if d["severity"] == 2  # warnings
+    )
+
+    return {
+        "success": result.success and not has_forbidden,
+        "diagnostics": diagnostics,
+        "goals": goals,
+    }
+
+
+def search_loogle(query, num_results=5):
+    """Search Mathlib via loogle for relevant lemmas."""
+    try:
+        from lean_lsp_mcp.loogle import loogle_remote
+        results = loogle_remote(query, num_results)
+        if isinstance(results, str):
+            # Error message
+            return {"results": [], "error": results}
+        return {
+            "results": [
+                {"name": r.name, "type": str(r.type), "module": str(r.module)}
+                for r in results
+            ]
+        }
+    except Exception as e:
+        return {"results": [], "error": str(e)}
+
+
+def replace_span_at_position(line_text, col, replacement):
+    """Replace the tactic/expression span at col while preserving the rest of the line."""
+    col = max(0, min(col, len(line_text)))
+
+    start = col
+    while start < len(line_text) and line_text[start].isspace():
+        start += 1
+
+    if start < len(line_text) and col < len(line_text) and not line_text[col].isspace():
+        start = col
+        while start > 0:
+            prev = line_text[start - 1]
+            if prev.isspace() or prev in ";|":
+                break
+            if start >= 3 and line_text[start - 3:start] == "<;>":
+                break
+            start -= 1
+
+    end = start
+    while end < len(line_text):
+        if line_text.startswith("<;>", end):
+            break
+        if line_text[end] in ";|":
+            break
+        end += 1
+
+    while end > start and line_text[end - 1].isspace():
+        end -= 1
+
+    return f"{line_text[:start]}{replacement}{line_text[end:]}"
+
+
+def probe_tactics(client, file_path, line, col, tactics):
+    """Try each tactic at a position and report goal state / success."""
+    try:
+        content = client.get_file_content(file_path)
+    except Exception:
+        # File might not be open yet
+        client.get_diagnostics(file_path)
+        content = client.get_file_content(file_path)
+
+    lines = content.splitlines()
+
+    # Replace the tactic/expression span at (line, col), preserving other
+    # tactics/expressions on the same line.
+    if line >= len(lines):
+        return {"error": f"line {line} out of range (file has {len(lines)} lines)"}
+
+    results = []
+    for tactic in tactics:
+        modified_line = replace_span_at_position(lines[line], col, tactic)
+        modified_lines = lines[:line] + [modified_line] + lines[line + 1:]
+        modified_content = "\n".join(modified_lines)
+        if content.endswith("\n"):
+            modified_content += "\n"
+
+        try:
+            client.update_file_content(file_path, modified_content)
+            diags = client.get_diagnostics(file_path)
+
+            # Check for errors on this specific line
+            line_errors = [
+                d for d in diags.diagnostics
+                if d.get("range", {}).get("start", {}).get("line", -1) == line
+                and d.get("severity", 1) == 1
+            ]
+
+            # Get goal state after this tactic
+            goal = None
+            # Query goal at the line AFTER, to see remaining goals
+            if line + 1 < len(modified_lines):
+                try:
+                    goal_resp = client.get_goal(file_path, line + 1, 0)
+                    if goal_resp and isinstance(goal_resp, dict):
+                        goal = goal_resp.get("goals", [])
+                except Exception:
+                    pass
+
+            if not line_errors and diags.success:
+                results.append({
+                    "tactic": tactic,
+                    "status": "solved",
+                    "remaining_goals": goal or [],
+                })
+            elif not line_errors:
+                results.append({
+                    "tactic": tactic,
+                    "status": "progress",
+                    "remaining_goals": goal or [],
+                })
+            else:
+                err_msg = line_errors[0].get("message", "error")
+                results.append({
+                    "tactic": tactic,
+                    "status": "failed",
+                    "error": err_msg.split("\n")[0],
+                })
+        except Exception as e:
+            results.append({
+                "tactic": tactic,
+                "status": "error",
+                "error": str(e),
+            })
+
+    # Restore original content
+    try:
+        client.update_file_content(file_path, content)
+    except Exception:
+        pass
+
+    return {"results": results}
+
+
+def main():
+    if len(sys.argv) < 2:
+        print(json.dumps({"error": "usage: lsp-server.py <lean-project-path>"}),
+              flush=True)
+        sys.exit(1)
+
+    project_path = sys.argv[1]
+    print(json.dumps({"status": "ready"}), flush=True)
+
+    client = None
+    try:
+        client = LeanLSPClient(project_path, initial_build=False)
+        print(json.dumps({"status": "initialized"}), flush=True)
+
+        for line in sys.stdin:
+            line = line.strip()
+            if not line:
+                continue
+
+            try:
+                cmd = json.loads(line)
+            except json.JSONDecodeError as e:
+                print(json.dumps({"error": f"invalid JSON: {e}"}), flush=True)
+                continue
+
+            action = cmd.get("cmd", "")
+
+            if action == "quit":
+                print(json.dumps({"status": "quit"}), flush=True)
+                break
+
+            elif action == "feedback":
+                file_path = cmd.get("file", "")
+                try:
+                    fb = gather_feedback(client, file_path)
+                    print(json.dumps(fb), flush=True)
+                except Exception as e:
+                    print(json.dumps({"error": str(e)}), flush=True)
+
+            elif action == "update":
+                file_path = cmd.get("file", "")
+                try:
+                    # Close file so LSP re-reads from disk
+                    try:
+                        client.close_files([file_path])
+                    except Exception:
+                        pass
+                    fb = gather_feedback(client, file_path)
+                    print(json.dumps(fb), flush=True)
+                except Exception as e:
+                    print(json.dumps({"error": str(e)}), flush=True)
+
+            elif action == "search":
+                query = cmd.get("query", "")
+                num = cmd.get("num_results", 5)
+                try:
+                    result = search_loogle(query, num)
+                    print(json.dumps(result), flush=True)
+                except Exception as e:
+                    print(json.dumps({"results": [], "error": str(e)}),
+                          flush=True)
+
+            elif action == "probe":
+                file_path = cmd.get("file", "")
+                line = cmd.get("line", 0)
+                col = cmd.get("col", 0)
+                tactics = cmd.get("tactics", [])
+                try:
+                    result = probe_tactics(client, file_path, line, col, tactics)
+                    print(json.dumps(result), flush=True)
+                except Exception as e:
+                    print(json.dumps({"error": str(e)}), flush=True)
+
+            else:
+                print(json.dumps({"error": f"unknown command: {action}"}),
+                      flush=True)
+
+    except Exception as e:
+        print(json.dumps({"error": f"init failed: {e}"}), flush=True)
+        sys.exit(1)
+
+    finally:
+        if client:
+            try:
+                client.close()
+            except Exception:
+                pass
+
+
+if __name__ == "__main__":
+    main()
diff --git a/crates/proof-pilot/src/lib.rs b/crates/proof-pilot/src/lib.rs
index 5aca1cf..9afeff7 100644
--- a/crates/proof-pilot/src/lib.rs
+++ b/crates/proof-pilot/src/lib.rs
@@ -1,3 +1,66 @@
+//! # proof-pilot
+//!
+//! A kernel-arbitrated LLM proof-completion loop for Lean 4, with anti-cheat
+//! and deterministic replay.
+//!
+//! Point it at a Lean file containing a theorem with a `sorry` and a backend
+//! (Claude CLI, the Anthropic API, or any OpenAI-compatible endpoint). The loop
+//! edits the proof body, compiles the exact target file with `lake build`,
+//! feeds the errors (or structured LSP goal states) back to the model, and
+//! repeats until the **Lean kernel** accepts or the budget runs out. The model
+//! writes the proof; the kernel decides — "I proved it" means the kernel
+//! checked it.
+//!
+//! ## Why trust the output
+//!
+//! - **The kernel is the oracle.** Success is `lake build` exiting clean on the
+//!   exact target file — never the model's claim.
+//! - **Anti-cheat.** The patcher structurally cannot modify the theorem
+//!   statement (everything up to `:= by` comes from the file; the model only
+//!   fills the body, bounded by the next top-level command), and a token-aware
+//!   scan rejects `sorry` / `axiom` / `native_decide` in what would be spliced.
+//! - **Deterministic replay.** Every session yields a [`journal::SessionJournal`]
+//!   (optionally saved as versioned JSON via [`transcript`]) recording each
+//!   iteration — and under best-of-n sampling, every candidate plus the
+//!   acceptance index. [`replay`] re-applies a transcript without an LLM,
+//!   refusing on toolchain/Mathlib mismatch unless overridden.
+//! - **Best-of-n, soundness-free.** [`session::SessionConfig::samples_per_iter`]
+//!   fires k attempts per iteration and lets the kernel filter: candidates are
+//!   deduplicated, tried shortest-first, first to build wins. A wrong candidate
+//!   costs a build, never a false acceptance.
+//!
+//! ## Quick start (library)
+//!
+//! ```no_run
+//! use proof_pilot::backend::make_backend;
+//! use proof_pilot::session::{self, SessionConfig};
+//!
+//! let backend = make_backend("claude", None, None, None).unwrap();
+//! let config = SessionConfig {
+//!     lean_file: "MyProject/Theorem.lean".into(),
+//!     lake_dir: "MyProject".into(),
+//!     max_iterations: 10,
+//!     system_prompt: None,
+//!     transcript: None,
+//!     use_lsp: false,
+//!     samples_per_iter: 1,
+//! };
+//! let (result, journal) = session::run(&config, backend.as_ref());
+//! println!("{result:?} after {} iteration(s)", journal.iterations.len());
+//! ```
+//!
+//! The `proof-pilot` binary wraps the same loop as a CLI; run
+//! `proof-pilot --help`.
+//!
+//! ## Scope
+//!
+//! proof-pilot is domain-agnostic: it needs a Lake project and a theorem, not
+//! any particular mathematics. It was extracted from
+//! [scribe](https://github.com/LucidSamuel/scribe), where it proves soundness
+//! theorems for zero-knowledge circuit gadgets against the kernel; scribe also
+//! runs the loop *adversarially* (proving negations to hunt counterexamples),
+//! which works unchanged because refutations answer to the same kernel.
+
 pub mod backend;
 pub mod journal;
 pub mod lean_runner;
diff --git a/crates/proof-pilot/src/lsp_feedback.rs b/crates/proof-pilot/src/lsp_feedback.rs
index d0d1855..42503da 100644
--- a/crates/proof-pilot/src/lsp_feedback.rs
+++ b/crates/proof-pilot/src/lsp_feedback.rs
@@ -221,7 +221,22 @@ impl Drop for LspBridge {
     }
 }
 
+/// The Python LSP bridge, embedded so the published crate is self-contained.
+/// (The canonical copy lives in the crate at scripts/lsp-server.py; the scribe
+/// repo also keeps one at the repo root for direct use.)
+const LSP_SERVER_SOURCE: &str = include_str!("../scripts/lsp-server.py");
+
 fn find_script() -> Result<String, String> {
+    // Explicit override, then repo-local copies (development), then the
+    // embedded source materialized into a stable per-user temp path.
+    if let Ok(path) = std::env::var("PROOF_PILOT_LSP_SERVER") {
+        if Path::new(&path).exists() {
+            return Ok(path);
+        }
+        return Err(format!(
+            "PROOF_PILOT_LSP_SERVER points at a missing file: {path}"
+        ));
+    }
     let candidates = [
         "scripts/lsp-server.py",
         "../scripts/lsp-server.py",
@@ -232,7 +247,12 @@ fn find_script() -> Result<String, String> {
             return Ok(c.to_string());
         }
     }
-    Err("could not find scripts/lsp-server.py — run from the repo root".to_string())
+    let dir = std::env::temp_dir().join("proof-pilot");
+    std::fs::create_dir_all(&dir).map_err(|e| format!("create {}: {e}", dir.display()))?;
+    let path = dir.join("lsp-server.py");
+    std::fs::write(&path, LSP_SERVER_SOURCE)
+        .map_err(|e| format!("write embedded lsp-server.py: {e}"))?;
+    Ok(path.to_string_lossy().into_owned())
 }
 
 fn parse_feedback(json_str: &str) -> Result<LspFeedback, String> {
diff --git a/crates/proof-pilot/src/notes.rs b/crates/proof-pilot/src/notes.rs
index 13015f3..d6c7e51 100644
--- a/crates/proof-pilot/src/notes.rs
+++ b/crates/proof-pilot/src/notes.rs
@@ -5,7 +5,24 @@
 
 use crate::journal::SessionJournal;
 
-/// Render a `SessionJournal` as a Markdown "notes" document.
+/// Embedder-supplied styling for the notes document: worked-example citations
+/// keyed by guidance pattern, appended to the matching guidance block. The
+/// crate's own guidance is domain-generic; a host project (e.g. scribe) points
+/// each pattern at its own solved-proof corpus.
+///
+/// Recognized pattern keys: `"linarith_zmod"`, `"zero_divisor"`,
+/// `"zmod_unsolved"`, `"fin_sums"`, `"unsolved_generic"`. The
+/// `reference_library` line is appended to the generic fallback checklist.
+#[derive(Default)]
+pub struct NotesStyle {
+    /// Pattern key → citation sentence (e.g. "See `lean/ZkGadgets/RangeCheck.lean` …").
+    pub citations: std::collections::BTreeMap<String, String>,
+    /// Closing pointer to a reference corpus of solved proofs.
+    pub reference_library: Option<String>,
+}
+
+/// Render a `SessionJournal` as a Markdown "notes" document with generic,
+/// domain-neutral guidance (no project-specific citations).
 ///
 /// The document contains:
 /// 1. Title, theorem, and final outcome.
@@ -13,6 +30,11 @@ use crate::journal::SessionJournal;
 /// 3. Last ≤ 3 iterations: source diff, build errors, patch status.
 /// 4. Suggested next steps with tactic references.
 pub fn render_notes(journal: &SessionJournal) -> String {
+    render_notes_styled(journal, &NotesStyle::default())
+}
+
+/// `render_notes` with embedder-supplied worked-example citations.
+pub fn render_notes_styled(journal: &SessionJournal, style: &NotesStyle) -> String {
     let mut out = String::new();
 
     // ── 1. Header ────────────────────────────────────────────────────────────
@@ -66,7 +88,7 @@ pub fn render_notes(journal: &SessionJournal) -> String {
     }
 
     // Plain-English guidance based on error/goal patterns.
-    let guidance = pick_guidance(last_errors, &last_goals);
+    let guidance = pick_guidance(last_errors, &last_goals, style);
     out.push_str("### Guidance\n\n");
     out.push_str(&guidance);
     out.push_str("\n\n");
@@ -121,7 +143,7 @@ pub fn render_notes(journal: &SessionJournal) -> String {
         .take(5)
         .collect();
 
-    let tactic_suggestions = pick_tactic_suggestions(last_errors, &last_goals);
+    let tactic_suggestions = pick_tactic_suggestions(last_errors, &last_goals, style);
     out.push_str(&tactic_suggestions);
     out.push('\n');
 
@@ -152,48 +174,61 @@ fn outcome_label(outcome: &str) -> &str {
 /// Map common error/goal patterns to actionable guidance.
 ///
 /// Matching order matters — more specific patterns first.
-fn pick_guidance(build_errors: &str, goal_states: &[&str]) -> String {
+fn pick_guidance(build_errors: &str, goal_states: &[&str], style: &NotesStyle) -> String {
+    let cite = |key: &str, text: String| -> String {
+        match style.citations.get(key) {
+            Some(c) => format!("{text} {c}"),
+            None => text,
+        }
+    };
     let combined = format!("{build_errors}\n{}", goal_states.join("\n"));
 
     if combined.contains("linarith") {
-        return "**`linarith` does not work on `ZMod p`** — the field is not linearly ordered. \
-                Instead, try `linear_combination <expr>` to derive equalities by arithmetic, \
-                or `field_simp` followed by `ring` for purely algebraic goals. \
-                See `lean/ZkGadgets/RangeCheck.lean` for a worked example that uses \
-                `linear_combination` to close ZMod goals."
-            .to_string();
+        return cite(
+            "linarith_zmod",
+            "**`linarith` does not work on `ZMod p`** — the field is not linearly ordered. \
+             Instead, try `linear_combination <expr>` to derive equalities by arithmetic, \
+             or `field_simp` followed by `ring` for purely algebraic goals."
+                .to_string(),
+        );
     }
 
     if combined.contains("mul_eq_zero") || combined.contains("IsUnit") {
-        return "**Goal involves a zero-divisor argument.** \
-                In a prime field `ZMod p`, use `mul_eq_zero.mp h` to case-split: \
-                `h : a * b = 0` gives you `a = 0 ∨ b = 0`. \
-                You need `haveI : Fact (Nat.Prime p) := ⟨p_prime_proof⟩` in scope, \
-                which unlocks `NoZeroDivisors`. \
-                See `lean/ZkGadgets/HalvaRangeCheck.lean` for the full pattern."
-            .to_string();
+        return cite(
+            "zero_divisor",
+            "**Goal involves a zero-divisor argument.** \
+             In a prime field `ZMod p`, use `mul_eq_zero.mp h` to case-split: \
+             `h : a * b = 0` gives you `a = 0 ∨ b = 0`. \
+             You need `haveI : Fact (Nat.Prime p) := ⟨p_prime_proof⟩` in scope, \
+             which unlocks `NoZeroDivisors`."
+                .to_string(),
+        );
     }
 
     if combined.contains("ZMod") && combined.contains("unsolved goals") {
-        return "**Unsolved goals in `ZMod p`.** \
-                Common moves: \n\
-                - `rcases h01 i with h | h <;> simp [h]` to case-split bit-boolean hypotheses.\n\
-                - `push_cast` to coerce `ℕ` literals into `ZMod p` before `ring`.\n\
-                - `linear_combination <expr>` when the goal is a linear identity.\n\
-                - `norm_num` for concrete numeric equalities.\n\
-                See `lean/ZkGadgets/RangeCheck.lean` (the `hcast` block) for an example \
-                of coercing natural-number bits into `ZMod p`."
-            .to_string();
+        return cite(
+            "zmod_unsolved",
+            "**Unsolved goals in `ZMod p`.** \
+             Common moves: \n\
+             - `rcases h01 i with h | h <;> simp [h]` to case-split bit-boolean hypotheses.\n\
+             - `push_cast` to coerce `ℕ` literals into `ZMod p` before `ring`.\n\
+             - `linear_combination <expr>` when the goal is a linear identity.\n\
+             - `norm_num` for concrete numeric equalities.\n"
+                .to_string(),
+        );
     }
 
     if combined.contains("unsolved goals")
         && (combined.contains("Fin") || combined.contains("Finset"))
     {
-        return "**Unsolved goals involving `Fin` or `Finset`.** \
-                Try `Finset.sum_le_sum` for bounding sums, `Fin.sum_univ_succ` to unroll \
-                finite sums by induction, and `omega` for the resulting arithmetic on `ℕ`. \
-                `simp only [Fin.val_zero, Fin.val_succ]` often clears `Fin` coercions. \
-                See `lean/ZkGadgets/RangeCheck.lean` (the `hlt` block) for a complete worked example.".to_string();
+        return cite(
+            "fin_sums",
+            "**Unsolved goals involving `Fin` or `Finset`.** \
+             Try `Finset.sum_le_sum` for bounding sums, `Fin.sum_univ_succ` to unroll \
+             finite sums by induction, and `omega` for the resulting arithmetic on `ℕ`. \
+             `simp only [Fin.val_zero, Fin.val_succ]` often clears `Fin` coercions."
+                .to_string(),
+        );
     }
 
     if combined.contains("unknown identifier") || combined.contains("unknown tactic") {
@@ -216,14 +251,16 @@ fn pick_guidance(build_errors: &str, goal_states: &[&str]) -> String {
     }
 
     if combined.contains("unsolved goals") {
-        return "**Unsolved goals remain.** \
-                Try `exact?` or `apply?` to let Lean suggest a closing lemma. \
-                `simp` with the relevant hypotheses often closes simple goals: `simp [h1, h2]`. \
-                For ring-equalities in a field, `ring` or `field_simp; ring` frequently works. \
-                For boolean facts (bit = 0 ∨ bit = 1), use `rcases` to split on cases \
-                and close each branch with `simp [h]`. \
-                See `lean/ZkGadgets/RangeCheck.lean` for worked patterns."
-            .to_string();
+        return cite(
+            "unsolved_generic",
+            "**Unsolved goals remain.** \
+             Try `exact?` or `apply?` to let Lean suggest a closing lemma. \
+             `simp` with the relevant hypotheses often closes simple goals: `simp [h1, h2]`. \
+             For ring-equalities in a field, `ring` or `field_simp; ring` frequently works. \
+             For boolean facts (bit = 0 ∨ bit = 1), use `rcases` to split on cases \
+             and close each branch with `simp [h]`."
+                .to_string(),
+        );
     }
 
     if combined.contains("failed to synthesize") || combined.contains("instance") {
@@ -236,26 +273,27 @@ fn pick_guidance(build_errors: &str, goal_states: &[&str]) -> String {
     }
 
     // Generic fallback
-    "**No specific pattern matched.** General checklist:\n\
+    let mut fallback = "**No specific pattern matched.** General checklist:\n\
      - Inspect the goal state carefully: what is on each side of `⊢`?\n\
      - Try `simp`, `ring`, `linarith` (only on ordered types), or `omega` (for `ℕ`/`ℤ`).\n\
      - For field arithmetic, `linear_combination` can close many goals that `ring` cannot.\n\
-     - When stuck, add `have h : <intermediate claim> := by <proof>` to build up evidence.\n\
-     - The proven gadgets in `lean/ZkGadgets/` are your reference library — \
-       `RangeCheck.lean`, `ConditionalSelect.lean`, `PoseidonSbox.lean`, \
-       `NonzeroCheck.lean`, `EdwardsAddition.lean`."
-        .to_string()
+     - When stuck, add `have h : <intermediate claim> := by <proof>` to build up evidence."
+        .to_string();
+    if let Some(lib) = &style.reference_library {
+        fallback.push_str(&format!("\n     - {lib}"));
+    }
+    fallback
 }
 
 // ─── Tactic suggestions ───────────────────────────────────────────────────────
 
-fn pick_tactic_suggestions(build_errors: &str, goal_states: &[&str]) -> String {
+fn pick_tactic_suggestions(build_errors: &str, goal_states: &[&str], style: &NotesStyle) -> String {
     let combined = format!("{build_errors}\n{}", goal_states.join("\n"));
 
     let mut items: Vec<&str> = Vec::new();
 
     if combined.contains("linarith") || combined.contains("ZMod") {
-        items.push("Replace `linarith` with `linear_combination <expr>` for ZMod goals (see `lean/ZkGadgets/RangeCheck.lean`).");
+        items.push("Replace `linarith` with `linear_combination <expr>` for ZMod goals.");
         items.push("Use `field_simp; ring` for purely algebraic equalities in a prime field.");
     }
 
@@ -281,13 +319,18 @@ fn pick_tactic_suggestions(build_errors: &str, goal_states: &[&str]) -> String {
         items.push("Add `haveI : Fact (Nat.Prime p) := ⟨p_prime_proof⟩` at the top of the proof to unlock field instances.");
     }
 
-    if items.is_empty() {
-        items.push("Try `exact?`, `apply?`, or `simp?` to let Lean suggest the next step.");
-        items.push("Consult `lean/ZkGadgets/RangeCheck.lean` for a fully worked gadget proof.");
+    let mut owned_items: Vec<String> = items.iter().map(|s| s.to_string()).collect();
+    if owned_items.is_empty() {
+        owned_items.push(
+            "Try `exact?`, `apply?`, or `simp?` to let Lean suggest the next step.".to_string(),
+        );
+        if let Some(lib) = &style.reference_library {
+            owned_items.push(format!("Consult {lib}"));
+        }
     }
 
     let mut out = String::new();
-    for item in &items {
+    for item in &owned_items {
         out.push_str(&format!("- {item}\n"));
     }
     out
@@ -475,15 +518,28 @@ mod tests {
             false,
         );
         let journal = make_journal("exhausted", vec![iter]);
-        let notes = render_notes(&journal);
 
+        // Generic rendering: domain-neutral guidance, no project citations.
+        let notes = render_notes(&journal);
         assert!(
             notes.contains("linear_combination"),
             "must suggest linear_combination for linarith errors"
         );
         assert!(
-            notes.contains("RangeCheck.lean"),
-            "must cite RangeCheck.lean"
+            !notes.contains("RangeCheck.lean"),
+            "generic notes must not cite a host project's corpus"
+        );
+
+        // Styled rendering: the embedder's citation is appended to the pattern.
+        let mut style = NotesStyle::default();
+        style.citations.insert(
+            "linarith_zmod".to_string(),
+            "See `lean/ZkGadgets/RangeCheck.lean` for a worked example.".to_string(),
+        );
+        let styled = render_notes_styled(&journal, &style);
+        assert!(
+            styled.contains("lean/ZkGadgets/RangeCheck.lean"),
+            "styled notes must carry the embedder's citation"
         );
     }
 
diff --git a/crates/scribe-cli/src/orchestrate.rs b/crates/scribe-cli/src/orchestrate.rs
index 2775cec..f6f301b 100644
--- a/crates/scribe-cli/src/orchestrate.rs
+++ b/crates/scribe-cli/src/orchestrate.rs
@@ -7,7 +7,7 @@ use std::process;
 use halva_bridge::{parse_halva_output, scaffold_raw, scaffold_soundness, SpecConfig};
 use proof_pilot::backend::make_backend;
 use proof_pilot::journal::SessionJournal;
-use proof_pilot::notes::render_notes;
+use proof_pilot::notes::{render_notes_styled, NotesStyle};
 use proof_pilot::session::{self, SessionConfig, SessionResult};
 use proof_pilot::transcript;
 
@@ -232,9 +232,51 @@ pub fn run_verify(args: VerifyArgs) {
     handle_session_result(result, &out_path);
 }
 
+/// scribe's notes style: point each guidance pattern at the proven gadgets in
+/// `lean/ZkGadgets/` (the worked-example corpus proof-pilot's generic guidance
+/// deliberately does not know about).
+fn scribe_notes_style() -> NotesStyle {
+    let mut style = NotesStyle::default();
+    let cites = [
+        (
+            "linarith_zmod",
+            "See `lean/ZkGadgets/RangeCheck.lean` for a worked example that uses \
+             `linear_combination` to close ZMod goals.",
+        ),
+        (
+            "zero_divisor",
+            "See `lean/ZkGadgets/HalvaRangeCheck.lean` for the full pattern.",
+        ),
+        (
+            "zmod_unsolved",
+            "See `lean/ZkGadgets/RangeCheck.lean` (the `hcast` block) for an example \
+             of coercing natural-number bits into `ZMod p`.",
+        ),
+        (
+            "fin_sums",
+            "See `lean/ZkGadgets/RangeCheck.lean` (the `hlt` block) for a complete \
+             worked example.",
+        ),
+        (
+            "unsolved_generic",
+            "See `lean/ZkGadgets/RangeCheck.lean` for worked patterns.",
+        ),
+    ];
+    for (key, text) in cites {
+        style.citations.insert(key.to_string(), text.to_string());
+    }
+    style.reference_library = Some(
+        "The proven gadgets in `lean/ZkGadgets/` are your reference library — \
+         `RangeCheck.lean`, `ConditionalSelect.lean`, `PoseidonSbox.lean`, \
+         `NonzeroCheck.lean`, `EdwardsAddition.lean`."
+            .to_string(),
+    );
+    style
+}
+
 /// Render and write a NOTES.md debugging report from the session journal.
 fn write_notes(journal: &SessionJournal, path: &str) {
-    let md = render_notes(journal);
+    let md = render_notes_styled(journal, &scribe_notes_style());
     match fs::write(path, md) {
         Ok(()) => eprintln!("[scribe] notes written to: {path}"),
         Err(e) => eprintln!("[scribe] warning: could not write notes: {e}"),