Enforce the Formalize execution-notes contract

autoform_cli/audit.py

@@ -211,6 +211,15 @@ def audit_graph(
                 )
             )
 
+        if derived[node_id].proved and article.has_execution_notes:
+            findings.append(
+                AuditFinding(
+                    article_path,
+                    "stale-execution-notes",
+                    "completed article retains Execution notes from an unfinished attempt",
+                )
+            )
+
         if node.mathlib and not declaration_names(node.mathlib_declaration or ""):
             findings.append(
                 AuditFinding(
@@ -252,13 +261,14 @@ def audit_graph(
 class _ArticleShape:
     statement_text: bool
     has_depends_section: bool
+    has_execution_notes: bool
 
 
 def _read_article(path: Path) -> _ArticleShape:
     try:
         text = path.read_text(encoding="utf-8")
     except (OSError, UnicodeError):
-        return _ArticleShape(False, False)
+        return _ArticleShape(False, False, False)
 
     lines = text.splitlines()
     start = _frontmatter_end(lines)
@@ -267,6 +277,7 @@ def _read_article(path: Path) -> _ArticleShape:
     before_first_h2 = True
     statement_text = False
     has_depends_section = False
+    has_execution_notes = False
     fence: tuple[str, int] | None = None
 
     for line in body.splitlines():
@@ -291,11 +302,13 @@ def _read_article(path: Path) -> _ArticleShape:
                 before_first_h2 = False
                 if title == "depends on":
                     has_depends_section = True
+                if title == "execution notes":
+                    has_execution_notes = True
             continue
         if seen_h1 and before_first_h2 and line.strip():
             statement_text = True
 
-    return _ArticleShape(statement_text, has_depends_section)
+    return _ArticleShape(statement_text, has_depends_section, has_execution_notes)
 
 
 def _source_findings(graph: Graph, node: Node, article_path: str) -> list[AuditFinding]:

autoform_cli/graph.py

@@ -392,6 +392,10 @@ def _parse_node(node_id: str, path: Path, text: str) -> tuple[_ParsedNode | None
         _SOURCES_SECTION: [],
     }
     section: str | None = None
+    execution_notes_seen = False
+    execution_notes_not_final_reported = False
+    statement_open = False
+    statement_text_seen = False
     fence: tuple[str, int] | None = None
     body = _HTML_COMMENT.sub("", "\n".join(lines[body_start:]))
 
@@ -412,14 +416,40 @@ def _parse_node(node_id: str, path: Path, text: str) -> tuple[_ParsedNode | None
         if heading:
             level = len(heading.group(1))
             heading_text = heading.group(2).strip()
+            heading_key = heading_text.casefold()
+            if (
+                execution_notes_seen
+                and level <= 2
+                and not execution_notes_not_final_reported
+            ):
+                issues.append(
+                    f"{node_id}: Execution notes must be the article's final section"
+                )
+                execution_notes_not_final_reported = True
             if level == 1:
                 title_count += 1
                 if title is None:
                     title = heading_text
+                    statement_open = True
+            elif title is not None and level <= 2:
+                statement_open = False
+            if heading_key == "execution notes":
+                section = None
+                execution_notes_seen = True
+                if level != 2:
+                    issues.append(
+                        f"{node_id}: Execution notes must be a top-level H2 section"
+                    )
+                if not statement_text_seen:
+                    issues.append(
+                        f"{node_id}: Execution notes must follow the article's mathematical statement"
+                    )
+                continue
             if level <= 2:
-                heading_key = heading_text.casefold()
                 section = heading_key if level == 2 and heading_key in targets else None
             continue
+        if statement_open and line.strip():
+            statement_text_seen = True
         if section is not None:
             for match in _LINK.finditer(_INLINE_CODE.sub("", line)):
                 target = match.group(1)

skills/formalize/SKILL.md

@@ -113,12 +113,18 @@ score instead.
 
 On acceptance, update only the claimed article with the exact compiled
 declaration and truthful assertions: `statement: formalized`, plus `proof:
-formalized` once the proof is complete. On a useful failed route, record only
-distilled reusable evidence under `## Execution notes`—the remaining goal,
-checked lemmas, and next route—never a transcript or retry counter. A missing
-prerequisite, an incorrect decomposition, a change another article needs, or a
-proof recorded without its statement returns to Roadmap instead of silently
-changing the DAG.
+formalized` once the proof is complete, and remove any stale `## Execution
+notes` from earlier failed attempts. On a useful failed route, record only
+distilled reusable evidence under one top-level `## Execution notes` section as
+the article's final section, after the mathematical statement and outside `##
+Depends on`, `## Proof depends on`, and `## Sources`. Replace that section's
+contents on a later failed route rather than appending another one; record the
+remaining goal, checked lemmas, and next route, never a transcript or retry
+counter. A missing
+prerequisite, an incorrect decomposition, or a change another article needs
+returns to Roadmap instead of silently changing the DAG. Never write `proof:
+formalized` without `statement: formalized`; graph loading rejects that
+inconsistent assertion rather than routing it to Roadmap.
 
 Run `autoform check <PROJECT>/blueprint --lean-root <PROJECT>` and `autoform
 audit <PROJECT>/blueprint --lean-root <PROJECT>`. Resolve every finding this

tests/test_audit.py

@@ -113,6 +113,28 @@ def test_clean_audit_has_stable_machine_readable_representation(tmp_path: Path)
     assert str(tmp_path) not in first.to_json()
 
 
+def test_completed_article_cannot_keep_stale_execution_notes(tmp_path: Path) -> None:
+    blueprint = tmp_path / "blueprint"
+    _coverage(blueprint)
+    article = _article(
+        blueprint,
+        "result.md",
+        declaration="theorem",
+        statement="formalized",
+        proof="formalized",
+        lean="Project.result",
+    )
+    article.write_text(
+        article.read_text(encoding="utf-8")
+        + "\n## Execution notes\n\nRemaining goal: obsolete.\n",
+        encoding="utf-8",
+    )
+
+    findings = _finding_map(blueprint)
+
+    assert any(code == "stale-execution-notes" for code, _ in findings["roadmap/result.md"])
+
+
 def test_audit_reports_formalizable_structure(tmp_path: Path) -> None:
     blueprint = tmp_path / "blueprint"
     _coverage(blueprint)

tests/test_graph.py

@@ -135,6 +135,99 @@ def test_rejects_invalid_nodes(tmp_path: Path, body: str, message: str) -> None:
         load_graph(blueprint)
 
 
+def test_execution_notes_cannot_nest_inside_dependency_sections(tmp_path: Path) -> None:
+    blueprint = tmp_path / "blueprint"
+    _node(blueprint, "base.md", "# Base\n")
+    _node(
+        blueprint,
+        "result.md",
+        "# Result\n\nA statement.\n\n## Proof depends on\n\n"
+        "### Execution notes\n\n[Base](base.md)\n",
+    )
+
+    with pytest.raises(GraphValidationError, match="Execution notes must be a top-level H2"):
+        load_graph(blueprint)
+
+
+def test_execution_notes_must_be_the_final_article_section(tmp_path: Path) -> None:
+    blueprint = tmp_path / "blueprint"
+    _node(
+        blueprint,
+        "result.md",
+        "# Result\n\nA statement.\n\n## Execution notes\n\nTry induction.\n\n"
+        "## Depends on\n\nNone.\n\n## Sources\n\nNone.\n",
+    )
+
+    with pytest.raises(GraphValidationError) as caught:
+        load_graph(blueprint)
+
+    assert caught.value.issues.count(
+        "result: Execution notes must be the article's final section"
+    ) == 1
+
+
+def test_execution_notes_must_follow_the_mathematical_statement(tmp_path: Path) -> None:
+    blueprint = tmp_path / "blueprint"
+    _node(
+        blueprint,
+        "result.md",
+        "# Result\n\n## Execution notes\n\nTry induction.\n",
+    )
+
+    with pytest.raises(
+        GraphValidationError,
+        match="Execution notes must follow the article's mathematical statement",
+    ):
+        load_graph(blueprint)
+
+
+def test_execution_notes_follow_statement_text_under_a_subheading(tmp_path: Path) -> None:
+    blueprint = tmp_path / "blueprint"
+    _node(
+        blueprint,
+        "result.md",
+        "# Result\n\n### Named case\n\nA mathematical statement.\n\n"
+        "## Execution notes\n\nTry induction.\n",
+    )
+
+    assert load_graph(blueprint).nodes["result"].title == "Result"
+
+
+@pytest.mark.parametrize(
+    ("section", "statement_dependencies", "proof_dependencies", "sources"),
+    [
+        ("Depends on", ("base",), (), ()),
+        ("Proof depends on", (), ("base",), ()),
+        ("Sources", (), (), ("base.md",)),
+    ],
+)
+def test_structured_final_execution_notes_do_not_change_article_relations(
+    tmp_path: Path,
+    section: str,
+    statement_dependencies: tuple[str, ...],
+    proof_dependencies: tuple[str, ...],
+    sources: tuple[str, ...],
+) -> None:
+    blueprint = tmp_path / "blueprint"
+    _node(blueprint, "base.md", "# Base\n\nA base statement.\n")
+    _node(blueprint, "other.md", "# Other\n\nAnother statement.\n")
+    _node(
+        blueprint,
+        "result.md",
+        f"# Result\n\nA result statement.\n\n## {section}\n\n[Base](base.md)\n\n"
+        "## Execution notes\n\n### Remaining goal\n\nTry induction.\n\n"
+        "### Next route\n\nTried [Other](other.md).\n",
+    )
+
+    graph = load_graph(blueprint)
+    node = graph.nodes["result"]
+
+    assert node.statement_dependencies == statement_dependencies
+    assert node.proof_dependencies == proof_dependencies
+    assert node.dependencies == tuple(dict.fromkeys((*statement_dependencies, *proof_dependencies)))
+    assert node.sources == sources
+
+
 def test_rejects_self_edge(tmp_path: Path) -> None:
     blueprint = tmp_path / "blueprint"
     _node(blueprint, "self.md", "# Self\n## Depends on\n[Self](self.md)\n")

tests/test_skill_examples.py

@@ -76,6 +76,12 @@ def test_formalize_replaces_custom_orchestration_with_the_markdown_frontier(
     assert "no custom scheduler or provider adapter" in normalized
     assert "ready, running, retrying, failed, or blocked scheduler states" in normalized
     assert "never a transcript or retry counter" in normalized
+    assert "remove any stale `## Execution notes`" in normalized
+    assert "outside `## Depends on`, `## Proof depends on`, and `## Sources`" in normalized
+    assert "article's final section" in normalized
+    assert "rather than appending another one" in normalized
+    assert "Never write `proof: formalized` without `statement: formalized`" in normalized
+    assert "graph loading rejects that inconsistent assertion" in normalized
     assert (
         "require the same `phase`, `blockers`, `dependencies`, `article_revision`, "
         "`open_statements`, `assumes`, and `revision` as the first read"