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 plus a gap scan 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, Skill
skills:
  - prothesis:frame
  - syneidesis:gap
---

# Formal Lens Review

A one-pass review of a PR diff through a **fixed formal lens panel** — Category Theory ∥ Type Theory ∥ Operational Semantics — plus a gap scan, posted back to the PR as a single consolidated comment for human reviewers. This is the project-local specialization of the general, frame-driven `/lens-review` (epistemic-cooperative): that skill lets `/frame` derive whatever lenses fit the diff, whereas this skill **pins** the formal triple on every run so a formally-structured protocol change gets a meticulous, complete formal review on the same three axes each time.

## 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. `/frame`, run generically, is unlikely to select all three formal lenses at once on a given diff; pinning them here guarantees the formal partial review is exhaustive every run. The fixed panel is therefore project-specific and belongs in the project skill layer, while the general frame-driven pipeline stays in the `/lens-review` plugin. This skill is self-contained — it composes `/frame` and `/gap` but does not depend on the `/lens-review` plugin skill being installed.

## 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, plus gap scanning — and is not a runtime parameter; the scope is the only argument. (For a diff-derived, non-fixed panel, use the general `/lens-review` instead.)

## 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) via /frame + /gap; 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 — plus a gap audit, 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)

`/frame` forms the parallel perspectives; this skill then describes the substrate that analyzes and adversarially verifies them **directly** — the isolated-then-adversarial arrangement is recorded here in the skill itself. Review **only the changed files**.

**Lens framing.** Call `/frame` (prothesis) to frame the perspectives and `/gap` (syneidesis) for the gap audit. Unlike the general `/lens-review`, this skill **pins** the panel: `/frame` is framed onto the fixed formal triple every run, never a diff-derived selection. The fixed lenses and gap dimensions 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
- **Gap Scanning** (via `/gap`) — scan decision points in the diff for unnoticed gaps:
  - **Procedural** — missing steps or incomplete workflows
  - **Consideration** — unaddressed trade-offs
  - **Assumption** — implicit assumptions needing explicit statement
  - **Alternative** — unexplored approaches

**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]`, `[OpSem]`, or `[Gap: <type>]`
- **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.

## Phase 3: Direction-Error Guard (Verify)

Before posting, cross-check the review text against the file fate read from the diff headers in Phase 1. For each **Added** file, if the review describes it as deleted, that is a likely diff-direction inversion — the reviewer read the diff backwards. Surface a warning that augments the review (it does not replace the findings): a direction-misread notice listing each Added-but-described-as-deleted file, advising verification against the diff headers before treating those findings as legitimate.

This is a relay verify step — a deterministic cross-check of the review text against the authoritative diff-header fate, presented and proceeded through; it does not gate.

## Phase 4: Post the Consolidated Comment

Post the findings back to the PR as a **single consolidated comment** — one comment carrying every finding, not one inline comment per diff line. This is a **substrate write** — an external, human-visible GitHub mutation — so it routes to the **harness permission layer**: surface what will be posted (the consolidated comment body) and let the harness gate the execution. The skill does not absorb that decision.

`call` one comment via `gh api repos/{owner}/{repo}/issues/{N}/comments` with `body` (`{owner}` and `{repo}` are gh's repo placeholders, auto-filled from the current repo; the bare `repos/{repo}/...` form drops the owner segment and resolves wrong). The body lists every finding as text, each referencing its `path:line` so a reviewer can navigate to it — no inline line-targeting API is used, so no `commit_id` / `path` / `line` / `side` machinery is needed.

Posting discipline:

- Consolidate all surviving findings into the one comment body; defeated findings (Phase 2b) go in a clearly-labelled **refuted** section of the same comment, each with its refutation basis — recorded as already-refuted, not presented as actionable, so a human reviewer cannot mistake them for live findings.
- Each finding line carries its `path:line`, the lens tag (`[Category Theory]` / `[Type Theory]` / `[OpSem]` / `[Gap: <type>]`), and the severity (Critical / Important / Suggestion).
- Skip duplicate or near-duplicate findings.
- Write the Markdown comment body through a file (e.g. a heredoc to a temp file), then build the JSON request body from that file with `jq --rawfile` (so the body becomes `{"body": "<markdown>"}`) and feed that JSON to `gh api` via `--input -`; do not pass the Markdown body inside a double-quoted shell argument, because backticks in Markdown trigger shell command substitution, and do not `--input` the raw Markdown file directly because the endpoint requires a JSON object. (`--input` makes `gh api` default to POST, so the comment is created, not listed.)

If the scope is a working tree (no PR), there is no PR to post to — present the findings in session text instead and note that posting requires a PR.

## Rules

1. **Fixed formal panel** — the lenses are pinned to Category Theory, Type Theory, and Operational Semantics every run; `/frame` is framed onto this triple, not a diff-derived selection. A diff-derived panel is the general `/lens-review`, not this skill.
2. **Changed files only** — review the files in the Phase 1 diff and nothing else; the diff headers are authoritative for file fate, the hunks for line-level evidence.
3. **Isolated lenses, then adversarial cross-verification** — each lens forms its findings in isolation (independence-before-contamination); the aggregated findings then pass a single adversarial refutation pass before posting. Surviving findings proceed; defeated findings are recorded in the consolidated comment as refuted with cited basis. The isolated-then-adversarial substrate is described in this skill directly.
4. **Confidence ≥ 80%** — only report findings at or above the confidence threshold; trivial changes (e.g. version bumps) are stated briefly and skipped rather than padded with low-value findings.
5. **Verify before post** — run the Phase 3 direction-error guard against the diff-header fate before any comment is posted; an Added-but-described-as-deleted file augments the review with a direction-misread warning.
6. **Substrate writes route to harness permission** — posting the consolidated PR comment is an external, human-visible GitHub mutation; surface what will be posted and let the harness gate the execution. The skill does not absorb that substrate decision.
7. **Context-question separation at gates** — present all analysis and evidence as text before any gate; a gate carries only the question and the options with their differential implications.
8. **Plain everyday language** in all user-facing emit — no internal protocol jargon at the user-facing surface.
9. **One consolidated comment** — all surviving findings go in a single PR comment, each referencing its `path:line` in text; preserve lens tags and severity on every finding; skip duplicates.