Formal Review

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 unchanged context.

The diff headers are the authoritative source for file fate and the hunks carry the line-level evidence; both feed Phase 2, and the fate read here is re-used by the Phase 3 direction-error guard.

Phase 2: Fixed-Lens Review (isolated analysis → adversarial cross-verification)

This skill names the parallel perspectives and describes the substrate that analyzes and adversarially verifies them directly — the isolated-then-adversarial arrangement is recorded here in the skill itself. This skill fixes the method — the lines of work, their order, independence, combination, stopping point, and where results go — so the method is not underdetermined and /conduct's AI-guided activation precondition is unmet: not activating it here IS that precondition read, not a shortcut past it. Review only the changed files.

Lens panel. This skill pins the panel to the fixed formal triple every run, so the same three axes are covered on every diff. The fixed lenses are:

• Category Theory — morphism coherence, composition laws, functor consistency
• Type Theory — type-signature soundness, variance, type safety
• Operational Semantics — evaluation order, phase transitions, state consistency

2a — Isolated per-lens analysis (independence-before-contamination). Analyze the changed files through each lens in isolation: every lens forms its findings without seeing the other lenses' findings, so a blind spot or bias in one lens cannot contaminate the others. Substrate realization (recorded here, executed by the substrate): run each lens as an isolated analysis — e.g. an isolated subagent per lens, briefed only with its single lens plus the diff — and collect the per-lens findings independently. Each finding carries:

• File path + line number drawn from the diff (the line must appear in the diff)
• Tag — [Category Theory], [Type Theory], or [OpSem]
• Severity — Critical / Important / Suggestion
• Evidence-grounded rationale — reference the actual changed code; confidence ≥ 80% (drop lower-confidence findings)

2b — Adversarial cross-verification. Once the isolated findings are collected, run a single adversarial pass over the aggregate: each finding is challenged against the other lenses and against the diff evidence — does it survive a refutation attempt, or is it defeated (hallucinated, stale against the actual diff, context-inappropriate, or subsumed by another finding)? Substrate realization: a refutation pass — the main session, a dedicated adversarial subagent, or an independent model — that tries to refute each finding and records survival or defeat with cited basis. Surviving findings proceed to Phase 3; defeated findings do not proceed as surviving findings — they are recorded in the Phase 4 consolidated comment as refuted, with their refutation basis (a relay drop with cited basis, never a silent discard). This is a single verification pass, not a convergence loop — this review stays one-pass.

If the changes are trivial (e.g. version bumps only), state that briefly and skip the full lens sweep and its adversarial pass.