scribe judge (SOUND / UNSOUND / UNDETERMINED) + best-of-n sampling

README.md

@@ -137,6 +137,28 @@ scribe refute --gadget examples/range-check/gadget.toml \
 
 The gadget's soundness statement is emitted at a concrete small prime, **negated**, and an LLM refuter loop (system prompt `prompts/lean-refuter.md`) tries to prove the negation — i.e. exhibit witness values that satisfy every constraint while violating the spec. A kernel-accepted refutation is exactly as trustworthy as a kernel-accepted proof, and carries its own `#audit_axioms` gate. Exit codes: `2` = **REFUTED** (the circuit is under-constrained or the spec is wrong — the counterexample is in the output file), `0` = **SURVIVED** (no refutation within budget; evidence, not proof), `1` = infrastructure error.
 
+### `scribe judge`
+
+The verdict engine as one command: prove AND attack, and say which side won.
+
+```sh
+scribe judge --gadget examples/range-check/gadget.toml \
+  [--prove-iters N] [--refute-iters M] [--prime P] [--samples-per-iter K]
+```
+
+The prover runs first (a kernel-accepted proof settles the question — no counterexample can exist, and sound gadgets usually prove in an iteration or two). Only if proving exhausts its budget does the adversarial refuter run. The verdict is backed by a kernel-checked artifact whenever it is not UNDETERMINED:
+
+| Exit code | Verdict | Meaning |
+|---|---|---|
+| `0` | **SOUND** | kernel-accepted proof of the spec (path printed) |
+| `1` | **UNDETERMINED** | neither proof nor refutation within budget |
+| `2` | **UNSOUND** | kernel-checked counterexample (path printed) |
+| `3` | — | infrastructure error |
+
+The exit codes are stable and documented so third parties can script `scribe judge` in their own CI.
+
+**Best-of-n sampling.** `--samples-per-iter K` (also on `verify`, `refute`, and `proof-pilot`) fires K attempts per iteration and lets the kernel filter: candidates are deduplicated, tried shortest-first, and the first to build wins. Parallel sampling is soundness-free — a wrong candidate costs a build, never a false acceptance — and the transcript records every candidate plus the acceptance index, so `--replay` determinism is preserved.
+
 ### `scribe init`
 
 Generates the editable Halva extractor project that `scribe verify --circuit` expects.

crates/bench/src/main.rs

@@ -419,6 +419,7 @@ fn main() {
                     system_prompt: system_prompt.clone(),
                     transcript: Some(transcript_path),
                     use_lsp: *mode == Mode::Lsp,
+                    samples_per_iter: 1,
                 };
 
                 eprint!(

crates/halva-bridge/src/lib.rs

@@ -926,7 +926,12 @@ private theorem helper : True := by
         };
         let combined = scaffold_soundness(&halva, &config);
         let re_pos = combined.find(reenable).expect("re-enable present");
-        assert!(combined.find("set_option linter.unusedVariables false").unwrap() < re_pos);
+        assert!(
+            combined
+                .find("set_option linter.unusedVariables false")
+                .unwrap()
+                < re_pos
+        );
         assert!(re_pos < combined.find("def Spec").unwrap());
 
         // Raw mode: same placement, before the snippet body.

crates/halva-bridge/src/main.rs

@@ -37,6 +37,7 @@ fn main() {
     let mut system_prompt_file = Some(DEFAULT_SYSTEM_PROMPT.to_string());
     let mut transcript = None;
     let mut use_lsp = false;
+    let mut samples_per_iter = 1u32;
     let mut backend_name = String::from("claude");
     let mut api_key: Option<String> = None;
     let mut base_url: Option<String> = None;
@@ -76,6 +77,16 @@ fn main() {
             }
             "--transcript" => transcript = Some(flag_value(&args, &mut i, "--transcript")),
             "--lsp" => use_lsp = true,
+            "--samples-per-iter" => {
+                samples_per_iter = flag_value(&args, &mut i, "--samples-per-iter")
+                    .parse()
+                    .ok()
+                    .filter(|&n| n >= 1)
+                    .unwrap_or_else(|| {
+                        eprintln!("invalid --samples-per-iter value (must be >= 1)");
+                        process::exit(1);
+                    });
+            }
             "--no-audit-gate" => audit_gate = false,
             "--backend" => backend_name = flag_value(&args, &mut i, "--backend"),
             "--api-key" => api_key = Some(flag_value(&args, &mut i, "--api-key")),
@@ -174,7 +185,10 @@ fn main() {
         })
     });
 
-    let backend = make_backend(&backend_name, model, api_key, base_url);
+    let backend = make_backend(&backend_name, model, api_key, base_url).unwrap_or_else(|e| {
+        eprintln!("error: {e}");
+        process::exit(1);
+    });
 
     let config = SessionConfig {
         lean_file: out_path.clone(),
@@ -183,6 +197,7 @@ fn main() {
         system_prompt,
         transcript,
         use_lsp,
+        samples_per_iter,
     };
 
     let (result, _journal) = session::run(&config, backend.as_ref());

crates/lean-emit/src/lib.rs

@@ -217,10 +217,16 @@ fn substitute_p(s: &str, prime: u64) -> String {
 /// is evidence, not proof, that the spec survives attack. The `#audit_axioms`
 /// gate holds refutations to the same axiom standard as proofs.
 pub fn emit_refutation(gadget: &Gadget, prime: u64) -> Result<String, EmitError> {
-    let spec = gadget.soundness_spec.as_ref().ok_or(EmitError::MissingSpec)?;
+    let spec = gadget
+        .soundness_spec
+        .as_ref()
+        .ok_or(EmitError::MissingSpec)?;
     let witness_names: Vec<&str> = gadget.witnesses.iter().map(|w| w.name.as_str()).collect();
     let witness_by_id = witness_map(gadget)?;
-    let theorem_name = format!("{}_refuted", sanitize_generated_ident(&gadget.name, "gadget"));
+    let theorem_name = format!(
+        "{}_refuted",
+        sanitize_generated_ident(&gadget.name, "gadget")
+    );
     let constraint_labels = generated_constraint_labels(gadget)?;
     let _ = constraint_labels; // labels documented in the header; antecedents are positional
 
@@ -263,14 +269,20 @@ pub fn emit_refutation(gadget: &Gadget, prime: u64) -> Result<String, EmitError>
         witness_names.join(" ")
     ));
     for h in &gadget.hypotheses {
-        out.push_str(&format!("        {} →\n", substitute_p(&h.lean_type, prime)));
+        out.push_str(&format!(
+            "        {} →\n",
+            substitute_p(&h.lean_type, prime)
+        ));
     }
     for c in &gadget.constraints {
         // constraint expressions can carry `(1 : ZMod p)`-style casts
         let expr = substitute_p(&emit_constraint_expr(c, &witness_by_id)?, prime);
         out.push_str(&format!("        {} = 0 →\n", expr));
     }
-    out.push_str(&format!("        ({})) := by\n  sorry\n", substitute_p(spec, prime)));
+    out.push_str(&format!(
+        "        ({})) := by\n  sorry\n",
+        substitute_p(spec, prime)
+    ));
 
     // -- audit gate: a refutation must rest on the trusted kernel axioms too
     out.push_str(&audit_gate(&theorem_name));

crates/proof-pilot/src/backend.rs

@@ -8,7 +8,11 @@
 use std::process::Command;
 
 /// Trait for LLM backends that can complete proof attempts.
-pub trait Backend {
+///
+/// `Send + Sync` so best-of-n sampling can issue concurrent `complete` calls
+/// from scoped threads; implementations take `&self` and hold no interior
+/// mutability.
+pub trait Backend: Send + Sync {
     /// Send a prompt to the model and return the response text.
     fn complete(&self, prompt: &str, system_prompt: Option<&str>) -> Result<String, BackendError>;
 
@@ -285,90 +289,89 @@ pub fn resolve_api_key(explicit: Option<&str>, env_var: &str) -> Option<String>
 }
 
 /// Require an API key, resolving from an explicit value or environment variable.
-///
-/// Prints an error and calls `std::process::exit(1)` if neither is available.
-pub fn require_api_key(explicit: Option<&str>, env_var: &str, backend: &str) -> String {
-    resolve_api_key(explicit, env_var).unwrap_or_else(|| {
-        eprintln!("{backend} backend requires --api-key or {env_var} env var");
-        std::process::exit(1);
-    })
+pub fn require_api_key(
+    explicit: Option<&str>,
+    env_var: &str,
+    backend: &str,
+) -> Result<String, String> {
+    resolve_api_key(explicit, env_var)
+        .ok_or_else(|| format!("{backend} backend requires --api-key or {env_var} env var"))
 }
 
-/// Construct a `Box<dyn Backend>` from a name, optional model, API key, and base URL.
-///
-/// Recognized names: `claude` / `claude-cli`, `anthropic`, `openai`, `leanstral`,
-/// `leanstral-local`, `openai-compat`.
-/// Exits the process with a diagnostic message if the name is unknown or required
-/// parameters (key, URL) are missing.
 /// Default model for the `claude`/`anthropic` backends when `--model` is not
 /// given. Kept in one place because retired models fail at request time (e.g.
 /// claude-sonnet-4-20250514 was retired 2026-06-15 and broke every default run).
 pub const DEFAULT_ANTHROPIC_MODEL: &str = "claude-sonnet-5";
 
+/// Construct a `Box<dyn Backend>` from a name, optional model, API key, and base URL.
+///
+/// Recognized names: `claude` / `claude-cli`, `anthropic`, `openai`, `leanstral`,
+/// `leanstral-local`, `openai-compat`.
+///
+/// Returns `Err` with a diagnostic message if the name is unknown or required
+/// parameters (key, URL) are missing — the CALLER owns the exit code, because
+/// different commands document different infrastructure-error codes (`scribe
+/// judge` exits 3, `scribe refute` exits 1).
 pub fn make_backend(
     name: &str,
     model: Option<String>,
     api_key: Option<String>,
     base_url: Option<String>,
-) -> Box<dyn Backend> {
+) -> Result<Box<dyn Backend>, String> {
     match name {
         "claude" | "claude-cli" => {
             let m = model.unwrap_or_else(|| DEFAULT_ANTHROPIC_MODEL.into());
-            Box::new(ClaudeCli::new(m))
+            Ok(Box::new(ClaudeCli::new(m)))
         }
         "anthropic" => {
             let m = model.unwrap_or_else(|| DEFAULT_ANTHROPIC_MODEL.into());
-            let key = require_api_key(api_key.as_deref(), "ANTHROPIC_API_KEY", "anthropic");
+            let key = require_api_key(api_key.as_deref(), "ANTHROPIC_API_KEY", "anthropic")?;
             let mut b = AnthropicApi::new(m, key);
             if let Some(url) = base_url {
                 b = b.with_base_url(url);
             }
-            Box::new(b)
+            Ok(Box::new(b))
         }
         "openai" => {
             let m = model.unwrap_or_else(|| "gpt-4o".into());
-            let key = require_api_key(api_key.as_deref(), "OPENAI_API_KEY", "openai");
+            let key = require_api_key(api_key.as_deref(), "OPENAI_API_KEY", "openai")?;
             let url = base_url.unwrap_or_else(|| "https://api.openai.com/v1".into());
-            Box::new(
+            Ok(Box::new(
                 OpenAiCompatible::new(m, Some(key), url)
                     .with_completion_tokens()
                     .with_name("openai".into()),
-            )
+            ))
         }
         "leanstral" => {
             let m = model.unwrap_or_else(|| "leanstral-v1".into());
-            let key = require_api_key(api_key.as_deref(), "LEANSTRAL_API_KEY", "leanstral");
-            let url = base_url.unwrap_or_else(|| {
-                eprintln!(
-                    "leanstral backend requires --base-url (e.g. https://api.leanstral.ai/v1)"
-                );
-                std::process::exit(1);
-            });
-            Box::new(OpenAiCompatible::new(m, Some(key), url).with_name("leanstral".into()))
+            let key = require_api_key(api_key.as_deref(), "LEANSTRAL_API_KEY", "leanstral")?;
+            let url = base_url.ok_or_else(|| {
+                "leanstral backend requires --base-url (e.g. https://api.leanstral.ai/v1)"
+                    .to_string()
+            })?;
+            Ok(Box::new(
+                OpenAiCompatible::new(m, Some(key), url).with_name("leanstral".into()),
+            ))
         }
         "leanstral-local" => {
             let m = model.unwrap_or_else(|| "leanstral-v1".into());
             let url = base_url.unwrap_or_else(|| "http://localhost:8000/v1".into());
-            Box::new(OpenAiCompatible::new(m, api_key, url).with_name("leanstral-local".into()))
+            Ok(Box::new(
+                OpenAiCompatible::new(m, api_key, url).with_name("leanstral-local".into()),
+            ))
         }
         "openai-compat" => {
-            let m = model.unwrap_or_else(|| {
-                eprintln!("openai-compat backend requires --model");
-                std::process::exit(1);
-            });
-            let url = base_url.unwrap_or_else(|| {
-                eprintln!("openai-compat backend requires --base-url");
-                std::process::exit(1);
-            });
-            Box::new(OpenAiCompatible::new(m, api_key, url).with_name("openai-compat".into()))
-        }
-        other => {
-            eprintln!("unknown backend: {other}");
-            eprintln!(
-                "available: claude, anthropic, openai, leanstral, leanstral-local, openai-compat"
-            );
-            std::process::exit(1);
+            let m = model.ok_or_else(|| "openai-compat backend requires --model".to_string())?;
+            let url =
+                base_url.ok_or_else(|| "openai-compat backend requires --base-url".to_string())?;
+            Ok(Box::new(
+                OpenAiCompatible::new(m, api_key, url).with_name("openai-compat".into()),
+            ))
         }
+        other => Err(format!(
+            "unknown backend: {other}\navailable: claude, anthropic, openai, leanstral, \
+             leanstral-local, openai-compat"
+        )),
     }
 }
 

crates/proof-pilot/src/journal.rs

@@ -5,6 +5,28 @@
 //! (P4 NOTES.md, P5 transcript replay) consume this type; it must remain
 //! serde-stable.
 
+/// One sampled candidate within a best-of-n iteration.
+///
+/// Recorded for every sample when `samples_per_iter > 1` so the transcript is a
+/// complete, deterministic record: `--replay` applies `source_after` states and
+/// never re-derives from responses, but an auditor must be able to see every
+/// candidate the kernel filtered and which one was accepted.
+#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)]
+pub struct CandidateRecord {
+    /// 0-based index in sampling order (the order responses were requested).
+    pub sample_index: u32,
+    /// Raw LLM response for this sample.
+    pub llm_response: String,
+    /// What happened to this candidate: `"accepted"`, `"build_failed"`,
+    /// `"patch_rejected"`, `"duplicate"` (identical patched source as an earlier
+    /// sample), `"not_tried"` (an earlier candidate was accepted first), or
+    /// `"request_failed"` (the backend call itself failed — `llm_response` is
+    /// empty and the error is in `build_output`).
+    pub status: String,
+    /// Build output for candidates that were built; empty otherwise.
+    pub build_output: String,
+}
+
 /// A single LLM iteration within a proof session.
 #[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)]
 pub struct IterationRecord {
@@ -16,7 +38,9 @@ pub struct IterationRecord {
     pub source_after: String,
     /// Full prompt sent to the LLM.
     pub prompt: String,
-    /// Raw text response from the LLM.
+    /// Raw text response from the LLM. Under best-of-n this is the response
+    /// whose patch ended the iteration (the accepted candidate, or the last
+    /// candidate tried when all failed) — consistent with `source_after`.
     pub llm_response: String,
     /// Build / LSP error text shown to the LLM for this iteration.
     pub build_errors: String,
@@ -26,6 +50,15 @@ pub struct IterationRecord {
     pub suggestions: Vec<String>,
     /// `true` if the patch was successfully applied; `false` if it was rejected.
     pub patch_applied: bool,
+    /// All sampled candidates, in sampling order. Empty when `samples_per_iter`
+    /// is 1 (the single response is already `llm_response`). `#[serde(default)]`
+    /// keeps pre-best-of-n transcripts loadable unchanged.
+    #[serde(default)]
+    pub candidates: Vec<CandidateRecord>,
+    /// `sample_index` of the accepted candidate, when one was accepted under
+    /// best-of-n sampling.
+    #[serde(default)]
+    pub accepted_sample: Option<u32>,
 }
 
 /// Complete record of one proof completion session.

crates/proof-pilot/src/main.rs

@@ -55,6 +55,7 @@ fn main() {
     let mut verify = false;
     let mut allow_toolchain_mismatch = false;
     let mut use_lsp = false;
+    let mut samples_per_iter = 1u32;
     let mut backend_name = String::from("claude");
     let mut api_key: Option<String> = None;
     let mut base_url: Option<String> = None;
@@ -107,6 +108,16 @@ fn main() {
             "--lsp" => {
                 use_lsp = true;
             }
+            "--samples-per-iter" => {
+                samples_per_iter = flag_value(&args, &mut i, "--samples-per-iter")
+                    .parse()
+                    .ok()
+                    .filter(|&n| n >= 1)
+                    .unwrap_or_else(|| {
+                        eprintln!("invalid --samples-per-iter value (must be >= 1)");
+                        std::process::exit(1);
+                    });
+            }
             "--backend" => {
                 backend_name = flag_value(&args, &mut i, "--backend");
             }
@@ -172,7 +183,10 @@ fn main() {
     });
 
     // Construct backend
-    let backend = make_backend(&backend_name, model, api_key, base_url);
+    let backend = make_backend(&backend_name, model, api_key, base_url).unwrap_or_else(|e| {
+        eprintln!("error: {e}");
+        std::process::exit(1);
+    });
 
     eprintln!("[proof-pilot] backend: {}", backend.name());
 
@@ -183,6 +197,7 @@ fn main() {
         system_prompt,
         transcript: transcript_path,
         use_lsp,
+        samples_per_iter,
     };
 
     let (result, journal) = session::run(&config, backend.as_ref());

crates/proof-pilot/src/notes.rs

@@ -422,6 +422,8 @@ mod tests {
             goal_states: goals.iter().map(|s| s.to_string()).collect(),
             suggestions: suggestions.iter().map(|s| s.to_string()).collect(),
             patch_applied: applied,
+            candidates: Vec::new(),
+            accepted_sample: None,
         }
     }