diff --git a/crates/burrower-cli/src/main.rs b/crates/burrower-cli/src/main.rs
index e17f8e1..5f609af 100644
--- a/crates/burrower-cli/src/main.rs
+++ b/crates/burrower-cli/src/main.rs
@@ -11,7 +11,10 @@
 //!   given a goal, return ranked candidate "homes".
 
 use anyhow::Result;
-use burrower_core::{parse_goal, rank, Corpus, Ledger, ProverConfig, Swarm};
+use burrower_core::{
+    parse_goal, rank, record_reconciliation, Corpus, Ledger, ProofReconciliation, ProverConfig,
+    Swarm,
+};
 use clap::{Parser, Subcommand};
 use std::path::PathBuf;
 
@@ -122,6 +125,18 @@ enum Cmd {
         #[arg(long, default_value = "julia")]
         oracle_julia: PathBuf,
     },
+    /// Record a reconciliation receipt as UNVERIFIED evidence, not a proof.
+    Reconcile {
+        /// JSON file with the proof.reconciliation/1 receipt.
+        #[arg(long)]
+        receipt: PathBuf,
+        /// Original theorem statement for ledger identity.
+        #[arg(long)]
+        goal: String,
+        /// Existing interim Burrow Ledger (JSONL).
+        #[arg(long)]
+        ledger: PathBuf,
+    },
     /// Burrow Ledger inspection.
     Ledger {
         #[command(subcommand)]
@@ -371,6 +386,9 @@ fn handle_attempt(
     Ok(())
 }
 
+/// Dispatch the requested command. Reconciliation reads a JSON receipt and
+/// records it as proposed evidence, propagating read, parse, validation and
+/// ledger errors.
 fn main() -> Result<()> {
     let cli = Cli::parse();
     match cli.cmd {
@@ -401,6 +419,18 @@ fn main() -> Result<()> {
                 oracle_julia,
             )
         }
+        Cmd::Reconcile {
+            receipt,
+            goal,
+            ledger,
+        } => {
+            let body = std::fs::read_to_string(&receipt)?;
+            let evidence: ProofReconciliation = serde_json::from_str(&body)?;
+            let ledger = Ledger::open(&ledger)?;
+            record_reconciliation(&ledger, &goal, &evidence)?;
+            eprintln!("reconciliation evidence recorded as proposed, NOT verified");
+            return Ok(());
+        }
         Cmd::Ledger { sub } => return handle_ledger(sub),
         Cmd::Serve { socket } => return burrower_core::serve::run(socket),
         Cmd::Index { root, output } => {
diff --git a/crates/burrower-core/src/lib.rs b/crates/burrower-core/src/lib.rs
index 4d1db1b..c51b877 100644
--- a/crates/burrower-core/src/lib.rs
+++ b/crates/burrower-core/src/lib.rs
@@ -34,6 +34,7 @@ pub mod ids;
 pub mod ledger;
 pub mod oracle;
 pub mod ranking;
+pub mod reconciliation;
 pub mod serve;
 pub mod specialist;
 
@@ -49,6 +50,10 @@ pub use ledger::{
     RecordResult,
 };
 pub use ranking::{rank, Home};
+pub use reconciliation::{
+    record_reconciliation, CheckLeg, Checker, Correspondence, LegOutcome, OriginalProof,
+    ProofReconciliation, Route, RECONCILIATION_SCHEMA,
+};
 pub use specialist::{
     Algebraist, Combinatorialist, ConsensusHome, OrderTheorist, Reading, Specialist, Swarm,
     Synthesis,
diff --git a/crates/burrower-core/src/reconciliation.rs b/crates/burrower-core/src/reconciliation.rs
new file mode 100644
index 0000000..ad5d8d9
--- /dev/null
+++ b/crates/burrower-core/src/reconciliation.rs
@@ -0,0 +1,335 @@
+// SPDX-License-Identifier: MPL-2.0
+//! Typed *evidence claims* for the interim Agda -> Rocq/Coq and Lean
+//! reconciliation process. Validating this document does NOT run a checker,
+//! verify a signature or authenticate a CI receipt. Do not treat it as a
+//! kernel-level proof; only the cited checker runs can establish that.
+use crate::ledger::{goal_hash, new_id, now_iso, Ledger, LedgerRecord, RecordResult};
+use anyhow::Result;
+use serde::{Deserialize, Serialize};
+
+pub const RECONCILIATION_SCHEMA: &str = "proof.reconciliation/1";
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(rename_all = "snake_case")]
+pub enum Checker {
+    Agda,
+    Rocq,
+    Lean,
+}
+
+/// These describe a single leg; they do not replace the estate's closed
+/// proof-ledger status vocabulary (proven/argued/open/etc.).
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(rename_all = "snake_case")]
+pub enum LegOutcome {
+    Open,
+    Unavailable,
+    Failed,
+    Checked,
+    CheckedWithAxioms,
+}
+
+impl LegOutcome {
+    /// Whether the leg claims a check, with or without axioms.
+    fn checked(self) -> bool {
+        matches!(self, Self::Checked | Self::CheckedWithAxioms)
+    }
+}
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(rename_all = "snake_case")]
+pub enum Route {
+    OriginalAgda,
+    Converted,
+    Reproved,
+    Transported,
+}
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(rename_all = "snake_case")]
+pub enum Correspondence {
+    /// Source/target propositions and assumptions were compared.
+    Verified,
+    /// No comparison established; a transported accepted term is insufficient.
+    Unchecked,
+    /// Only appropriate for the Agda source leg.
+    NotApplicable,
+}
+
+/// A claim about a real checker run, rather than a proof-checking operation.
+#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
+pub struct CheckLeg {
+    pub checker: Checker,
+    pub route: Route,
+    pub outcome: LegOutcome,
+    pub artifact_path: Option<String>,
+    /// SHA-256 digest of the checked source or witness.
+    pub artifact_sha256: Option<String>,
+    pub checker_version: Option<String>,
+    pub invocation: Option<String>,
+    /// Immutable CI run URL, local signed execution receipt, or equivalent.
+    pub run_ref: Option<String>,
+    pub correspondence: Correspondence,
+    #[serde(default)]
+    pub axioms: Vec<String>,
+}
+
+#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
+pub struct OriginalProof {
+    pub language: String,
+    pub path: String,
+    pub sha256: String,
+}
+
+#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
+pub struct ProofReconciliation {
+    pub schema: String,
+    pub theorem_id: String,
+    pub original: OriginalProof,
+    pub agda: CheckLeg,
+    pub rocq: CheckLeg,
+    pub lean: CheckLeg,
+}
+
+/// Whether a value is present and contains non-whitespace characters.
+fn filled(s: &Option<String>) -> bool {
+    s.as_deref().is_some_and(|v| !v.trim().is_empty())
+}
+
+/// Whether a string has the shape of a SHA-256 digest in hexadecimal.
+fn sha256(s: &str) -> bool {
+    s.len() == 64 && s.bytes().all(|b| b.is_ascii_hexdigit())
+}
+
+impl ProofReconciliation {
+    /// Reject contradictory or under-specified evidence metadata.
+    ///
+    /// A successful validation is NOT a checked proof; callers must still
+    /// authenticate the run references and check the referenced artefacts.
+    /// Unchecked or unavailable legs can pass validation without run evidence.
+    ///
+    /// # Errors
+    ///
+    /// Returns a description of the first invalid schema, provenance, leg
+    /// route, run evidence, correspondence, axiom claim or Agda invocation.
+    pub fn validate(&self) -> std::result::Result<(), String> {
+        if self.schema != RECONCILIATION_SCHEMA {
+            return Err("unsupported reconciliation schema".into());
+        }
+        if self.theorem_id.trim().is_empty()
+            || self.original.language.trim().is_empty()
+            || self.original.path.trim().is_empty()
+            || !sha256(&self.original.sha256)
+        {
+            return Err("theorem identity or original proof provenance missing".into());
+        }
+        for (expected, leg) in [
+            (Checker::Agda, &self.agda),
+            (Checker::Rocq, &self.rocq),
+            (Checker::Lean, &self.lean),
+        ] {
+            if leg.checker != expected {
+                return Err(format!("leg checker mismatch: expected {expected:?}"));
+            }
+            let source_leg = expected == Checker::Agda;
+            let valid_route = if source_leg {
+                matches!(
+                    leg.route,
+                    Route::OriginalAgda | Route::Converted | Route::Reproved
+                )
+            } else {
+                matches!(leg.route, Route::Transported | Route::Reproved)
+            };
+            if !valid_route {
+                return Err(format!("invalid {expected:?} reconciliation route"));
+            }
+            if leg.outcome.checked() {
+                if !filled(&leg.artifact_path)
+                    || !leg.artifact_sha256.as_deref().is_some_and(sha256)
+                    || !filled(&leg.checker_version)
+                    || !filled(&leg.invocation)
+                    || !filled(&leg.run_ref)
+                {
+                    return Err(format!("checked {expected:?} leg lacks run evidence"));
+                }
+                if !source_leg && leg.correspondence != Correspondence::Verified {
+                    return Err(format!(
+                        "checked {expected:?} target lacks statement/assumptions comparison"
+                    ));
+                }
+                if source_leg && leg.correspondence != Correspondence::NotApplicable {
+                    return Err("Agda source leg must not claim a cross-prover comparison".into());
+                }
+                if leg.outcome == LegOutcome::Checked && !leg.axioms.is_empty() {
+                    return Err(format!("unchecked axioms in {expected:?} no-axiom claim"));
+                }
+                if leg.outcome == LegOutcome::CheckedWithAxioms
+                    && (leg.axioms.is_empty() || leg.axioms.iter().any(|a| a.trim().is_empty()))
+                {
+                    return Err(format!("{expected:?} axiomatic claim names no axioms"));
+                }
+                if source_leg {
+                    // The canonical policy requires this exact command-line option set.
+                    // A shell line is metadata only: it must be backed by run_ref.
+                    let words: Vec<&str> = leg
+                        .invocation
+                        .as_deref()
+                        .unwrap_or_default()
+                        .split_whitespace()
+                        .collect();
+                    if words.len() < 5
+                        || !words[0].rsplit('/').next().is_some_and(|cmd| cmd == "agda")
+                        || words[1..4] != ["--safe", "--without-K", "--cubical-compatible"]
+                        || words[4..].iter().any(|w| w.starts_with('-'))
+                    {
+                        return Err("Agda check missing canonical safe flags".into());
+                    }
+                }
+            } else if leg.correspondence == Correspondence::Verified && !source_leg {
+                return Err(format!(
+                    "unchecked {expected:?} leg claims verified correspondence"
+                ));
+            }
+        }
+        Ok(())
+    }
+}
+
+/// Append the *claim* to Burrower's existing interim JSONL ledger. The
+/// status remains "proposed": an imported receipt is not proof of execution.
+/// No second persistent database or new state store is introduced.
+/// `theorem_statement` supplies the ledger's goal identity and excerpt.
+///
+/// # Errors
+///
+/// Returns a validation error before appending if the receipt is invalid,
+/// or propagates an error from serialising or appending the ledger record.
+pub fn record_reconciliation(
+    ledger: &Ledger,
+    theorem_statement: &str,
+    receipt: &ProofReconciliation,
+) -> Result<()> {
+    receipt.validate().map_err(anyhow::Error::msg)?;
+    ledger.append(&LedgerRecord {
+        id: new_id(),
+        timestamp: now_iso(),
+        goal_hash: goal_hash(theorem_statement),
+        goal_id: Some(crate::ids::goal_content_id(theorem_statement)),
+        goal_excerpt: theorem_statement.chars().take(200).collect(),
+        specialist: "ProofReconciliation".to_string(),
+        approach: None,
+        result: Some(RecordResult {
+            status: "proposed".to_string(),
+            explanation:
+                "Reconciliation evidence submitted; checker runs not authenticated by Burrower"
+                    .into(),
+            artifacts: Vec::new(),
+        }),
+        learning: None,
+        extra: serde_json::json!({"proof_reconciliation": receipt}),
+    })
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use tempfile::tempdir;
+
+    const DIGEST: &str = "0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef";
+
+    fn checked(checker: Checker, route: Route, invocation: &str) -> CheckLeg {
+        CheckLeg {
+            checker,
+            route,
+            outcome: LegOutcome::Checked,
+            artifact_path: Some("verification/theorem".into()),
+            artifact_sha256: Some(DIGEST.into()),
+            checker_version: Some("pinned-1.0".into()),
+            invocation: Some(invocation.into()),
+            run_ref: Some("https://github.com/hyperpolymath/proof-burrower/actions/runs/1".into()),
+            correspondence: if checker == Checker::Agda {
+                Correspondence::NotApplicable
+            } else {
+                Correspondence::Verified
+            },
+            axioms: Vec::new(),
+        }
+    }
+
+    fn valid() -> ProofReconciliation {
+        ProofReconciliation {
+            schema: RECONCILIATION_SCHEMA.into(),
+            theorem_id: "theory/example/theorem1".into(),
+            original: OriginalProof {
+                language: "Idris2".into(),
+                path: "verification/theorem.idr".into(),
+                sha256: DIGEST.into(),
+            },
+            agda: checked(
+                Checker::Agda,
+                Route::Reproved,
+                "agda --safe --without-K --cubical-compatible verification/Theorem.agda",
+            ),
+            rocq: checked(Checker::Rocq, Route::Reproved, "rocq c theorem.v"),
+            lean: checked(Checker::Lean, Route::Reproved, "lake env lean Theorem.lean"),
+        }
+    }
+
+    #[test]
+    fn honest_record_roundtrip() {
+        let record = valid();
+        assert_eq!(record.validate(), Ok(()));
+        let roundtrip: ProofReconciliation =
+            serde_json::from_str(&serde_json::to_string(&record).unwrap()).unwrap();
+        assert_eq!(roundtrip, record);
+    }
+
+    #[test]
+    fn cannot_promote_uncompared_transport() {
+        let mut r = valid();
+        r.lean.route = Route::Transported;
+        r.lean.correspondence = Correspondence::Unchecked;
+        assert!(r.validate().is_err());
+    }
+
+    #[test]
+    fn cannot_hide_unsafe_agda_invocation() {
+        let mut r = valid();
+        r.agda.invocation = Some("agda --safe --without-K theorem.agda".into());
+        assert!(r.validate().is_err());
+    }
+
+    #[test]
+    fn cannot_promote_unattributed_result_or_axioms() {
+        let mut r = valid();
+        r.rocq.run_ref = None;
+        assert!(r.validate().is_err());
+        r = valid();
+        r.lean.axioms.push("classical_choice".into());
+        assert!(r.validate().is_err());
+        r.lean.outcome = LegOutcome::CheckedWithAxioms;
+        assert_eq!(r.validate(), Ok(()));
+    }
+
+    #[test]
+    fn unavailable_checker_is_not_a_success() {
+        let mut r = valid();
+        r.rocq.outcome = LegOutcome::Unavailable;
+        r.rocq.correspondence = Correspondence::Unchecked;
+        assert_eq!(r.validate(), Ok(()));
+    }
+
+    #[test]
+    fn persistence_never_claims_proven_without_external_check() {
+        let tmp = tempdir().unwrap();
+        let ledger = Ledger::open(tmp.path().join("ledger.jsonl")).unwrap();
+        record_reconciliation(&ledger, "Theorem1", &valid()).unwrap();
+        let rows = ledger.read_all().unwrap();
+        assert_eq!(rows.len(), 1);
+        assert_eq!(rows[0].result.as_ref().unwrap().status, "proposed");
+        assert_eq!(
+            rows[0].extra["proof_reconciliation"]["schema"],
+            RECONCILIATION_SCHEMA
+        );
+    }
+}
diff --git a/docs/PROOF-RECONCILIATION.adoc b/docs/PROOF-RECONCILIATION.adoc
new file mode 100644
index 0000000..dcb416d
--- /dev/null
+++ b/docs/PROOF-RECONCILIATION.adoc
@@ -0,0 +1,73 @@
+// SPDX-License-Identifier: MPL-2.0
+= Proof Reconciliation Receipts
+:toc:
+
+Proof Burrower discovers candidate proof locations and can ask ECHIDNA to
+run a prover; neither a search hit nor a proposed tactic establishes that
+a theory theorem has been checked.
+
+Estate policy: https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[Proof and Verification Policy].
+
+== Interim theory reconciliation
+
+The canonical primary checker invocation is:
+
+[source,bash]
+----
+agda --safe --without-K --cubical-compatible path/to/Theorem.agda
+----
+
+Record each original proof and Agda conversion or re-proof, its stable
+theorem identity, source and target digests, checker version and exact
+command, assumptions, kernel result, and CI execution evidence.
+
+Rocq/Coq and Lean are distinct recheck legs. A transported witness is not
+independent evidence until the target kernel accepts it and the source and
+target statements (and assumptions) are compared. A fresh re-proof is a
+valid fallback, with the statement comparison recorded. Preserve all
+prior evidence on unsuccessful conversion; a translation failure never
+refutes a theorem.
+
+Proof status remains the estate's canonical closed vocabulary:
+`proven`, `proven-with-postulates`, `tested-only`, `argued`,
+`open`. The route and execution state of an individual leg are
+separate metadata, not new global status tokens.
+
+A checker that was not invoked is `open` (unavailable), not `proven`.
+Current Burrower attempts use Isabelle; they do not claim to run the
+Agda/Rocq/Lean reconciliation pipeline. ECHIDNA will eventually
+coordinate the full process; this record is an interim evidence format,
+not a second proof engine.
+
+== Recording a reconciliation claim
+
+The first consumer is a typed evidence claim, not an automatic checker.
+Its schema identifier is `proof.reconciliation/1`. To ingest an existing
+JSON receipt (with source/target SHA-256 digests, checker versions, run
+references, and the Agda, Rocq and Lean legs), run:
+
+[source,bash]
+----
+cargo run --locked -p burrower -- reconcile \
+  --receipt path/to/receipt.json \
+  --goal 'the original theorem statement' \
+  --ledger path/to/burrow-ledger.jsonl
+----
+
+The CLI validates the metadata shape and consistency and appends a record
+with status `proposed`. The caller remains responsible for authenticating
+checker executions and comparing statements and assumptions. Do not elevate
+this receipt to `proven` merely because the CLI accepted it.
+
+To check an Agda source with the mandated flags:
+
+[source,bash]
+----
+bash scripts/agda-safe-check.sh verification/proofs/agda/Properties.agda
+bash tests/agda-safe-check.sh
+----
+
+The second command tests the *wrapper* with an artificial checker and
+negative controls; it does not prove Properties.agda. The first command
+requires a real Agda binary and suitable installed libraries and fails
+closed if either is missing or incompatible.
diff --git a/scripts/agda-safe-check.sh b/scripts/agda-safe-check.sh
new file mode 100644
index 0000000..eac4b04
--- /dev/null
+++ b/scripts/agda-safe-check.sh
@@ -0,0 +1,39 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# First-party Agda theory checks: keep the safety flags and module roots.
+set -euo pipefail
+if (( $# == 0 )); then
+  echo "usage: $0 FILE.agda [FILE.agda ...]" >&2
+  exit 2
+fi
+agda_bin="${AGDA_BIN:-agda}"
+checker="$(command -v -- "$agda_bin" || true)"
+if [[ -z "$checker" ]]; then
+  echo "Agda checker unavailable: $agda_bin" >&2
+  exit 127
+fi
+# Preserve an executable path when checking modules from their own roots.
+if [[ "$checker" != /* ]]; then
+  checker="$(realpath -e -- "$checker")"
+fi
+"$checker" --version >&2
+include_args=()
+if [[ -n "${AGDA_LIBRARY_INCLUDE:-}" ]]; then
+  if [[ ! -d "$AGDA_LIBRARY_INCLUDE" ]]; then
+    echo "Agda library source directory unavailable: $AGDA_LIBRARY_INCLUDE" >&2
+    exit 2
+  fi
+  include_args=(-i "$(realpath -e -- "$AGDA_LIBRARY_INCLUDE")")
+fi
+for source in "$@"; do
+  if [[ "$source" == -* || "$source" != *.agda || ! -f "$source" ]]; then
+    echo "Not a readable Agda source (options forbidden): $source" >&2
+    exit 2
+  fi
+  module="$(realpath -e -- "$source")"
+  # Module Properties in path/to/Properties.agda must be checked from
+  # path/to, rather than forcing a false module/path mismatch at repo root.
+  ( cd -- "$(dirname -- "$module")" &&
+    "$checker" --safe --without-K --cubical-compatible \
+      "${include_args[@]}" "$(basename -- "$module")" )
+done
diff --git a/tests/agda-safe-check.sh b/tests/agda-safe-check.sh
new file mode 100644
index 0000000..98ecce0
--- /dev/null
+++ b/tests/agda-safe-check.sh
@@ -0,0 +1,45 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Tests scripts/agda-safe-check.sh with a fake Agda executable.
+# Checks the canonical safe Agda options, rejection of --with-K, and failure when the checker is missing.
+set -euo pipefail
+root="$(cd "$(dirname "$0")/.." && pwd)"
+tmp="$(mktemp -d)"
+trap 'rm -rf "$tmp"' EXIT
+mkdir -p "$tmp/nested" "$tmp/stdlib"
+printf 'module Test where\n' > "$tmp/nested/Test.agda"
+cat > "$tmp/fake-agda" <<'SH'
+#!/usr/bin/env bash
+set -euo pipefail
+if [[ "${1:-}" == --version ]]; then
+  printf 'Agda version 2.8.0\n'
+else
+  printf '%s\n' "$@" > "$AGDA_CAPTURE"
+  pwd > "$AGDA_CWD_CAPTURE"
+fi
+SH
+chmod +x "$tmp/fake-agda"
+AGDA_BIN="$tmp/fake-agda" AGDA_CAPTURE="$tmp/capture" \
+ AGDA_CWD_CAPTURE="$tmp/cwd" bash "$root/scripts/agda-safe-check.sh" "$tmp/nested/Test.agda"
+mapfile -t args < "$tmp/capture"
+[[ "${#args[@]}" -eq 4 && "${args[0]}" == --safe ]]
+[[ "${args[1]}" == --without-K && "${args[2]}" == --cubical-compatible ]]
+[[ "${args[3]}" == Test.agda ]]
+[[ "$(cat "$tmp/cwd")" == "$tmp/nested" ]]
+AGDA_BIN="$tmp/fake-agda" AGDA_CAPTURE="$tmp/capture" AGDA_CWD_CAPTURE="$tmp/cwd" \
+ AGDA_LIBRARY_INCLUDE="$tmp/stdlib" bash "$root/scripts/agda-safe-check.sh" "$tmp/nested/Test.agda"
+mapfile -t args < "$tmp/capture"
+[[ "${#args[@]}" -eq 6 && "${args[3]}" == -i ]]
+[[ "${args[4]}" == "$tmp/stdlib" && "${args[5]}" == Test.agda ]]
+if AGDA_BIN="$tmp/fake-agda" AGDA_CAPTURE="$tmp/capture" \
+  bash "$root/scripts/agda-safe-check.sh" --with-K; then
+  echo "unsafe option was accepted" >&2; exit 1
+fi
+if AGDA_BIN="$tmp/not-installed" bash "$root/scripts/agda-safe-check.sh" "$tmp/nested/Test.agda"; then
+  echo "missing checker was accepted" >&2; exit 1
+fi
+if AGDA_BIN="$tmp/fake-agda" AGDA_LIBRARY_INCLUDE="$tmp/missing" \
+  bash "$root/scripts/agda-safe-check.sh" "$tmp/nested/Test.agda"; then
+  echo "missing include directory was accepted" >&2; exit 1
+fi
+echo 'Agda safe invocation, nested module, include path, and negative controls passed'