/formal-review

name: formal-review
description: "This skill should be used when the user asks to \"formal review\", \"formal lens review\", or invokes /formal-review. A fixed-lens PR review for this repository's formally-structured protocol changes: it pins a Category Theory / Type Theory / Operational Semantics lens panel over only the files changed in a PR, analyzes each lens in isolation, adversarially cross-verifies the findings, and posts the survivors as a single consolidated PR comment. Project-local contributor tooling."
allowed-tools: Bash, Read, Grep, Glob, Task

Formal Lens Review

A one-pass review of a PR diff through a **fixed formal lens panel** — Category Theory ∥ Type Theory ∥ Operational Semantics — posted back to the PR as a single consolidated comment for human reviewers. The panel is **pinned** at definition time rather than derived from the diff, so a formally-structured protocol change gets a meticulous, complete formal review on the same three axes every run.

Why this is a project skill

The formal triple (morphism coherence, type soundness, evaluation-order consistency) is **this repository's** standing review axis — protocol `SKILL.md` files carry category-theoretic formal blocks, `TYPES` / `PHASE TRANSITIONS`, and operational-semantics state machines. Pinning all three here guarantees the formal partial review is exhaustive every run. The fixed panel is therefore project-specific and belongs in the project skill layer. This skill is self-contained — it names its own lenses and describes its own isolated-then-adversarial substrate, with no plugin dependency.

Caller Signature

/formal-review [scope?]

scope : PR number | (implicit)                       -- optional; PR number, or implicit current-branch PR / working-tree detection
                                                     --   absent → Phase 0 detects it

When `scope` is omitted, Phase 0 detects it (current-branch PR, else working tree). The lens panel is fixed in this skill — Category Theory, Type Theory, Operational Semantics — and is not a runtime parameter; the scope is the only argument.

Pipeline Overview

/formal-review [scope?]
  Phase 0  : scope detect (PR number | current-branch PR | working tree) + free-exit — no SHA pinning, tools fetch live
  Phase 1  : diff prep   — fetch diff live (gh pr diff {N} | git diff HEAD); read file fate (A/M/D/R) from diff headers; state diff-reading conventions
  Phase 2  : fixed-lens review (isolated → adversarial) — pin the formal triple (Category Theory ∥ Type Theory ∥ OpSem); substrate described in-skill (not /conduct)
              2a isolated per-lens analysis (independence) — each finding: file:line + lens tag + severity + evidence-grounded rationale, confidence ≥ 80%
              2b adversarial cross-verification — refute each finding; survive → Phase 3, defeated → recorded in the Phase 4 comment as refuted (relay drop w/ basis)
  Phase 3  : direction-error guard (verify) — cross-check review text vs diff-header fate; Added-but-described-as-deleted → warning augment (relay)
  Phase 4  : post comment  — one consolidated PR comment carrying every finding (path:line in text); substrate write → harness permission
  free-exit : user may end the review at any time (declared once in Phase 0)

The skill's identity is the **fixed formal lens panel** applied once over a PR diff and posted back as a single PR comment — a one-pass review for human reviewers, not a convergence loop.

When to Use

• One-pass review of a formally-structured protocol change on this repository's standing formal axes — morphism/type/evaluation-order coherence — every run on the same three lenses
• You want the findings posted back to the PR as a single consolidated comment for human reviewers to consume
• The change touches protocol formal blocks (`TYPES`, `PHASE TRANSITIONS`, `MORPHISM`, `LOOP`, `CONVERGENCE`) where the formal triple is the load-bearing review axis

Phase 0: Scope Detection + Free-Exit

**Scope detection** — the skill runs interactively on the branch, so resolve the scope to a target the tools can fetch live; no base/head SHA pinning is needed:

1. PR number given as `scope`: scope = PR `{N}` 2. No PR argument: `gh pr view --json number 2>/dev/null` to detect a current-branch PR; if found, scope = that PR 3. No PR: scope = working tree 4. No changes anywhere — check with `git status --porcelain` (empty output), not `git diff HEAD`, so an untracked-only working tree is not mistaken for "no changes": report and stop (nothing to review)

**Free-exit affordance (declared once).** Announce here, before the review begins: *"You can end this review at any time by saying so; I will stop and report what has been gathered."* This is a free-response pathway, not a gate option — it does not reappear as a peer option at later phases.

Phase 1: Diff Preparation

Fetch the diff for the resolved scope with your tools — `gh pr diff {N}` (PR scope) or `git diff HEAD` (working tree). The tool resolves the current PR/tree directly, so the diff is the single live source for both file fate and line-level evidence. For a working-tree scope, `git diff HEAD` omits untracked (new, never-added) files; detect them with `git status --porcelain` and read each untracked file's content as added (`new file`) lines so an untracked-only change set is reviewed rather than silently skipped.

Read **file fate** directly from the diff headers — this is authoritative:

• `new file mode` → **Added**: created by this change; the body begins `--- /dev/null` / `+++ b/<path>` and the `+` lines are the file's initial content.
• `deleted file mode` → **Deleted**: removed by this change; the body begins `--- a/<path>` / `+++ /dev/null` and the `-` lines are the prior content removed.
• `rename from <old>` / `rename to <new>` → **Renamed**.
• otherwise → **Modified**.

**Diff-reading conventions**: lines starting with `+` are added; lines starting with `-` are removed; a leading space is