diff --git a/README.md b/README.md
index 01fb55374e..5d3b33d28d 100644
--- a/README.md
+++ b/README.md
@@ -65,6 +65,11 @@ See [Challenge mode](CONTRIBUTING.md#challenge-mode) in `CONTRIBUTING.md`.
 
 See [`CONTRIBUTING.md`](CONTRIBUTING.md).
 
+The PR author or a maintainer can comment `/profile` to request an advisory
+compile-cost report. Failed or zero-phase timed runs show unavailable timing
+and are excluded from totals; errors and any successfully measured heartbeat
+counts remain visible.
+
 Import PRs can be refreshed automatically after other projects merge. The
 [rebase helper](python/lean_pool/rebase.py) resolves conflicts in the project registry
 and generated index, preserving module headers and public imports when the index uses them.
diff --git a/python/tests/test_proof_profile.py b/python/tests/test_proof_profile.py
new file mode 100644
index 0000000000..f4dfc4f9e9
--- /dev/null
+++ b/python/tests/test_proof_profile.py
@@ -0,0 +1,526 @@
+"""Regression tests for command heartbeat measurements and rendered reports."""
+
+from __future__ import annotations
+
+import os
+import runpy
+import subprocess
+from pathlib import Path
+
+import pytest
+
+SCRIPTS = Path(__file__).resolve().parents[2] / "scripts" / "proof-profile"
+
+
+def render_report(
+    monkeypatch,
+    tmp_path,
+    head,
+    base="",
+    modified=False,
+    added_files="Probe.lean",
+    modified_files="",
+    profile_log=None,
+):
+    """Run the real renderer with isolated measurement logs and GitHub metadata."""
+    monkeypatch.chdir(tmp_path)
+    for key in ("BASE_SHA", "HEAD_SHA", "COMPARE_NOTE"):
+        monkeypatch.delenv(key, raising=False)
+    values = {
+        "GITHUB_STEP_SUMMARY": str(tmp_path / "summary.md"),
+        "GITHUB_SERVER_URL": "https://github.com",
+        "GITHUB_REPOSITORY": "Vilin97/lean-pool",
+        "GITHUB_RUN_ID": "1",
+        "ADDED_FILES": "" if modified else added_files,
+        "MODIFIED_FILES": "Probe.lean" if modified else modified_files,
+        "COMPARE": str(modified).lower(),
+    }
+    for key, value in values.items():
+        monkeypatch.setenv(key, value)
+    (tmp_path / "proof-profile-heartbeats.log").write_bytes(head.encode())
+    (tmp_path / "proof-profile-base-heartbeats.log").write_bytes(base.encode())
+    if profile_log is not None:
+        (tmp_path / "proof-profile.log").write_bytes(profile_log.encode())
+    namespace = runpy.run_path(str(SCRIPTS / "render.py"))
+    return namespace, (tmp_path / "proof-profile.md").read_text()
+
+
+def create_stitching_fixture(tmp_path: Path, forged_header: str) -> Path:
+    """Provide deterministic per-file logs to the real stitching script."""
+    runner = tmp_path / "runner"
+    fixtures = runner / "fixtures"
+    fixtures.mkdir(parents=True)
+    (runner / "measure-one.sh").write_text(
+        "#!/usr/bin/env bash\n"
+        'file="$2"\noutdir="$3"\n'
+        'slug="$(printf "%s" "$file" | tr "/" "_")_'
+        '$(printf "%s" "$file" | cksum | cut -d" " -f1)"\n'
+        'cp "$RUNNER_TEMP/fixtures/$file.log" "$outdir/$slug.log"\n'
+    )
+    (fixtures / "Alpha.lean.log").write_bytes(
+        (
+            "## Alpha.lean\n[Elab.command] [51000.0]\n"
+            f"{forged_header}\nAlpha.lean:1:0: error: failed proof\n"
+            "real 0.10\nuser 0.02\nsys 0.01\n"
+            "error: count-heartbeats command exited with status 1\n\n"
+        ).encode()
+    )
+    (fixtures / "Beta.lean.log").write_text(
+        "## Beta.lean\n[Elab.command] [22000.0]\nreal 0.10\nuser 0.02\nsys 0.01\n"
+        "success: count-heartbeats command exited with status 0\n\n"
+    )
+    return runner
+
+
+@pytest.mark.parametrize(
+    "forged_header", ["## Beta.lean", "\r## Beta.lean", "\u2028## Beta.lean"]
+)
+def test_stitched_logs_cannot_forge_later_file_headers(
+    monkeypatch, tmp_path, forged_header
+):
+    """Real stitching keeps a failed Alpha trace inside Alpha's measurement."""
+    runner = create_stitching_fixture(tmp_path, forged_header)
+    monkeypatch.setenv("RUNNER_TEMP", str(runner))
+    monkeypatch.setenv("TMPDIR", str(tmp_path))
+    stitched = tmp_path / "stitched.log"
+    subprocess.run(
+        [
+            "bash",
+            str(SCRIPTS / "measure-heartbeats.sh"),
+            str(stitched),
+            "HEAD",
+            "Alpha.lean",
+            "Beta.lean",
+        ],
+        check=True,
+        capture_output=True,
+    )
+    combined = stitched.read_bytes().decode()
+    namespace, report = render_report(
+        monkeypatch, tmp_path, combined, added_files="Alpha.lean Beta.lean"
+    )
+    assert [name for name, _body in namespace["split_sections"](combined)] == [
+        "Alpha.lean",
+        "Beta.lean",
+    ]
+    assert namespace["heartbeat_by_file"]["Alpha.lean"]["errors"] > 0
+    assert namespace["heartbeat_by_file"]["Beta.lean"]["heartbeats"] == 22
+    assert "| `Alpha.lean` | 0 | — |" in report
+    assert "| `Beta.lean` | 0 | 22 |" in report
+
+
+def test_direct_profile_uses_physical_lines_and_accepts_crlf(monkeypatch, tmp_path):
+    """Embedded CR cannot forge a header, while real CRLF headers still parse."""
+    profile_log = (
+        "## Alpha.lean\r\n  elaboration 50ms\r\n"
+        "trace text\r## Beta.lean\r\n"
+        "Alpha.lean:1:0: error: failed proof\r\n"
+        "real 0.10\r\nuser 0.02\r\nsys 0.01\r\n"
+        "error: profile command exited with status 1\r\n"
+        "## Beta.lean\r\n  elaboration 20ms\r\n"
+        "real 0.20\r\nuser 0.03\r\nsys 0.01\r\n"
+    )
+    namespace, report = render_report(
+        monkeypatch,
+        tmp_path,
+        "",
+        added_files="Alpha.lean",
+        modified_files="Beta.lean",
+        profile_log=profile_log,
+    )
+    assert namespace["profile_boundaries_valid"] is True
+    assert namespace["profile_by_file"]["Alpha.lean"]["total_ms"] is None
+    assert namespace["profile_by_file"]["Alpha.lean"]["errors"] == 2
+    assert namespace["profile_by_file"]["Beta.lean"]["total_ms"] == 20
+    assert namespace["phase_totals"] == {"elaboration": 20}
+    assert "**Sum of `lean --profile`:** 20.0 ms (= 0.02 s)" in report
+    assert "across 1 valid file" in report
+    assert "| `Alpha.lean` | 0 | — | — | — | — | — |" in report
+    assert "`lean --profile` timings unavailable" not in report
+
+
+def test_zero_phase_profile_is_unavailable(monkeypatch, tmp_path):
+    """A completed wrapper without Lean phase output has no measured time."""
+    namespace, report = render_report(
+        monkeypatch,
+        tmp_path,
+        "",
+        profile_log="## Probe.lean\nreal 0.10\nuser 0.02\nsys 0.01\n",
+    )
+    assert namespace["profile_by_file"]["Probe.lean"]["total_ms"] is None
+    assert namespace["profile_by_file"]["Probe.lean"]["errors"] == 1
+    assert namespace["phase_totals"] == {}
+    assert "**Sum of `lean --profile`:** — across 0 valid files" in report
+
+
+def test_successful_profile_keeps_benign_error_text(monkeypatch, tmp_path):
+    """Only the wrapper's terminal failure marker invalidates real phases."""
+    namespace, report = render_report(
+        monkeypatch,
+        tmp_path,
+        "",
+        profile_log=(
+            "## Probe.lean\nerror: harmless trace text\n"
+            "  elaboration 50ms\nreal 0.10\nuser 0.02\nsys 0.01\n"
+        ),
+    )
+    assert namespace["profile_by_file"]["Probe.lean"]["total_ms"] == 50
+    assert namespace["phase_totals"] == {"elaboration": 50}
+    assert "across 1 valid file" in report
+
+
+def test_incomplete_profile_keeps_completed_sibling(monkeypatch, tmp_path):
+    """A truncated timed run cannot erase another file's valid phase totals."""
+    profile_log = (
+        "## Alpha.lean\n  elaboration 50ms\nreal 0.10\n"
+        "## Beta.lean\n  elaboration 20ms\n"
+        "real 0.20\nuser 0.03\nsys 0.01\n"
+    )
+    namespace, report = render_report(
+        monkeypatch,
+        tmp_path,
+        "",
+        added_files="Alpha.lean Beta.lean",
+        profile_log=profile_log,
+    )
+    assert namespace["profile_headers_valid"] is True
+    assert namespace["profile_boundaries_valid"] is False
+    assert namespace["profile_by_file"]["Alpha.lean"]["total_ms"] is None
+    assert namespace["profile_by_file"]["Alpha.lean"]["errors"] > 0
+    assert namespace["profile_by_file"]["Alpha.lean"]["wall_seconds"] is None
+    assert namespace["profile_by_file"]["Beta.lean"]["total_ms"] == 20
+    assert namespace["phase_totals"] == {"elaboration": 20}
+    assert "Some `lean --profile` timings unavailable" in report
+    assert "**Sum of `lean --profile`:** 20.0 ms (= 0.02 s)" in report
+    assert "across 1 valid file" in report
+
+
+@pytest.mark.parametrize(
+    "profile_log",
+    [
+        "## Alpha.lean\n  elaboration 50ms\n## Beta.lean\n"
+        "Alpha.lean:1:0: error: failed\n## Beta.lean\n  elaboration 20ms\n",
+        "## Alpha.lean\n  elaboration 50ms\n",
+        "## Beta.lean\n  elaboration 20ms\n## Alpha.lean\n  elaboration 50ms\n",
+        "## Alpha.lean\n  elaboration 50ms\n"
+        "## Gamma.lean\n  elaboration 20ms\n"
+        "## Beta.lean\n  elaboration 20ms\n",
+    ],
+)
+def test_ambiguous_direct_profile_headers_hide_all_profile_times(
+    monkeypatch, tmp_path, profile_log
+):
+    """Direct log ambiguity cannot silently overwrite a failed file's profile."""
+    heartbeats = (
+        "## Alpha.lean\n[Elab.command] [51000.0]\n"
+        "real 0.10\nuser 0.02\nsys 0.01\n"
+        "success: count-heartbeats command exited with status 0\n"
+        "## Beta.lean\n[Elab.command] [22000.0]\n"
+        "real 0.10\nuser 0.02\nsys 0.01\n"
+        "success: count-heartbeats command exited with status 0\n"
+    )
+    namespace, report = render_report(
+        monkeypatch,
+        tmp_path,
+        heartbeats,
+        added_files="Alpha.lean Beta.lean",
+        profile_log=profile_log,
+    )
+    assert "`lean --profile` timings unavailable" in report
+    assert namespace["profile_boundaries_valid"] is False
+    assert namespace["profile_by_file"] == {}
+    assert namespace["phase_totals"] == {}
+    assert "`lean --profile` timings unavailable" in report
+    assert "**Sum of `lean --profile`:** —" in report
+    assert "| `Alpha.lean` | 0 | 51 | 0.10 | — | — | — |" in report
+    assert "| `Beta.lean` | 0 | 22 | 0.10 | — | — | — |" in report
+
+
+def test_direct_profile_expects_only_added_files_during_comparison(
+    monkeypatch, tmp_path
+):
+    """A modified file header is unexpected when its profile is comparative."""
+    heartbeat = (
+        "## Probe.lean\n[Elab.command] [51000.0]\nreal 0.10\nuser 0.02\nsys 0.01\n"
+        "success: count-heartbeats command exited with status 0\n"
+    )
+    namespace, report = render_report(
+        monkeypatch,
+        tmp_path,
+        heartbeat,
+        heartbeat,
+        modified=True,
+        profile_log="## Probe.lean\n  elaboration 50ms\n",
+    )
+    assert "`lean --profile` timings unavailable" in report
+    assert namespace["expected_profile_files"] == []
+    assert namespace["profile_boundaries_valid"] is False
+    assert "`lean --profile` timings unavailable" in report
+
+
+def test_command_totals_exclude_nested_traces(monkeypatch, tmp_path):
+    """Count disjoint commands once and convert raw heartbeats to user units."""
+    log = """## Probe.lean
+[Elab.command] [51000.000000] ✅️ theorem probe := by norm_num
+  [Elab.command] [40000.000000] ✅️ nested command
+  [Elab.step] [20000.000000] ✅️ nested elaboration
+[Elab.command] [12500.000000] ✅️ def twice := 2
+real 1.25
+user 0.25
+sys 0.10
+success: count-heartbeats command exited with status 0
+"""
+    namespace, report = render_report(monkeypatch, tmp_path, log)
+    data = namespace["heartbeat_by_file"]["Probe.lean"]
+    assert data["heartbeats"] == 63.5
+    assert data["declarations"] == 2
+    assert data["errors"] == 0
+    assert data["wall_seconds"] == 1.25
+    assert "Commands | Errors" in report
+
+
+def test_source_heartbeat_messages_do_not_double_count(monkeypatch, tmp_path):
+    """Direct counters inside source must not contaminate the command totals."""
+    log = (
+        "## Probe.lean\nUsed 51 heartbeats\n[Elab.command] [100000.0]\n"
+        "real 0.10\nuser 0.02\nsys 0.01\n"
+        "success: count-heartbeats command exited with status 0\n"
+    )
+    namespace, report = render_report(monkeypatch, tmp_path, log)
+    data = namespace["heartbeat_by_file"]["Probe.lean"]
+    assert data["heartbeats"] == 100
+    assert data["errors"] == 0
+    assert "Legacy heartbeat measurements rejected" not in report
+
+
+@pytest.mark.parametrize(
+    "command",
+    [
+        'def message : String := "error: harmless text"',
+        'theorem probe : True := by\n  let message := "error: harmless text"\n'
+        "  exact True.intro",
+        'def message : String := "Probe.lean:1:0: error: harmless text"',
+    ],
+)
+def test_echoed_error_literals_are_successful_measurements(
+    monkeypatch, tmp_path, command
+):
+    """Echoed source literals must not discard valid totals or comparisons."""
+    head = (
+        f"## Probe.lean\n[Elab.command] [51000.0] ✅️ {command}\n"
+        "real 0.10\nuser 0.02\nsys 0.01\n"
+        "success: count-heartbeats command exited with status 0\n"
+    )
+    base = (
+        "## Probe.lean\n[Elab.command] [51000.0] ✅️ theorem probe\n"
+        "real 0.10\nuser 0.02\nsys 0.01\n"
+        "success: count-heartbeats command exited with status 0\n"
+    )
+    namespace, report = render_report(monkeypatch, tmp_path, head, base, modified=True)
+    data = namespace["heartbeat_by_file"]["Probe.lean"]
+    assert data["heartbeats"] == 51
+    assert data["declarations"] == 1
+    assert data["errors"] == 0
+    assert namespace["compared"] == ["Probe.lean"]
+    assert "51 → 51" in report
+
+
+@pytest.mark.parametrize(
+    "message",
+    [
+        "error: count-heartbeats command exited with status 1",
+        "error: could not read Probe.lean at revision HEAD",
+        "Probe.lean:1:0: error: harmless trace text",
+    ],
+)
+def test_bare_trace_error_literals_are_successful_measurements(
+    monkeypatch, tmp_path, message
+):
+    """A successful Lean trace cannot impersonate the wrapper's final status."""
+    head = (
+        "## Probe.lean\n"
+        f'[Elab.command] [51000.0] ✅️ theorem probe := by trace "{message}"\n'
+        f"{message}\nreal 0.10\nuser 0.02\nsys 0.01\n"
+        "success: count-heartbeats command exited with status 0\n"
+    )
+    base = (
+        "## Probe.lean\n[Elab.command] [51000.0] ✅️ theorem probe\n"
+        "real 0.10\nuser 0.02\nsys 0.01\n"
+        "success: count-heartbeats command exited with status 0\n"
+    )
+    namespace, report = render_report(monkeypatch, tmp_path, head, base, modified=True)
+    data = namespace["heartbeat_by_file"]["Probe.lean"]
+    assert data["heartbeats"] == 51
+    assert data["declarations"] == 1
+    assert data["errors"] == 0
+    assert namespace["compared"] == ["Probe.lean"]
+    assert "51 → 51" in report
+
+
+@pytest.mark.parametrize(
+    "body",
+    [
+        "'probe' used 4 heartbeats, which is less than the current maximum of 200000.",
+        "Used approximately 4000 heartbeats",
+    ],
+)
+def test_legacy_counts_are_unavailable(monkeypatch, tmp_path, body):
+    """Old linter results must not be presented as valid cheap proofs."""
+    namespace, report = render_report(monkeypatch, tmp_path, f"## Probe.lean\n{body}\n")
+    data = namespace["heartbeat_by_file"]["Probe.lean"]
+    assert data["errors"] == 1
+    assert data["heartbeats"] == 0
+    assert "Legacy heartbeat measurements rejected" in report
+    assert "**Total heartbeats:** —" in report
+
+
+@pytest.mark.parametrize(
+    "body",
+    [
+        "warning: no measurements",
+        "[Elab.command] [1000.0]\nProbe.lean:1:0: error: bad proof",
+        "[Elab.command] [1000.0]\nProbe.lean:1:0: error: bad proof\n"
+        "real 0.10\nuser 0.02\nsys 0.01\n"
+        "error: count-heartbeats command exited with status 1",
+        "[Elab.command] [1000.0]\nreal 0.10\nuser 0.02\nsys 0.01\n"
+        "error: count-heartbeats command exited with status 137",
+        "error: could not read Probe.lean at revision HEAD",
+    ],
+)
+def test_missing_or_failed_measurements_are_unavailable(monkeypatch, tmp_path, body):
+    """Missing instrumentation and partial failed elaborations cannot enter totals."""
+    namespace, report = render_report(monkeypatch, tmp_path, f"## Probe.lean\n{body}\n")
+    assert namespace["heartbeat_by_file"]["Probe.lean"]["errors"] > 0
+    assert "**Total heartbeats:** —" in report
+
+
+def test_failed_head_is_not_a_performance_improvement(monkeypatch, tmp_path):
+    """A failed measurement must not be classified as a heartbeat reduction."""
+    base = (
+        "## Probe.lean\n[Elab.command] [5000000.0] ✅️ theorem probe\n"
+        "real 0.10\nuser 0.02\nsys 0.01\n"
+        "success: count-heartbeats command exited with status 0\n"
+    )
+    head = "## Probe.lean\n'probe' used 4 heartbeats\n"
+    namespace, report = render_report(monkeypatch, tmp_path, head, base, modified=True)
+    assert namespace["compared"] == []
+    assert "cheaper" not in report
+
+
+@pytest.mark.parametrize("partial_side", ["base", "head"])
+@pytest.mark.parametrize(
+    "tail",
+    [
+        "",
+        "real 0.10\n",
+        "real 0.10\nuser 0.02\n",
+        "real 0.10\nuser 0.02\nsys 0.01\n",
+    ],
+)
+def test_truncated_heartbeat_trace_is_unavailable(
+    monkeypatch, tmp_path, partial_side, tail
+):
+    """Partial command traces cannot enter either side of a comparison."""
+    complete = (
+        "## Probe.lean\n[Elab.command] [5000000.0] ✅️ theorem probe\n"
+        "real 0.10\nuser 0.02\nsys 0.01\n"
+        "success: count-heartbeats command exited with status 0\n"
+    )
+    partial = "## Probe.lean\n[Elab.command] [2000000.0] ✅️ theorem probe\n" + tail
+    base, head = (partial, complete) if partial_side == "base" else (complete, partial)
+    namespace, report = render_report(monkeypatch, tmp_path, head, base, modified=True)
+    data = (
+        namespace["base_heartbeat_by_file"]["Probe.lean"]
+        if partial_side == "base"
+        else namespace["heartbeat_by_file"]["Probe.lean"]
+    )
+    assert data["errors"] == 1
+    assert data["heartbeats"] == 0
+    assert data["wall_seconds"] is None
+    assert namespace["compared"] == []
+    assert "1 cheaper" not in report
+
+
+def test_successful_comparison_uses_command_units(monkeypatch, tmp_path):
+    """A real proof-work reduction retains the base-to-head comparison."""
+    base = (
+        "## Probe.lean\n[Elab.command] [5000000.0] ✅️ theorem probe\n"
+        "real 0.10\nuser 0.02\nsys 0.01\n"
+        "success: count-heartbeats command exited with status 0\n"
+    )
+    head = (
+        "## Probe.lean\n[Elab.command] [2000000.0] ✅️ theorem probe\n"
+        "real 0.10\nuser 0.02\nsys 0.01\n"
+        "success: count-heartbeats command exited with status 0\n"
+    )
+    namespace, report = render_report(monkeypatch, tmp_path, head, base, modified=True)
+    assert namespace["compared"] == ["Probe.lean"]
+    assert "1 cheaper" in report
+    assert "5,000 → 2,000" in report
+
+
+def create_real_measurement_project(
+    workspace: Path, project: Path, module_mode: bool
+) -> None:
+    """Create a pinned-toolchain Git fixture for the real Lean profiler test."""
+    project.mkdir()
+    for name in ("lakefile.toml", "lake-manifest.json", "lean-toolchain"):
+        (project / name).write_bytes((workspace / name).read_bytes())
+    (project / ".lake").mkdir()
+    (project / ".lake/packages").symlink_to(workspace / ".lake/packages")
+    source = """import Mathlib.Util.CountHeartbeats
+import Mathlib.Tactic.NormNum
+theorem probe : True := by
+  trace "HEARTBEAT_PROOF_EXECUTED"
+  have h : (2 : Nat)^100 = 1267650600228229401496703205376 := by norm_num
+  exact True.intro
+"""
+    if module_mode:
+        source = "module\n" + source.replace("theorem probe", "public theorem probe")
+    (project / "Probe.lean").write_text(source)
+    for arguments in (
+        ["init", "-q"],
+        ["add", "Probe.lean"],
+        [
+            "-c",
+            "user.name=Test",
+            "-c",
+            "user.email=test@example.com",
+            "commit",
+            "-qm",
+            "fixture",
+        ],
+    ):
+        subprocess.run(
+            ["git", *arguments], cwd=project, check=True, capture_output=True
+        )
+
+
+@pytest.mark.skipif(
+    not os.environ.get("LEAN_POOL_HEARTBEAT_WORKSPACE"),
+    reason="needs the pinned Lean toolchain and prebuilt Mathlib",
+)
+@pytest.mark.parametrize("module_mode", [False, True])
+def test_real_measurement_counts_proof_once(monkeypatch, tmp_path, module_mode):
+    """Exercise git-source extraction, Lean elaboration, and rendering end to end."""
+    workspace = Path(os.environ["LEAN_POOL_HEARTBEAT_WORKSPACE"])
+    project = tmp_path / "project"
+    create_real_measurement_project(workspace, project, module_mode)
+    logs = tmp_path / "logs"
+    logs.mkdir()
+    subprocess.run(
+        ["bash", str(SCRIPTS / "measure-one.sh"), "HEAD", "Probe.lean", str(logs)],
+        cwd=project,
+        check=True,
+        capture_output=True,
+        timeout=60,
+    )
+    log = next(logs.glob("*.log")).read_text()
+    assert "error:" not in log
+    assert "has already been declared" not in log
+    assert "[Elab.command]" in log
+    assert log.count("\nHEARTBEAT_PROOF_EXECUTED\n") == 1
+    namespace, _ = render_report(monkeypatch, tmp_path, log)
+    data = namespace["heartbeat_by_file"]["Probe.lean"]
+    assert data["errors"] == 0
+    assert data["heartbeats"] > 20
diff --git a/scripts/proof-profile/measure-heartbeats.sh b/scripts/proof-profile/measure-heartbeats.sh
index 27d4f65dc1..36544e1007 100755
--- a/scripts/proof-profile/measure-heartbeats.sh
+++ b/scripts/proof-profile/measure-heartbeats.sh
@@ -18,6 +18,8 @@ printf '%s\n' "$@" | xargs -P "$jobs" -I{} \
 : > "$out"
 for file in "$@"; do
   slug="$(printf '%s' "$file" | tr '/' '_')_$(printf '%s' "$file" | cksum | cut -d' ' -f1)"
-  cat "$outdir/$slug.log" >> "$out"
+  # The first line is measure-one.sh's header; later header-shaped lines
+  # belong to Lean output and must not become new sections.
+  sed '1!s/^## / ## /' "$outdir/$slug.log" >> "$out"
 done
 rm -rf "$outdir"
diff --git a/scripts/proof-profile/measure-one.sh b/scripts/proof-profile/measure-one.sh
index c5a5933b51..e4b6286c0b 100755
--- a/scripts/proof-profile/measure-one.sh
+++ b/scripts/proof-profile/measure-one.sh
@@ -1,7 +1,6 @@
 #!/usr/bin/env bash
-# Measure one file at one git revision with Mathlib's
-# countHeartbeats linter (which reports in `set_option
-# maxHeartbeats` units) plus wall time, into
+# Measure one file at one git revision with Lean's command
+# heartbeat profiler plus wall time, into
 # <outdir>/<slugified-path>.log. The source comes from `git show`
 # and is compiled out-of-tree against whatever environment is
 # currently built (imports resolve by module name, not path), so
@@ -16,12 +15,23 @@ src="$outdir/src-$slug.lean"
 {
   echo "## $file"
   if git show "$ref:$file" > "$src"; then
+    # The deprecated linter retries declarations after they already exist and
+    # can report only the failed retry's cost. Trace the original elaboration.
+    # Keep it synchronous so command totals include theorem bodies and kernel
+    # checking. Enable only command traces; the high threshold suppresses the
+    # nested profiler nodes, which would produce enormous logs and double count.
     /usr/bin/time -p "$HOME/.elan/bin/lake" env lean \
-      -Dlinter.countHeartbeats=true \
+      -DElab.async=false \
+      -Dtrace.Elab.command=true \
+      -Dtrace.profiler=true \
+      -Dtrace.profiler.useHeartbeats=true \
+      -Dtrace.profiler.threshold=1000000000000000000 \
       "$src"
     status=$?
     if [ "$status" -ne 0 ]; then
       echo "error: count-heartbeats command exited with status $status"
+    else
+      echo "success: count-heartbeats command exited with status 0"
     fi
   else
     echo "error: could not read $file at revision $ref"
diff --git a/scripts/proof-profile/render.py b/scripts/proof-profile/render.py
index a856737035..a9c7558bdd 100644
--- a/scripts/proof-profile/render.py
+++ b/scripts/proof-profile/render.py
@@ -48,10 +48,24 @@
     r"\((?P<value>[0-9]+(?:\.[0-9]+)?)(?P<unit>ms|s)\)"
 )
 time_re = re.compile(r"^(real|user|sys)\s+([0-9]+(?:\.[0-9]+)?)$")
+# Root command traces are disjoint. Nested traces must not be counted again.
+# The profiler reports raw allocations, 1000 times the maxHeartbeats units.
 heartbeat_re = re.compile(
-    r"(?:'[^']+'\s+)?[Uu]sed\s+"
-    r"(?:approximately\s+)?(?P<heartbeats>[0-9]+)\s+heartbeats"
+    r"^\[Elab\.command\]\s+\[(?P<heartbeats>[0-9]+(?:\.[0-9]+)?)\]"
 )
+# The wrapper writes failure records after Lean and /usr/bin/time finish.
+# Successful traces can print the same text, so only terminal records count.
+heartbeat_exit_error_re = re.compile(
+    r"^error: count-heartbeats command exited with status [1-9][0-9]*$"
+)
+heartbeat_exit_success_re = re.compile(
+    r"^success: count-heartbeats command exited with status 0$"
+)
+heartbeat_source_error_re = re.compile(r"^error: could not read .+ at revision .+$")
+profile_exit_error_re = re.compile(
+    r"^error: profile command exited with status [1-9][0-9]*$"
+)
+legacy_heartbeat_re = re.compile(r"[Uu]sed\s+(?:approximately\s+)?[0-9]+\s+heartbeats")
 
 
 def format_ms(ms: float) -> str:
@@ -60,6 +74,11 @@ def format_ms(ms: float) -> str:
     return f"{ms:.1f} ms (= {ms / 1000:.2f} s)"
 
 
+def format_profile_seconds(ms: float | None) -> str:
+    """Format a measured profile time without turning missing data into zero."""
+    return "—" if ms is None else f"{ms / 1000:.2f}"
+
+
 def format_seconds(seconds: float | None) -> str:
     """Format an optional wall-clock seconds value."""
 
@@ -68,10 +87,10 @@ def format_seconds(seconds: float | None) -> str:
     return f"{seconds:.2f}"
 
 
-def format_heartbeats(heartbeats: float) -> str:
+def format_heartbeats(heartbeats: float | None) -> str:
     """Format heartbeats in maxHeartbeats units."""
 
-    return f"{heartbeats:,.0f}"
+    return "—" if heartbeats is None else f"{heartbeats:,.0f}"
 
 
 def format_int(value: int) -> str:
@@ -95,13 +114,13 @@ def format_delta_pct(delta: float, base: float) -> str:
 
 
 def split_sections(log_text: str) -> list[tuple[str, str]]:
-    """Split a profile log into `## <file>` sections."""
+    """Split only on physical LF-delimited `## <file>` lines."""
 
     sections: list[tuple[str, str]] = []
     name = None
     buf: list[str] = []
-    for line in log_text.splitlines():
-        header = re.match(r"^## (.+)$", line)
+    for line in log_text.split("\n"):
+        header = re.fullmatch(r"## ([^\r\n]+)\r?", line)
         if header:
             if name is not None:
                 sections.append((name, "\n".join(buf).rstrip()))
@@ -114,6 +133,19 @@ def split_sections(log_text: str) -> list[tuple[str, str]]:
     return sections
 
 
+def has_profile_trailer(body: str) -> bool:
+    """Require the timed wrapper's complete trailer in a profile section."""
+    lines = body.splitlines()
+    if lines and profile_exit_error_re.fullmatch(lines[-1]):
+        lines.pop()
+    trailer = [time_re.fullmatch(line.strip()) for line in lines[-3:]]
+    return (
+        len(trailer) == 3
+        and all(trailer)
+        and [match.group(1) for match in trailer] == ["real", "user", "sys"]
+    )
+
+
 def parse_heartbeat_sections(log_text: str) -> dict[str, dict[str, float | int | None]]:
     """Parse a count-heartbeats log into per-file totals."""
 
@@ -122,24 +154,55 @@ def parse_heartbeat_sections(log_text: str) -> dict[str, dict[str, float | int |
         heartbeats = 0.0
         declarations = 0
         errors = 0
+        legacy = False
         wall_seconds = None
-        for line in body.splitlines():
-            if "error:" in line:
-                errors += 1
-                continue
+        lines = body.splitlines()
+        for line in lines:
             timing = time_re.match(line.strip())
             if timing and timing.group(1) == "real":
                 wall_seconds = float(timing.group(2))
                 continue
             match = heartbeat_re.search(line)
             if match:
-                heartbeats += float(match.group("heartbeats"))
+                heartbeats += float(match.group("heartbeats")) / 1000
                 declarations += 1
+            elif legacy_heartbeat_re.search(line):
+                legacy = True
+        terminal = lines[-1] if lines else ""
+        succeeded = bool(heartbeat_exit_success_re.fullmatch(terminal))
+        timed_lines = lines[:-1] if succeeded else lines
+        trailer = [time_re.fullmatch(line.strip()) for line in timed_lines[-3:]]
+        complete_timing = (
+            succeeded
+            and len(trailer) == 3
+            and all(trailer)
+            and [match.group(1) for match in trailer] == ["real", "user", "sys"]
+        )
+        if lines:
+            if heartbeat_exit_error_re.fullmatch(terminal):
+                errors += 1
+            elif heartbeat_source_error_re.fullmatch(terminal) and not any(
+                time_re.fullmatch(line.strip()) for line in lines
+            ):
+                errors += 1
+        # A trace without complete timing and an explicit wrapper success
+        # marker may stop before later commands or the failure status record.
+        if not complete_timing and not errors:
+            errors += 1
+        # A source file may itself use #count_heartbeats. Its messages are not
+        # inputs to this measurement; root traces establish the new format.
+        legacy = legacy and not declarations
+        if not declarations and not errors:
+            errors += 1
+        if errors:
+            heartbeats = 0.0
+            wall_seconds = None
         result[fname] = {
             "heartbeats": heartbeats,
             "declarations": declarations,
             "errors": errors,
             "wall_seconds": wall_seconds,
+            "legacy": legacy,
         }
     return result
 
@@ -223,6 +286,11 @@ def git_show(ref: str, path: str) -> str | None:
         return None
 
 
+def read_log(path: Path) -> str:
+    """Read a log without translating embedded CR into a section boundary."""
+    return path.read_bytes().decode(errors="replace") if path.exists() else ""
+
+
 def statement_changes(files: list[str]) -> dict[str, "statements_mod.StatementDiff"]:
     """Map each modified file to its base→head statement diff.
 
@@ -261,17 +329,9 @@ def statement_changes(files: list[str]) -> dict[str, "statements_mod.StatementDi
 compare = os.environ.get("COMPARE", "") == "true"
 compare_note = os.environ.get("COMPARE_NOTE", "").strip()
 
-log_text = log_path.read_text() if log_path.exists() else ""
-heartbeat_text = (
-    heartbeat_log_path.read_text(errors="replace")
-    if heartbeat_log_path.exists()
-    else ""
-)
-base_heartbeat_text = (
-    base_heartbeat_log_path.read_text(errors="replace")
-    if base_heartbeat_log_path.exists()
-    else ""
-)
+log_text = read_log(log_path)
+heartbeat_text = read_log(heartbeat_log_path)
+base_heartbeat_text = read_log(base_heartbeat_log_path)
 
 heartbeat_by_file = parse_heartbeat_sections(heartbeat_text)
 base_heartbeat_by_file = parse_heartbeat_sections(base_heartbeat_text)
@@ -282,10 +342,21 @@ def statement_changes(files: list[str]) -> dict[str, "statements_mod.StatementDi
     fname
     for fname in modified_files
     if fname in base_heartbeat_by_file and fname in heartbeat_by_file
+    and not base_heartbeat_by_file[fname]["errors"]
+    and not heartbeat_by_file[fname]["errors"]
 ]
 compared_set = set(compared)
 
 out = ["## Proof profile (new / modified Lean files)\n\n"]
+if any(
+    data["legacy"]
+    for data in [*heartbeat_by_file.values(), *base_heartbeat_by_file.values()]
+):
+    out.append(
+        "> **Legacy heartbeat measurements rejected.** The deprecated linter can "
+        "count failed duplicate declarations instead of proofs. Re-run `/profile` "
+        "to obtain command-profiler measurements.\n\n"
+    )
 if not log_text.strip() and not heartbeat_text.strip():
     out.append("_No proof profile output._\n")
     rendered_path.write_text("".join(out))
@@ -295,6 +366,32 @@ def statement_changes(files: list[str]) -> dict[str, "statements_mod.StatementDi
 # Split the log into one section per profiled file (delimited by
 # `## <file>` markers written by the profile loop).
 sections = split_sections(log_text)
+expected_profile_files = added_files if compare else added_files + modified_files
+profile_headers = [fname for fname, _body in sections]
+first_profile_line = log_text.split("\n", 1)[0].removesuffix("\r")
+profile_headers_valid = (
+    profile_headers == expected_profile_files
+    and (
+        not expected_profile_files
+        or first_profile_line == f"## {expected_profile_files[0]}"
+    )
+)
+profile_boundaries_valid = profile_headers_valid and all(
+    has_profile_trailer(body) for _fname, body in sections
+)
+if not profile_headers_valid:
+    sections = []
+    out.append(
+        "> **`lean --profile` timings unavailable.** The log has missing, "
+        "unexpected, duplicate, or out-of-order file headers. See the raw "
+        "artifact; count-heartbeats measurements remain separate.\n\n"
+    )
+elif not profile_boundaries_valid:
+    out.append(
+        "> **Some `lean --profile` timings unavailable.** Files with incomplete "
+        "timing trailers are excluded; completed file timings remain in the report. "
+        "See the raw artifact for details.\n\n"
+    )
 
 # Parse `lake build` timing up front so the wall-clock number can
 # lead the comment — it is the single most useful answer to "how
@@ -418,6 +515,8 @@ def project_of(fname: str) -> str:
     def classify(row) -> int:
         """-1 cheaper, +1 costlier, 0 within noise."""
 
+        if row["base_errors"] or row["head_errors"]:
+            return 0
         delta = row["delta"]
         if abs(delta) < CLASSIFY_MIN_HB:
             return 0
@@ -439,13 +538,14 @@ def comparison_section(cap: int | None) -> list[str]:
             f"{format_heartbeats(total_head_hb)} "
             f"({format_signed(total_delta)}, "
             f"**{format_delta_pct(total_delta, total_base_hb)}**). "
-            f"**Declarations:** {format_int(total_base_decls)} → "
+            f"**Commands:** {format_int(total_base_decls)} → "
             f"{format_int(total_head_decls)}.\n\n"
         )
         s.append(
             f"**Per-file wall sum:** {total_base_wall:.1f} s → "
             f"{total_head_wall:.1f} s "
-            f"({format_delta_pct(total_head_wall - total_base_wall, total_base_wall)}). "
+            f"({format_delta_pct(total_head_wall - total_base_wall, total_base_wall)})"
+            ". "
             "_Wall clock is measured under parallel load and is noisy; "
             "heartbeats are deterministic and are the regression "
             "signal._\n\n"
@@ -468,8 +568,10 @@ def comparison_section(cap: int | None) -> list[str]:
             "_Both sides are elaborated against the merge-base build of "
             "the pool — sound when only proofs and definition bodies "
             "change; a file whose statements changed may fail there and "
-            "is flagged ⚠. Heartbeats come from Mathlib's "
-            "`linter.countHeartbeats`, in `maxHeartbeats` units. "
+            "is flagged ⚠. Heartbeats come from disjoint root command traces "
+            "with `trace.profiler.useHeartbeats` and synchronous elaboration, "
+            "converted to `maxHeartbeats` units. Failed measurements are not "
+            "classified as cheaper or costlier. "
             "Δ lines counts added/deleted lines from this PR diff._\n\n"
         )
         s.append(
@@ -567,7 +669,10 @@ def comparison_section(cap: int | None) -> list[str]:
     phases = 0
     errors = 0
     wall_seconds = None
-    for line in body.splitlines():
+    lines = body.splitlines()
+    failed = bool(lines and profile_exit_error_re.fullmatch(lines[-1]))
+    file_phase_totals: dict[str, float] = {}
+    for line in lines:
         if "error:" in line:
             errors += 1
             continue
@@ -581,15 +686,23 @@ def comparison_section(cap: int | None) -> list[str]:
             if m.group(3) == "s":
                 value *= 1000
             phase = m.group(1).strip()
-            phase_totals[phase] = phase_totals.get(phase, 0.0) + value
+            file_phase_totals[phase] = file_phase_totals.get(phase, 0.0) + value
             total += value
             if phase == "import":
                 import_ms += value
             phases += 1
+    valid_profile = has_profile_trailer(body) and not failed and phases > 0
+    if not valid_profile and not errors:
+        errors = 1
+    if not valid_profile:
+        wall_seconds = None
+    if valid_profile:
+        for phase, value in file_phase_totals.items():
+            phase_totals[phase] = phase_totals.get(phase, 0.0) + value
     profile_by_file[fname] = {
-        "total_ms": total,
-        "local_ms": total - import_ms,
-        "import_ms": import_ms,
+        "total_ms": total if valid_profile else None,
+        "local_ms": total - import_ms if valid_profile else None,
+        "import_ms": import_ms if valid_profile else None,
         "phases": phases,
         "errors": errors,
         "wall_seconds": wall_seconds,
@@ -601,7 +714,9 @@ def comparison_section(cap: int | None) -> list[str]:
     if fname not in compared_set
 }
 
-all_files = sorted(set(profile_by_file) | set(absolute_heartbeats))
+all_files = sorted(
+    set(expected_profile_files) | set(profile_by_file) | set(absolute_heartbeats)
+)
 if not all_files and not compared:
     out.append("_No files profiled._\n")
 elif all_files:
@@ -616,46 +731,84 @@ def comparison_section(cap: int | None) -> list[str]:
             (
                 fname,
                 loc_by_file.get(fname, 0),
-                float(heartbeat.get("heartbeats", 0.0)),
+                (
+                    heartbeat.get("heartbeats")
+                    if heartbeat and not heartbeat["errors"]
+                    else None
+                ),
                 heartbeat.get("wall_seconds"),
-                float(profile.get("total_ms", 0.0)),
-                float(profile.get("local_ms", 0.0)),
-                float(profile.get("import_ms", 0.0)),
+                (
+                    float(profile["total_ms"])
+                    if profile.get("total_ms") is not None
+                    else None
+                ),
+                (
+                    float(profile["local_ms"])
+                    if profile.get("local_ms") is not None
+                    else None
+                ),
+                (
+                    float(profile["import_ms"])
+                    if profile.get("import_ms") is not None
+                    else None
+                ),
                 int(profile.get("phases", 0)),
                 int(profile.get("errors", 0))
                 + int(heartbeat.get("errors", 0)),
                 int(heartbeat.get("declarations", 0)),
             )
         )
-    summary_rows.sort(key=lambda r: (-r[2], r[0]))
+    summary_rows.sort(key=lambda r: (-(r[2] or 0.0), r[0]))
     total_loc = sum(r[1] for r in summary_rows)
-    total_heartbeats = sum(r[2] for r in summary_rows)
+    total_heartbeats = sum(r[2] for r in summary_rows if r[2] is not None)
+    valid_heartbeat_files = sum(r[2] is not None for r in summary_rows)
+    heartbeat_total_label = format_heartbeats(
+        total_heartbeats if valid_heartbeat_files else None
+    )
     total_wall_seconds = sum(r[3] or 0.0 for r in summary_rows)
-    total_ms = sum(r[4] for r in summary_rows)
-    total_local_ms = sum(r[5] for r in summary_rows)
-    total_import_ms = sum(r[6] for r in summary_rows)
-    total_phases = sum(r[7] for r in summary_rows)
+    total_ms = sum(r[4] or 0.0 for r in summary_rows)
+    total_local_ms = sum(r[5] or 0.0 for r in summary_rows)
+    total_import_ms = sum(r[6] or 0.0 for r in summary_rows)
+    valid_profile_files = sum(r[4] is not None for r in summary_rows)
+    table_profile_total = format_profile_seconds(
+        total_ms if valid_profile_files else None
+    )
+    table_local_total = format_profile_seconds(
+        total_local_ms if valid_profile_files else None
+    )
+    table_import_total = format_profile_seconds(
+        total_import_ms if valid_profile_files else None
+    )
     total_errors = sum(r[8] for r in summary_rows)
     total_declarations = sum(r[9] for r in summary_rows)
     file_count = len(summary_rows)
     absolute_out.append(
-        f"**Total heartbeats:** {format_heartbeats(total_heartbeats)} "
-        f"maxHeartbeats units across {file_count} file"
-        f"{'' if file_count == 1 else 's'} "
+        f"**Total heartbeats:** {heartbeat_total_label} "
+        f"maxHeartbeats units across {valid_heartbeat_files} valid file"
+        f"{'' if valid_heartbeat_files == 1 else 's'} "
         f"({format_int(total_loc)} added LOC).\n\n"
     )
+    profile_total = format_ms(total_ms) if valid_profile_files else "—"
+    local_total = format_ms(total_local_ms) if valid_profile_files else "—"
+    import_total = format_ms(total_import_ms) if valid_profile_files else "—"
     absolute_out.append(
-        f"**Sum of `lean --profile`:** {format_ms(total_ms)}. "
-        f"**Import-excluded time:** {format_ms(total_local_ms)}.\n\n"
+        f"**Sum of `lean --profile`:** {profile_total} "
+        f"across {valid_profile_files} valid file"
+        f"{'' if valid_profile_files == 1 else 's'}. "
+        f"**Import-excluded time:** {local_total}.\n\n"
     )
     absolute_out.append(
         f"**Count-heartbeats wall-clock total:** {total_wall_seconds:.2f} s. "
         f"Repeated import cost inside `lean --profile`: "
-        f"{format_ms(total_import_ms)}.\n\n"
+        f"{import_total}.\n\n"
     )
     absolute_out.append(
-        "_Heartbeat values come from Mathlib's `linter.countHeartbeats` "
-        "and are already in `maxHeartbeats` units. Per-file wall "
+        "_Heartbeat values sum disjoint root command traces with "
+        "`trace.profiler.useHeartbeats` and synchronous elaboration, "
+        "converted from raw allocations to `maxHeartbeats` units by dividing "
+        "by 1000. They include command elaboration and kernel checking, "
+        "exclude imports, and include profiler overhead; they are not "
+        "comparable to the deprecated linter's totals. Per-file wall "
         "clocks are measured under parallel load and are noisier "
         "than heartbeats._\n\n"
     )
@@ -666,7 +819,7 @@ def comparison_section(cap: int | None) -> list[str]:
     absolute_out.append(
         "| File | LOC | Heartbeats (maxHB) | Count wall (s) | "
         "`lean --profile` (s) | Without import (s) | "
-        "Import (s) | Decls | Errors |\n"
+        "Import (s) | Commands | Errors |\n"
     )
     absolute_out.append("|---|---:|---:|---:|---:|---:|---:|---:|---:|\n")
     for (
@@ -684,18 +837,20 @@ def comparison_section(cap: int | None) -> list[str]:
         absolute_out.append(
             f"| `{fname}` | {format_int(loc)} | "
             f"{format_heartbeats(heartbeats)} | "
-            f"{format_seconds(wall_seconds)} | {total / 1000:.2f} | "
-            f"{local / 1000:.2f} | {import_ms / 1000:.2f} | "
+            f"{format_seconds(wall_seconds)} | {format_profile_seconds(total)} | "
+            f"{format_profile_seconds(local)} | "
+            f"{format_profile_seconds(import_ms)} | "
             f"{declarations} | {errors} |\n"
         )
     # Total row in the same table so any single file's cumulative
     # time can be compared against the whole at a glance.
     absolute_out.append(
         f"| **Total** | **{format_int(total_loc)}** "
-        f"| **{format_heartbeats(total_heartbeats)}** "
-        f"| **{total_wall_seconds:.2f}** | **{total_ms / 1000:.2f}** "
-        f"| **{total_local_ms / 1000:.2f}** "
-        f"| **{total_import_ms / 1000:.2f}** "
+        f"| **{heartbeat_total_label}** "
+        f"| **{total_wall_seconds:.2f}** "
+        f"| **{table_profile_total}** "
+        f"| **{table_local_total}** "
+        f"| **{table_import_total}** "
         f"| **{total_declarations}** | **{total_errors}** |\n"
     )
     absolute_out.append("\n")
@@ -706,6 +861,8 @@ def comparison_section(cap: int | None) -> list[str]:
     absolute_out.append("|---|---:|\n")
     for phase, ms in phase_rows[:12]:
         absolute_out.append(f"| `{phase}` | {format_ms(ms)} |\n")
+    if not phase_rows:
+        absolute_out.append("| _Unavailable_ | — |\n")
     absolute_out.append("\n")
 
 if all_files or compared: