From a3e77130cfac4a3b7dd62e36e5dba0b76f4a7752 Mon Sep 17 00:00:00 2001
From: Levi Neuwirth <ln@levineuwirth.org>
Date: Thu, 21 May 2026 15:58:07 -0400
Subject: [PATCH] Phase 3 Rocq parity M3: bridge-aware LLM adapter +
 reconstruction fallback
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Rocq mirror of Lean PR #36 (LLM-assisted Tier-3 reconstruction
fallback), plus the load-bearing prerequisite that makes the
fallback actually work cross-bridge: the SDK's `Adapter_llm` and
`Llm_reconstruct` now produce bridge-appropriate prompts /
trace_formats based on `ir.source_system.name`.

**Bridge-aware SDK** (`sdk/lib/adapter_llm.ml`, `llm_reconstruct.ml`):
- New `rocq_ty` / `rocq_term` / `rocq_paren` parallel to the
  existing Lean rendering helpers — translate IR's bridge-agnostic
  type-ref vocabulary (Int / Real / Prop + arrow chains) to Rocq
  Stdlib syntax (Z / R / Prop with ASCII `->`), and render
  shell_terms with Rocq's `/\` `\/` `~` connectives, `forall (x :
  T), body` quantifiers, ASCII Z-scope arithmetic.
- New `dialect` record bundles per-bridge state (system_prompt,
  render_prompt, ty, term, trace_format, cert_format, annotation).
  `dialect_of_ir` dispatches on `ir.source_system.name`: "rocq" →
  `rocq_dialect`, everything else → `lean_dialect` (safer
  LLM-familiar default).
- `Adapter_llm.dispatch` and `Llm_reconstruct.translate` both pick
  the dialect upfront — Rocq home systems get Rocq-flavored
  prompts asking for Ltac in a fenced ```coq block; minted certs
  carry `format = trace_format = "rocq-tactic-script"`.
- `Verifier.verify` extends its Tier-3 dispatch to recognize both
  `lean-tactic-script` and `rocq-tactic-script` → both return
  `Tier3_replay_deferred { trace_format }` (envelope-only;
  soundness deferred to the home kernel's audit-H1 replay gate).

**Closers tightened** (M3.b): Rocq's `close_or_fail` now matches
`Tier3_replay_deferred { trace_format = "rocq-tactic-script" }`
specifically. A `lean-tactic-script` cert reaching the Rocq closer
(misconfigured manifest pointing this bridge at a Lean-flavored
LLM endpoint, or future bug) is a clean user error rather than a
silent parse failure when Ltac tries to chew on Lean syntax.

**Reconstruction fallback** (M3.c, `rocq-bridge/src/pb_rocq_main.ml`):
Mirror of Lean's `closeOrFailPrimary` + `closeOrFail` wrap.
- The existing `close_or_fail` is renamed `close_or_fail_primary`.
- New `replay_reconstructed_script trace_format script` runs the
  candidate through `Llm_replay.replay_script` (the same audit-H1
  gate from M2) and on success emits a `Feedback.msg_info` line
  naming the source trace format — audit trail visible in build
  output.
- New `try_llm_reconstruct ir cert?` gates on Tier-3 cert with
  `trace_format ≠ rocq-tactic-script`, calls
  `Proof_broker.Llm_reconstruct.translate` (direct-linked, no FFI),
  returns `Some fallback_tac` or `None`.
- New `close_or_fail` wraps primary in `Proofview.tclORELSE`; on
  primary failure invokes `try_llm_reconstruct` lazily (HTTP only
  fires when primary actually fails) and routes to the fallback
  if a script came back, else re-raises the primary error.
- Audit H1: reconstruction goes through the SAME audit gate as
  primary LLM-replay (kernel replay + axiom-footprint subset
  check), so the LLM never widens the trust base.

**Test-only tactic** (`g_proof_broker.mlg`): new `llm_reconstruct_test
"<format>" "<script>"` drives `replay_reconstructed_script`
directly with a string literal — exercises the audit-H1 contract
without a live LLM endpoint. Mirror of Lean's evalLlmReconstructTest.

**Tests** (Rocq-side mirror of Lean's `llm_reconstruct_test` block):
- Positive `pb_llm_reconstruct_axiom_free`: clean `intros;
  reflexivity` translation closes a Z-equality goal. Allowlisted
  `[]`.
- Negative `assert_fails (llm_reconstruct_test ... "idtac")` —
  non-closing translation.
- Negative `assert_fails (llm_reconstruct_test ... "@@@ ...")` —
  parse failure.

**SDK tests** added bridge-aware coverage: Rocq-flavored
`test_prompt_render_rocq` and `test_mock_endpoint_rocq` for
`Adapter_llm`; `test_prompt_render_rocq` for `Llm_reconstruct`.
Verifies Z translation, Theorem...Proof...Qed scaffold, ```coq
fence, and that the Rocq-flavored cert's verify reason carries
`trace_format = "rocq-tactic-script"`.

Locally verified: SDK + Rocq plugin sources build clean (`dune
build sdk rocq-bridge/src` rc=0). Full SDK suite passes including
the new Rocq tests. Python schema/gate suite green. JSON
allowlist valid. The Rocq theory build path (incl. the new
fallback test and Print Assumptions on `pb_llm_reconstruct_axiom_free`)
needs CI per the same broken-local-rocq-env caveat from M1/M2.

With this, Phase 3 Rocq parity is structurally complete for
deliverables #3 and #4. M4 (polish) carries the
`fragment_of_logic` consolidation (Phase-4 retro carry) plus a
README/delta sync to record the Rocq Phase-3 surface.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 rocq-bridge/src/g_proof_broker.mlg |  20 +++
 rocq-bridge/src/pb_rocq_main.ml    |  93 +++++++++++-
 rocq-bridge/src/pb_rocq_main.mli   |  10 ++
 rocq-bridge/theories/Test.v        |  46 ++++++
 sdk/lib/adapter_llm.ml             | 225 ++++++++++++++++++++++++++---
 sdk/lib/llm_reconstruct.ml         |  58 +++++---
 sdk/lib/verifier.ml                |  31 ++--
 sdk/test/test_adapter_llm.ml       | 102 ++++++++++++-
 sdk/test/test_llm_reconstruct.ml   |  42 +++++-
 tools/axiom_allowlist.json         |   2 +
 10 files changed, 573 insertions(+), 56 deletions(-)

diff --git a/rocq-bridge/src/g_proof_broker.mlg b/rocq-bridge/src/g_proof_broker.mlg
index 011479c..09609e2 100644
--- a/rocq-bridge/src/g_proof_broker.mlg
+++ b/rocq-bridge/src/g_proof_broker.mlg
@@ -58,3 +58,23 @@ END
 TACTIC EXTEND ProofBrokerLlmReplayTest
 | [ "llm_replay_test" string(s) ] -> { Llm_replay.replay_script s }
 END
+
+(* TEST-ONLY tactic for the LLM-assisted Tier-3 reconstruction
+   fallback (roadmap §Phase 3 #4, Rocq parity M3). The live SDK
+   path ([Llm_reconstruct.translate]) only runs when an endpoint
+   is configured — for CI we skip the translation call and feed
+   the candidate script directly into the {e same} closer the
+   production path invokes after a successful translation
+   ([Pb_rocq_main.replay_reconstructed_script]). This pins the
+   integration: a translated script flows through
+   [Llm_replay.replay_script] (kernel replay + axiom-footprint
+   gate), the same audit-H1 contract [llm_replay_test] exercises
+   for primary LLM certs. First argument is the trace format of
+   the (notionally un-replayable) source cert — surfaces in the
+   audit feedback line. Mirror of [llm_reconstruct_test] in
+   lean-bridge/Test/Tactic.lean. *)
+TACTIC EXTEND ProofBrokerLlmReconstructTest
+| [ "llm_reconstruct_test" string(fmt) string(s) ] -> {
+    Pb_rocq_main.replay_reconstructed_script fmt s
+  }
+END
diff --git a/rocq-bridge/src/pb_rocq_main.ml b/rocq-bridge/src/pb_rocq_main.ml
index dea62a8..c7c9660 100644
--- a/rocq-bridge/src/pb_rocq_main.ml
+++ b/rocq-bridge/src/pb_rocq_main.ml
@@ -211,7 +211,13 @@ let closer_for_fragment fragment : unit Proofview.tactic =
               cert-gated closer in the core plugin)"
              other))
 
-let close_or_fail (p : path) : unit Proofview.tactic =
+(* Primary closer chain: fragment-keyed dispatch for verified
+   reasons, plus the LLM-replay arm for [rocq-tactic-script]
+   certs. Renamed from [close_or_fail] in M3.c — the public
+   [close_or_fail] (below) is now a wrapper that catches a
+   primary failure and tries LLM-assisted Tier-3 reconstruction
+   before re-raising the error. *)
+let close_or_fail_primary (p : path) : unit Proofview.tactic =
   match p.cert, p.verify_reason with
   | None, _ ->
     CErrors.user_err Pp.(
@@ -229,7 +235,13 @@ let close_or_fail (p : path) : unit Proofview.tactic =
         Rocq Stdlib allowlist. Audit H1: a hallucinated [admit]
         or [Axiom Foo] is a tactic failure, never an admitted
         theorem. *)
-     | Tier3_replay_deferred _ ->
+     | Tier3_replay_deferred { trace_format = "rocq-tactic-script" } ->
+       (* M3.b: tightened to only accept the Rocq-flavored cert.
+          A [lean-tactic-script] cert reaching the Rocq closer is
+          a configuration error (LLM adapter saw this bridge as
+          Lean-flavored), not a tactic-soundness issue — surface
+          it as a clear user error rather than silently trying to
+          parse Lean tactics as Ltac. *)
        (match cert.payload with
         | Tier3_proof_trace { trace_data = `String script; _ } ->
           Llm_replay.replay_script script
@@ -237,6 +249,16 @@ let close_or_fail (p : path) : unit Proofview.tactic =
           CErrors.user_err Pp.(
             str "proof_broker: Tier-3 replay-deferred cert payload \
                  is not a string trace; cannot replay"))
+     | Tier3_replay_deferred { trace_format } ->
+       CErrors.user_err Pp.(
+         str (Printf.sprintf
+                "proof_broker: LLM cert has trace_format=%S but the \
+                 Rocq home-system replayer only accepts \
+                 'rocq-tactic-script'. The LLM adapter likely saw \
+                 this IR as a Lean source_system; ensure the Rocq \
+                 reifier sets ir.source_system.name = \"rocq\" so \
+                 [Adapter_llm.dialect_of_ir] picks the Rocq dialect."
+                trace_format))
      | Verified_envelope | Verified_farkas
      | Verified_case_split | Verified_tier3
      (* Verified_tier3_provenance gates the home-system closer
@@ -270,6 +292,73 @@ let close_or_fail (p : path) : unit Proofview.tactic =
     CErrors.user_err Pp.(
       str "proof_broker: internal — cert present but verify outcome missing")
 
+(* --- M3.c: LLM-assisted Tier-3 reconstruction fallback ----------- *)
+
+(* Run [Llm_replay.replay_script] on a candidate the LLM produced
+   via reconstruction (rather than the primary LLM-as-backend
+   path). On success, emit a [Feedback.msg_info] line naming the
+   source trace format so the audit trail of how the goal closed
+   is visible in the build output. Mirror of Lean's
+   [replayReconstructedScript]. *)
+let replay_reconstructed_script (trace_format : string)
+    (script : string) : unit Proofview.tactic =
+  let announce =
+    Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
+      Feedback.msg_info (Pp.str (Printf.sprintf
+        "proof_broker: closed via LLM Tier-3 reconstruction \
+         (%s trace → Rocq Ltac script, kernel-checked, audit H1)."
+        trace_format))))
+  in
+  Proofview.tclBIND (Llm_replay.replay_script script) (fun () -> announce)
+
+(* Decide whether to invoke LLM-assisted reconstruction on the
+   current cert + return a fallback tactic if so. Gates (no-op
+   unless all hold):
+   * a cert is in hand,
+   * tier is 3 with a [Tier3_proof_trace] payload,
+   * [trace_format] is not already [rocq-tactic-script] (which the
+     primary LLM-replay arm at the top of [close_or_fail_primary]
+     handles),
+   * the SDK's [Llm_reconstruct.translate] returns a non-empty
+     script (so this is silent when no endpoint is configured —
+     the primary failure is re-raised).
+
+   The translate call runs immediately when this function is
+   invoked; callers should only invoke it from the [tclORELSE]
+   handler so the HTTP request is lazy (fires only on primary
+   failure). *)
+let try_llm_reconstruct (ir : Ir.t) (cert_opt : Cert.t option)
+  : unit Proofview.tactic option =
+  match cert_opt with
+  | None -> None
+  | Some (cert : Cert.t) ->
+    if cert.tier <> 3 then None
+    else match cert.payload with
+    | Tier3_proof_trace { trace_format = "rocq-tactic-script"; _ } ->
+      None
+    | Tier3_proof_trace { trace_format; _ } ->
+      (match Proof_broker.Llm_reconstruct.translate ir cert with
+       | Error _ -> None
+       | Ok script ->
+         Some (replay_reconstructed_script trace_format script))
+    | _ -> None
+
+(* Public closer: try the primary fragment-keyed chain; on any
+   failure, try LLM-assisted Tier-3 reconstruction before
+   re-raising the primary error. Mirror of Lean's [closeOrFail]
+   try/catch wrap. Audit H1: the reconstruction path goes
+   through the SAME audit gate [replay_reconstructed_script] →
+   [Llm_replay.replay_script] uses for primary
+   [rocq-tactic-script] certs — kernel replay + axiom-footprint
+   subset check — so the LLM never widens the trust base. *)
+let close_or_fail (p : path) : unit Proofview.tactic =
+  Proofview.tclORELSE
+    (close_or_fail_primary p)
+    (fun (primary_exn, primary_info) ->
+      match try_llm_reconstruct p.ir p.cert with
+      | None -> Proofview.tclZERO ~info:primary_info primary_exn
+      | Some fallback -> fallback)
+
 (* --- public entry points ------------------------------------------- *)
 
 let run_close (names : Names.Id.t list option) : unit Proofview.tactic =
diff --git a/rocq-bridge/src/pb_rocq_main.mli b/rocq-bridge/src/pb_rocq_main.mli
index 79303ea..ffc1869 100644
--- a/rocq-bridge/src/pb_rocq_main.mli
+++ b/rocq-bridge/src/pb_rocq_main.mli
@@ -38,3 +38,13 @@ val run_close_term : Names.Id.t list option -> unit Proofview.tactic
     arity > 2, non-Le hypotheses, etc.) — the user explicitly
     opted into term mode by typing [proof_broker_term] over
     plain [proof_broker]. *)
+
+val replay_reconstructed_script :
+  string -> string -> unit Proofview.tactic
+(** [replay_reconstructed_script trace_format script] feeds the
+    LLM-translated script through [Llm_replay.replay_script]
+    (the audit-H1 gate) and, on success, emits a
+    [Feedback.msg_info] line naming the source trace format so
+    the audit trail is visible in build output. Exported for the
+    test-only [llm_reconstruct_test] tactic to drive the
+    reconstruction-side closer without a live LLM endpoint. *)
diff --git a/rocq-bridge/theories/Test.v b/rocq-bridge/theories/Test.v
index 2c25cd4..09fe76f 100644
--- a/rocq-bridge/theories/Test.v
+++ b/rocq-bridge/theories/Test.v
@@ -703,3 +703,49 @@ Proof.
   assert_fails (llm_replay_test "@@@ not lean @@@").
   exact I.
 Qed.
+
+(* ============================================================
+   LLM-assisted Tier-3 reconstruction fallback
+   (roadmap §Phase 3 deliverable 4, Rocq parity M3).
+
+   [llm_reconstruct_test "<traceFmt>" "<script>"] simulates a
+   successful [Llm_reconstruct.translate] call (the LLM was
+   asked to translate an un-replayable Tier-3 trace and
+   returned the script) and routes the candidate through the
+   SAME audit-H1 gate the production fallback uses. The
+   translation step itself is a pure I/O wrapper around an
+   untrusted oracle — no soundness contribution — so swapping
+   the live SDK call for a literal script is faithful to what's
+   being tested: that a candidate script makes it through
+   [replay_reconstructed_script] → [Llm_replay.replay_script],
+   with the audit-H1 gate firing identically. Mirror of the
+   llm_reconstruct_test block in lean-bridge/Test/Tactic.lean. *)
+
+(* Positive: a translated script the kernel independently
+   accepts (axiom-free [intros; reflexivity]) closes the goal
+   via the reconstruction fallback's replay closer. The build
+   log carries the "closed via LLM Tier-3 reconstruction …"
+   audit line. *)
+Theorem pb_llm_reconstruct_axiom_free : forall x : Z, x = x.
+Proof.
+  llm_reconstruct_test "alethe-2024" "intros x; reflexivity".
+Qed.
+
+Print pb_llm_reconstruct_axiom_free.
+Print Assumptions pb_llm_reconstruct_axiom_free.
+
+(* Negative: a translation that runs without error but does not
+   close the goal is a tactic failure, never a silent pass. *)
+Example pb_llm_reconstruct_rejects_non_closing : True.
+Proof.
+  assert_fails (llm_reconstruct_test "alethe-2024" "idtac").
+  exact I.
+Qed.
+
+(* Negative: a translation that does not parse as Rocq Ltac is
+   a tactic failure, not an admitted theorem. *)
+Example pb_llm_reconstruct_rejects_unparsable : True.
+Proof.
+  assert_fails (llm_reconstruct_test "tstp-fof" "@@@ not lean @@@").
+  exact I.
+Qed.
diff --git a/sdk/lib/adapter_llm.ml b/sdk/lib/adapter_llm.ml
index e2afb44..6b6ab99 100644
--- a/sdk/lib/adapter_llm.ml
+++ b/sdk/lib/adapter_llm.ml
@@ -42,7 +42,18 @@ let default_timeout_ms = 30_000
 let timeout_of_ir (ir : Ir.t) : int =
   Adapter.resolve_timeout_ms ~default_ms:default_timeout_ms ir
 
-(* --- IR → Lean surface syntax ---------------------------------------- *)
+(* --- IR → bridge surface syntax -------------------------------------- *)
+
+(** The IR's type-ref vocabulary is bridge-agnostic ([Int]/[Real]/
+    [Prop] + arrow chains). Each home bridge needs the *prompt*
+    rendered in its own surface syntax — Lean asks for Lean
+    tactics, Rocq asks for Ltac — so the rendering layer splits
+    here. The discriminator is [ir.source_system.name]; see
+    [dispatch] for the call site. Sym-and-IR translation logic
+    that doesn't depend on the surface syntax (e.g.
+    [strip_uf], [extract_script], [curl_post]) stays shared. *)
+
+(** {2 Lean dialect (Lean 4)} *)
 
 (** Render an IR type-ref as Lean (the IR uses [->] for arrows;
     Lean reads [→], and the parenthesization the reifier emits is
@@ -121,10 +132,96 @@ and paren (t : Ir.shell_term) : string =
   | Var _ | Const _ | Num_lit _ -> lean_term t
   | _ -> lean_term t  (* lean_term already parenthesizes compounds *)
 
-(** The theorem statement + an instruction, as the user prompt.
-    Free vars and hypotheses become binders; the goal is the
-    conclusion. *)
-let render_prompt (ir : Ir.t) : string =
+(** {2 Rocq dialect (Coq / Rocq Stdlib)} *)
+
+(** Render an IR type-ref as Rocq Stdlib syntax. The IR's
+    bridge-agnostic vocabulary ([Int] / [Real] / [Prop]) is mapped
+    to Rocq's [Z] / [R] / [Prop]; arrow chains stay structural
+    (Rocq writes them with ASCII [->], matching the IR's own
+    encoding). Parenthesization the reifier emits is preserved
+    verbatim. *)
+let rocq_ty (t : Ir.type_ref) : string =
+  (* Build out with one pass: substitute the bridge-agnostic
+     type names for their Rocq Stdlib equivalents. The IR's
+     [parse_arrow_type] convention keeps everything else
+     character-by-character. *)
+  let n = String.length t in
+  let b = Buffer.create n in
+  let i = ref 0 in
+  while !i < n do
+    let c = t.[!i] in
+    if c = 'I' && !i + 3 <= n && String.sub t !i 3 = "Int" then begin
+      Buffer.add_char b 'Z'; i := !i + 3
+    end else if c = 'R' && !i + 4 <= n && String.sub t !i 4 = "Real" then begin
+      Buffer.add_char b 'R'; i := !i + 4
+    end else begin
+      Buffer.add_char b c; incr i
+    end
+  done;
+  Buffer.contents b
+
+(** Infix Rocq operator for the recognized arithmetic/relational
+    shell symbols. Assumes [Z_scope] (or [R_scope]) is open in
+    the proof context — the prompt's [Open Scope Z_scope.]
+    instruction sets that up. *)
+let rocq_infix_of = function
+  | "HAdd.hAdd" | "Int.add" | "Add.add" | "+" -> Some "+"
+  | "HSub.hSub" | "Int.sub" | "Sub.sub" | "-" -> Some "-"
+  | "HMul.hMul" | "Int.mul" | "Mul.mul" | "*" -> Some "*"
+  | "LE.le" | "<=" -> Some "<="
+  | "LT.lt" | "<" -> Some "<"
+  | "GE.ge" | ">=" -> Some ">="
+  | "GT.gt" | ">" -> Some ">"
+  | _ -> None
+
+let rec rocq_term (t : Ir.shell_term) : string =
+  match t with
+  | Var { name } -> name
+  | Const { name = "True" } -> "True"
+  | Const { name = "False" } -> "False"
+  | Const { name } -> name
+  | Num_lit { value; _ } -> value
+  | Not { operand } -> "~ " ^ rocq_paren operand
+  | And { left; right } ->
+    Printf.sprintf "(%s /\\ %s)" (rocq_term left) (rocq_term right)
+  | Or { left; right } ->
+    Printf.sprintf "(%s \\/ %s)" (rocq_term left) (rocq_term right)
+  | Implies { antecedent; consequent } ->
+    Printf.sprintf "(%s -> %s)" (rocq_term antecedent) (rocq_term consequent)
+  | Eq { left; right; _ } ->
+    Printf.sprintf "(%s = %s)" (rocq_term left) (rocq_term right)
+  | Forall { var; ty; body } ->
+    Printf.sprintf "(forall %s : %s, %s)" var (rocq_ty ty) (rocq_term body)
+  | Exists { var; ty; body } ->
+    Printf.sprintf "(exists %s : %s, %s)" var (rocq_ty ty) (rocq_term body)
+  | Lambda { binders; body } ->
+    let bs =
+      String.concat " "
+        (List.map
+           (fun (b : Ir.binder) ->
+              Printf.sprintf "(%s : %s)" b.var (rocq_ty b.ty))
+           binders)
+    in
+    Printf.sprintf "(fun %s => %s)" bs (rocq_term body)
+  | App { symbol; args; _ } ->
+    let sym = strip_uf symbol in
+    (match rocq_infix_of symbol, args with
+     | Some op, [ a; b ] ->
+       Printf.sprintf "(%s %s %s)" (rocq_term a) op (rocq_term b)
+     | _, [] -> sym
+     | _, _ ->
+       Printf.sprintf "(%s %s)" sym
+         (String.concat " " (List.map rocq_paren args)))
+  | Opaque { payload_id } -> "(_ (* opaque:" ^ payload_id ^ " *))"
+
+and rocq_paren (t : Ir.shell_term) : string =
+  match t with
+  | Var _ | Const _ | Num_lit _ -> rocq_term t
+  | _ -> rocq_term t  (* rocq_term already parenthesizes compounds *)
+
+(** The theorem statement + an instruction, as the user prompt
+    rendered for the Lean home system. *)
+let render_prompt_lean (ir : Ir.t) : string =
   let fv =
     List.map
       (fun (v : Ir.free_var) ->
@@ -145,13 +242,103 @@ let render_prompt (ir : Ir.t) : string =
      theorem goal %s : %s := by\n  -- your tactics here\n"
     binders goal
 
-(* --- request body ---------------------------------------------------- *)
+(** The theorem statement + an instruction, as the user prompt
+    rendered for the Rocq home system. Asks for Ltac in a fenced
+    ```coq block; binders are introduced into the proof context
+    by Rocq's section-style theorem header, so the LLM's tactics
+    can refer to free vars / hypotheses by name without needing
+    to [intros] them. *)
+let render_prompt_rocq (ir : Ir.t) : string =
+  let fv =
+    List.map
+      (fun (v : Ir.free_var) ->
+         Printf.sprintf "(%s : %s)" v.name (rocq_ty v.ty))
+      ir.context.free_vars
+  in
+  let hyps =
+    List.map
+      (fun (h : Ir.hypothesis) ->
+         Printf.sprintf "(%s : %s)" h.name (rocq_term h.shell))
+      ir.context.hypotheses
+  in
+  let binders = String.concat " " (fv @ hyps) in
+  let goal = rocq_term ir.goal.shell in
+  Printf.sprintf
+    "Prove this Rocq theorem (assume [From Stdlib Require Import ZArith.] \
+     and [Open Scope Z_scope.] are in effect). Reply with ONLY a fenced \
+     ```coq code block containing an Ltac proof script (the lines between \
+     `Proof.` and `Qed.`, exclusive), no prose.\n\n\
+     Theorem goal %s : %s.\n\
+     Proof.\n  (* your tactics here *)\nQed.\n"
+    binders goal
 
-let system_prompt =
-  "You are a Lean 4 proof assistant. Output only a Lean 4 tactic \
-   script inside a single ```lean fenced block. No explanations."
+(* --- dialect bundle --------------------------------------------------- *)
+
+(** Per-bridge configuration: prompt template, [trace_format]
+    label for the minted cert, and the [system_prompt] role
+    message. [Adapter_llm.dispatch] and [Llm_reconstruct.translate]
+    both branch on [ir.source_system.name] via [dialect_of_ir] to
+    pick the right bundle. *)
+type dialect = {
+  system_prompt : string;
+  render_prompt : Ir.t -> string;
+  ty : Ir.type_ref -> string;
+  term : Ir.shell_term -> string;
+  trace_format : string;
+  cert_format : string;
+  annotation : string;
+}
+
+let lean_dialect : dialect = {
+  system_prompt =
+    "You are a Lean 4 proof assistant. Output only a Lean 4 tactic \
+     script inside a single ```lean fenced block. No explanations.";
+  render_prompt = render_prompt_lean;
+  ty = lean_ty;
+  term = lean_term;
+  trace_format = "lean-tactic-script";
+  cert_format = "lean-tactic-script";
+  annotation =
+    "LLM-suggested Lean tactic script. NOT verified by the broker — \
+     soundness rests entirely on the home system replaying it through \
+     its kernel (audit H1); a failed replay is a tactic failure, never \
+     an axiom.";
+}
 
-let build_body ~model ~(prompt : string) : string =
+let rocq_dialect : dialect = {
+  system_prompt =
+    "You are a Rocq (Coq) proof assistant. Output only an Ltac proof \
+     script inside a single ```coq fenced block. No explanations.";
+  render_prompt = render_prompt_rocq;
+  ty = rocq_ty;
+  term = rocq_term;
+  trace_format = "rocq-tactic-script";
+  cert_format = "rocq-tactic-script";
+  annotation =
+    "LLM-suggested Rocq Ltac script. NOT verified by the broker — \
+     soundness rests entirely on the home system replaying it through \
+     its kernel (audit H1); a failed replay is a tactic failure, never \
+     an axiom.";
+}
+
+(** Pick the dialect for an IR. Defaults to the Lean dialect for
+    any [source_system.name] other than ["rocq"] — the IR's
+    source_system field is bridge-supplied, so an unrecognized
+    value here means a bridge we haven't taught the LLM about
+    yet, and Lean is the safer (more LLM-familiar) default. *)
+let dialect_of_ir (ir : Ir.t) : dialect =
+  match ir.source_system.name with
+  | "rocq" -> rocq_dialect
+  | _ -> lean_dialect
+
+(** Back-compat alias for callers that want the Lean rendering
+    without going through [dialect_of_ir]. *)
+let render_prompt (ir : Ir.t) : string =
+  (dialect_of_ir ir).render_prompt ir
+
+(* --- request body ---------------------------------------------------- *)
+
+let build_body ~model ~system_prompt ~(prompt : string) : string =
   Yojson.Safe.to_string
     (`Assoc [
        "model", `String model;
@@ -256,6 +443,7 @@ let extract_script (content : string) : string =
 (* --- cert minting ---------------------------------------------------- *)
 
 let mk_cert ~(ir : Ir.t) ~model ~script ~timeout_ms : Certificate.t =
+  let dialect = dialect_of_ir ir in
   let fragment =
     let f = ir.logic_classification.first_order_fragment in
     if f = "" then "none" else f
@@ -263,7 +451,7 @@ let mk_cert ~(ir : Ir.t) ~model ~script ~timeout_ms : Certificate.t =
   {
     cert_version = "1.0";
     tier = 3;
-    format = "lean-tactic-script";
+    format = dialect.cert_format;
     goal = ir.goal;
     dispatch_context_hash = Hash.sha256_of_json (Codec.to_json ir);
     rewrite_trace_hash = "sha256:" ^ String.make 64 '0';
@@ -284,15 +472,11 @@ let mk_cert ~(ir : Ir.t) ~model ~script ~timeout_ms : Certificate.t =
       auxiliary = Some (`Assoc [ "model", `String model ]);
     };
     payload = Tier3_proof_trace {
-      trace_format = "lean-tactic-script";
+      trace_format = dialect.trace_format;
       trace_data = `String script;
       trace_dialect_features =
         Some [ "llm_generated"; "unverified_until_kernel_replay" ];
-      trace_annotations =
-        Some "LLM-suggested Lean tactic script. NOT verified by the \
-              broker — soundness rests entirely on the home system \
-              replaying it through its kernel (audit H1); a failed \
-              replay is a tactic failure, never an axiom.";
+      trace_annotations = Some dialect.annotation;
     };
   }
 
@@ -316,8 +500,11 @@ let dispatch (ir : Ir.t) : Adapter.result =
         ~default:"default"
     in
     let timeout_ms = timeout_of_ir ir in
-    let prompt = render_prompt ir in
-    let body = build_body ~model ~prompt in
+    let dialect = dialect_of_ir ir in
+    let prompt = dialect.render_prompt ir in
+    let body =
+      build_body ~model ~system_prompt:dialect.system_prompt ~prompt
+    in
     (try
        let stdout, stderr, code =
          curl_post ~timeout_ms ~url ~api_key ~body
diff --git a/sdk/lib/llm_reconstruct.ml b/sdk/lib/llm_reconstruct.ml
index d13b70c..d3c38b6 100644
--- a/sdk/lib/llm_reconstruct.ml
+++ b/sdk/lib/llm_reconstruct.ml
@@ -32,11 +32,13 @@
 
 let default_timeout_ms = Adapter_llm.default_timeout_ms
 
-(** Build the user prompt: the goal as a Lean [theorem ... := by]
-    skeleton (same shape [Adapter_llm.render_prompt] uses for the
-    primary path), followed by the original trace as a hint with
-    its declared format. Free vars and hypotheses become binders;
-    the conclusion is the goal. *)
+(** Build the user prompt: the goal as a theorem skeleton in the
+    home bridge's surface syntax (Lean / Rocq), followed by the
+    original trace as a hint with its declared format. Free vars
+    and hypotheses become binders; the conclusion is the goal.
+    Uses the same [Adapter_llm.dialect_of_ir] dispatch as the
+    primary LLM adapter, so Lean home systems get a Lean-flavored
+    prompt and Rocq home systems get a Rocq-flavored one. *)
 let render_prompt (ir : Ir.t) (cert : Certificate.t) : string =
   let trace_format, trace_data =
     match cert.payload with
@@ -48,33 +50,47 @@ let render_prompt (ir : Ir.t) (cert : Certificate.t) : string =
          Tier3_proof_trace (reconstruction only applies to Tier-3 \
          certificates that carry a proof trace)"
   in
+  let dialect = Adapter_llm.dialect_of_ir ir in
   let fv =
     List.map
       (fun (v : Ir.free_var) ->
-         Printf.sprintf "(%s : %s)" v.name (Adapter_llm.lean_ty v.ty))
+         Printf.sprintf "(%s : %s)" v.name (dialect.ty v.ty))
       ir.context.free_vars
   in
   let hyps =
     List.map
       (fun (h : Ir.hypothesis) ->
-         Printf.sprintf "(%s : %s)"
-           h.name (Adapter_llm.lean_term h.shell))
+         Printf.sprintf "(%s : %s)" h.name (dialect.term h.shell))
       ir.context.hypotheses
   in
   let binders = String.concat " " (fv @ hyps) in
-  let goal = Adapter_llm.lean_term ir.goal.shell in
+  let goal = dialect.term ir.goal.shell in
   let trace_str = Yojson.Safe.to_string trace_data in
+  let is_rocq = (ir.source_system.name = "rocq") in
+  let fence, theorem_skeleton =
+    if is_rocq then
+      "coq",
+      Printf.sprintf
+        "Theorem goal %s : %s.\nProof.\n  (* your tactics here *)\nQed.\n"
+        binders goal
+    else
+      "lean",
+      Printf.sprintf
+        "theorem goal %s : %s := by\n  -- your tactics here\n"
+        binders goal
+  in
   Printf.sprintf
-    "A theorem prover produced a `%s` proof trace for the Lean 4 \
-     theorem below, but the home system has no symbolic replayer \
-     for that trace format. Use the trace as a hint and reply with \
-     ONLY a fenced ```lean code block containing a Lean 4 tactic \
-     proof (the `by` block body), no prose. A wrong or sorry-laden \
-     script will be rejected by the home system's kernel-and-axiom \
-     gate; the goal is left open in that case.\n\n\
-     theorem goal %s : %s := by\n  -- your tactics here\n\n\
+    "A theorem prover produced a `%s` proof trace for the theorem \
+     below, but the home system has no symbolic replayer for that \
+     trace format. Use the trace as a hint and reply with ONLY a \
+     fenced ```%s code block containing the tactic proof body, no \
+     prose. A wrong or sorry-laden / admit-laden script will be \
+     rejected by the home system's kernel-and-axiom gate; the goal \
+     is left open in that case.\n\n\
+     %s\n\
      --- begin %s trace ---\n%s\n--- end %s trace ---\n"
-    trace_format binders goal trace_format trace_str trace_format
+    trace_format fence theorem_skeleton
+    trace_format trace_str trace_format
 
 (** Translate [cert]'s trace into a candidate Lean tactic script
     by prompting the configured LLM. Returns the script on
@@ -104,8 +120,12 @@ let translate (ir : Ir.t) (cert : Certificate.t) : (string, string) result =
        ());
     (match cert.payload with
      | Tier3_proof_trace _ ->
+       let dialect = Adapter_llm.dialect_of_ir ir in
        let prompt = render_prompt ir cert in
-       let body = Adapter_llm.build_body ~model ~prompt in
+       let body =
+         Adapter_llm.build_body ~model
+           ~system_prompt:dialect.system_prompt ~prompt
+       in
        (try
           let stdout, stderr, code =
             Adapter_llm.curl_post ~timeout_ms ~url ~api_key ~body
diff --git a/sdk/lib/verifier.ml b/sdk/lib/verifier.ml
index d8dfecd..a1db6b7 100644
--- a/sdk/lib/verifier.ml
+++ b/sdk/lib/verifier.ml
@@ -85,13 +85,14 @@ type reason =
   | Tier3_unsupported_format of { trace_format : string }
   (** A Tier-3 trace whose format the broker recognizes but
       cannot soundness-check in OCaml because verification is the
-      home system's job — specifically [lean-tactic-script] from
-      the LLM adapter, which only Lean's kernel can re-check.
-      Envelope-verified (hashes / tier / dispatch context all
-      passed) but NOT a soundness verdict: the home-system replay
-      is the proof (audit H1). Distinct from
-      [Tier3_unsupported_format] (no replayer anywhere) and from
-      [Tier_check_deferred] (no tier verifier at all). *)
+      home system's job — specifically [lean-tactic-script] or
+      [rocq-tactic-script] from the LLM adapter, which only the
+      home system's kernel can re-check. Envelope-verified
+      (hashes / tier / dispatch context all passed) but NOT a
+      soundness verdict: the home-system replay is the proof
+      (audit H1). Distinct from [Tier3_unsupported_format] (no
+      replayer anywhere) and from [Tier_check_deferred] (no tier
+      verifier at all). *)
   | Tier3_replay_deferred of { trace_format : string }
   | Unsupported_witness_kind of { kind : string }
   | Tier_check_deferred of { tier : int }
@@ -515,11 +516,17 @@ let verify
      | Tier3_proof_trace { trace_format = ("tstp-fof" | "tstp-thf");
                            trace_data = `String proof_str; _ } ->
        reason_of_tier3_tptp (Tier3_tptp.verify ir proof_str)
-     | Tier3_proof_trace { trace_format = "lean-tactic-script"; _ } ->
-       (* Untrusted LLM oracle output: only Lean's kernel can
-          re-check it. Envelope passed; defer the proof to the
-          home-system replay (audit H1). *)
-       Tier3_replay_deferred { trace_format = "lean-tactic-script" }
+     | Tier3_proof_trace
+         { trace_format = ("lean-tactic-script" | "rocq-tactic-script")
+            as trace_format; _ } ->
+       (* Untrusted LLM oracle output: only the home system's
+          kernel can re-check it. Envelope passed; defer the proof
+          to the home-system replay (audit H1). The two formats
+          correspond to the two home bridges
+          [Adapter_llm.dialect_of_ir] dispatches on; both share
+          this verdict because the broker's role is identical for
+          either (envelope check + hand off). *)
+       Tier3_replay_deferred { trace_format }
      | Tier3_proof_trace { trace_format; _ } ->
        Tier3_unsupported_format { trace_format }
      | _ -> Tier_check_deferred { tier = cert.tier })
diff --git a/sdk/test/test_adapter_llm.ml b/sdk/test/test_adapter_llm.ml
index f148fbd..c60ccbb 100644
--- a/sdk/test/test_adapter_llm.ml
+++ b/sdk/test/test_adapter_llm.ml
@@ -56,6 +56,36 @@ let test_prompt_render () =
   Alcotest.(check bool) "asks for a fenced lean block" true
     (contains p "```lean")
 
+(* Rocq-flavored IR: same logical shape as [sample_ir] but with
+   [source_system.name = "rocq"] and an [Int] free var (which the
+   Rocq dialect renders as [Z]). Exercises the bridge-aware
+   dispatch in [Adapter_llm.dialect_of_ir]. *)
+let sample_ir_rocq () =
+  let ir = make_ir
+    ~free_vars:[ { name = "a"; ty = "Int" } ]
+    ~hypotheses:[
+      { name = "h1";
+        shell = App { symbol = "UF.p"; type_args = [];
+                      args = [ Var { name = "a" } ] } } ]
+    (App { symbol = "UF.p"; type_args = []; args = [ Var { name = "a" } ] })
+  in
+  { ir with source_system = { name = "rocq"; version = "0.0" } }
+
+let test_prompt_render_rocq () =
+  let p = Adapter_llm.render_prompt (sample_ir_rocq ()) in
+  Alcotest.(check bool) "translates Int → Z in binder type" true
+    (contains p "(a : Z)");
+  Alcotest.(check bool) "binds the hypothesis (Rocq Ltac form)" true
+    (contains p "(h1 : (p a))");
+  Alcotest.(check bool) "states the goal as a Rocq theorem (Theorem ... .)" true
+    (contains p "Theorem goal");
+  Alcotest.(check bool) "asks for a fenced coq block" true
+    (contains p "```coq");
+  Alcotest.(check bool) "does not leak Lean's by-block syntax" false
+    (contains p "```lean");
+  Alcotest.(check bool) "does not leak Lean's := by" false
+    (contains p ":= by")
+
 let test_extract_script_fenced () =
   Alcotest.(check string) "fenced lean block extracted" "subst h; simp"
     (Adapter_llm.extract_script
@@ -145,11 +175,75 @@ let test_mock_endpoint () =
        Alcotest.fail ("mock endpoint should yield a cert; got "
                       ^ Adapter.kind_of_failure f))
 
+(* Rocq mock endpoint: same forked one-shot responder pattern,
+   but the IR's source_system.name="rocq" so dispatch picks the
+   Rocq dialect — the minted cert's [format] and
+   [trace_format] should both be "rocq-tactic-script", and the
+   embedded script preserves the ```coq fence content. *)
+let mock_body_rocq =
+  {|{"choices":[{"message":{"content":"```coq\nintros; lia.\n```"}}]}|}
+
+let test_mock_endpoint_rocq () =
+  if not (curl_available ()) then Alcotest.skip ();
+  let sock = Unix.socket Unix.PF_INET Unix.SOCK_STREAM 0 in
+  Unix.setsockopt sock Unix.SO_REUSEADDR true;
+  Unix.bind sock (Unix.ADDR_INET (Unix.inet_addr_loopback, 0));
+  Unix.listen sock 1;
+  let port =
+    match Unix.getsockname sock with
+    | Unix.ADDR_INET (_, p) -> p
+    | _ -> Alcotest.fail "no port"
+  in
+  match Unix.fork () with
+  | 0 ->
+    (try
+       let c, _ = Unix.accept sock in
+       let buf = Bytes.create 4096 in
+       ignore (Unix.read c buf 0 (Bytes.length buf));
+       let resp =
+         Printf.sprintf
+           "HTTP/1.1 200 OK\r\nContent-Type: application/json\r\n\
+            Content-Length: %d\r\nConnection: close\r\n\r\n%s"
+           (String.length mock_body_rocq) mock_body_rocq
+       in
+       ignore (Unix.write_substring c resp 0 (String.length resp));
+       Unix.close c
+     with _ -> ());
+    Unix._exit 0
+  | child ->
+    Unix.close sock;
+    Unix.putenv "PROOF_BROKER_LLM_ENDPOINT"
+      (Printf.sprintf "http://127.0.0.1:%d/v1/chat/completions" port);
+    Unix.putenv "PROOF_BROKER_LLM_MODEL" "mock-model-rocq";
+    Unix.putenv "PROOF_BROKER_LLM_API_KEY" "";
+    let result = Adapter_llm.dispatch (sample_ir_rocq ()) in
+    ignore (Unix.waitpid [] child);
+    (match result with
+     | Cert c ->
+       Alcotest.(check string) "cert.format" "rocq-tactic-script" c.format;
+       (match c.payload with
+        | Tier3_proof_trace { trace_format; trace_data = `String s; _ } ->
+          Alcotest.(check string) "trace_format" "rocq-tactic-script"
+            trace_format;
+          Alcotest.(check string) "extracted Ltac script" "intros; lia." s
+        | _ -> Alcotest.fail "expected Tier3_proof_trace");
+       (match Verifier.verify c (sample_ir_rocq ()) with
+        | Tier3_replay_deferred { trace_format } ->
+          Alcotest.(check string) "verify reason picks up Rocq format"
+            "rocq-tactic-script" trace_format
+        | r ->
+          Alcotest.fail ("expected tier3_replay_deferred, got "
+                         ^ Verifier.kind_of_reason r))
+     | Failed f ->
+       Alcotest.fail ("Rocq mock endpoint should yield a cert; got "
+                      ^ Adapter.kind_of_failure f))
+
 let () =
   Alcotest.run "adapter_llm"
     [
       ( "render",
-        [ Alcotest.test_case "prompt" `Quick test_prompt_render;
+        [ Alcotest.test_case "prompt (Lean)" `Quick test_prompt_render;
+          Alcotest.test_case "prompt (Rocq)" `Quick test_prompt_render_rocq;
           Alcotest.test_case "extract fenced" `Quick
             test_extract_script_fenced;
           Alcotest.test_case "extract bare" `Quick
@@ -157,6 +251,8 @@ let () =
       ( "transport",
         [ Alcotest.test_case "fail-closed (no endpoint)" `Quick
             test_fail_closed;
-          Alcotest.test_case "mock endpoint → Tier-3 cert" `Quick
-            test_mock_endpoint ] );
+          Alcotest.test_case "mock endpoint → Lean Tier-3 cert" `Quick
+            test_mock_endpoint;
+          Alcotest.test_case "mock endpoint → Rocq Tier-3 cert" `Quick
+            test_mock_endpoint_rocq ] );
     ]
diff --git a/sdk/test/test_llm_reconstruct.ml b/sdk/test/test_llm_reconstruct.ml
index fb72f68..532a6b8 100644
--- a/sdk/test/test_llm_reconstruct.ml
+++ b/sdk/test/test_llm_reconstruct.ml
@@ -119,6 +119,45 @@ let test_prompt_render () =
   Alcotest.(check bool) "warns that the script is gated" true
     (contains p "kernel-and-axiom gate")
 
+(* Rocq-flavored variant: [source_system.name = "rocq"] routes
+   through [Adapter_llm.rocq_dialect] so the rendered theorem
+   skeleton uses [Theorem ... Proof. ... Qed.] form and asks for
+   a fenced ```coq block, not ```lean. *)
+let sample_ir_rocq () =
+  let ir = make_ir
+    ~free_vars:[ { name = "a"; ty = "Int" } ]
+    ~hypotheses:[
+      { name = "h1";
+        shell = App { symbol = "UF.p"; type_args = [];
+                      args = [ Var { name = "a" } ] } } ]
+    (App { symbol = "UF.p"; type_args = []; args = [ Var { name = "a" } ] })
+  in
+  { ir with source_system = { name = "rocq"; version = "0.0" } }
+
+let test_prompt_render_rocq () =
+  let ir = sample_ir_rocq () in
+  let cert =
+    sample_cert ~trace_format:"otter-resolution"
+      ~trace_data:(`String "(resolved C1 C2 → C3)") ir
+  in
+  let p = Llm_reconstruct.render_prompt ir cert in
+  Alcotest.(check bool) "names the source trace format" true
+    (contains p "otter-resolution");
+  Alcotest.(check bool) "embeds the trace verbatim" true
+    (contains p "resolved C1 C2");
+  Alcotest.(check bool) "translates Int → Z in binder" true
+    (contains p "(a : Z)");
+  Alcotest.(check bool) "states the goal as a Rocq theorem" true
+    (contains p "Theorem goal");
+  Alcotest.(check bool) "Proof. ... Qed. scaffold" true
+    (contains p "Proof.");
+  Alcotest.(check bool) "asks for a fenced coq block" true
+    (contains p "```coq");
+  Alcotest.(check bool) "does not leak Lean by-block" false
+    (contains p "```lean");
+  Alcotest.(check bool) "does not leak `:= by` syntax" false
+    (contains p ":= by")
+
 (** A non-Tier3 cert raises [Invalid_argument] from [render_prompt]
     — defensive, since this is a programming error not a runtime
     failure mode the caller should swallow. *)
@@ -205,7 +244,8 @@ let () =
   Alcotest.run "llm_reconstruct"
     [
       ( "render",
-        [ Alcotest.test_case "prompt" `Quick test_prompt_render;
+        [ Alcotest.test_case "prompt (Lean)" `Quick test_prompt_render;
+          Alcotest.test_case "prompt (Rocq)" `Quick test_prompt_render_rocq;
           Alcotest.test_case "reject non-tier3" `Quick
             test_prompt_render_rejects_non_tier3 ] );
       ( "transport",
diff --git a/tools/axiom_allowlist.json b/tools/axiom_allowlist.json
index 71bfa1a..4fce7c0 100644
--- a/tools/axiom_allowlist.json
+++ b/tools/axiom_allowlist.json
@@ -417,6 +417,8 @@
     "pb_hol_function_composition_axiom_free":
       [],
     "pb_llm_replay_axiom_free":
+      [],
+    "pb_llm_reconstruct_axiom_free":
       []
   }
 }