# reasoning-semiformally - Changelog

All notable changes to the `reasoning-semiformally` skill are documented in this file. The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).

## [0.3.1] - 2026-09-09

### Fixed

- repair broken frontmatter, mark obsolete skills, close registry gaps (#746)

### Other

- prompt-audit: dated prompting patterns across the skill catalogue (#791)
- Semi-formal reasoning: model-specific routing (Haiku vs Sonnet) (#524)
- Add model-tier guidance from CVE-2026-29000 experiment (#523)
- Add reasoning-semiformally skill (#522)

# Semi-Formal Code Reasoning (Full Templates)

These templates tell you exactly what to do at each step. Follow them literally. Do not skip steps. Do not summarize — write out each step's result before moving to the next.

## Template 1: Patch Verification

Use when reviewing a diff or proposed fix.

### Procedure

**Step 1: State premises.**
Write exactly three lines:
```
P1: The patch modifies [list every file and function touched].
P2: The intended fix is [one sentence: what the patch should accomplish].
P3: Must not break [one sentence: what existing behavior must be preserved].
```

**Step 2: Function resolution.**
For EACH function call that appears in the changed lines, resolve it using this exact sequence. Write out each sub-step:
1. Is there a local variable or parameter with this name in the current function? If yes → that's what's called. STOP.
2. Is there a definition with this name in the enclosing class? If yes → that's what's called. STOP.
3. Is there a definition with this name at module level (same file, top-level)? If yes → that's what's called. STOP.
4. Is this name imported? If yes → trace the import to its source. That's what's called. STOP.
5. Is this a language builtin? If yes → the builtin is what's called. STOP.
6. If none of the above: flag as UNRESOLVED.

If at any step you find a definition AND a later step would also match (e.g., a module-level function has the same name as a builtin), write: "NAME SHADOWING: [name] at [scope] shadows [what it shadows]."

**Step 3: Execution trace.**
Pick one concrete input that triggers the bug. Write:
```
Before patch: [input] → step-by-step what happens → [buggy result]
After patch:  [input] → step-by-step what happens → [correct result]
```
Keep each trace to 3-5 steps maximum.

**Step 4: Regression check.**
For each function modified by the patch, find one other place in the code that calls it. Write:
```
[caller] calls [modified function] with [typical input] → still produces [expected output]: PRESERVED
```
If you cannot find a caller, write: "No callers found in provided context."
If behavior would break, write: "REGRESSION: [caller] would now get [wrong result] because [reason]."

**Step 5: Edge cases.**
List 1-3 inputs the patch does not handle. If none exist, write: "No unhandled edge cases identified."

**Step 6: Verdict.**
Use this decision rubric:
- BUGGY: Step 2 found unresolved shadowing that changes behavior, OR Step 4 found a regression, OR Step 3 shows the fix doesn't work.
- CONCERNS: Step 5 found edge cases that could fail, OR Step 2 found shadowing that might not affect behavior but is risky.
- LIKELY_CORRECT: All steps passed but the provided context is incomplete (you couldn't trace all callers).
- CORRECT: All steps passed and the context is sufficient to verify fully.

Write exactly:
```
VERDICT: [CORRECT | LIKELY_CORRECT | CONCERNS | BUGGY]
CONFIDENCE: [high | medium | low]
SUMMARY: [one sentence explaining the verdict]
```

### Worked Example: Patch Verification

**Input:** A Django patch that changes `django/utils/text.py` line 42 from `return format(value, spec)` to `return builtins.format(value, spec)`.

**Correct output:**

```
P1: The patch modifies django/utils/text.py, function format_lazy(), line 42.
P2: The intended fix is to call Python's builtin format() instead of the module-level format() function.
P3: Must not break existing callers of format_lazy() who expect standard string formatting.

FUNCTION RESOLUTION:
- format() on line 42 (before patch):
  1. Local variable? No.
  2. Enclosing class? No (this is a module-level function).
  3. Module-level definition? YES — django/utils/text.py defines format() at line 12.
  → NAME SHADOWING: module-level format() at line 12 shadows builtin format().
  → Before patch: line 42 calls the module-level format(), not the builtin.

- builtins.format() on line 42 (after patch):
  1-4. Explicit builtins reference bypasses all scopes.
  5. builtins.format is the Python builtin.
  → After patch: line 42 calls the builtin format(). Shadowing is bypassed.

EXECUTION TRACE:
Before patch: format_lazy("hello {}", "world") → calls module-level format()
  → module-level format() does lazy evaluation wrapping → returns LazyString, not "hello world"
After patch: format_lazy("hello {}", "world") → calls builtins.format("hello {}", "world")
  → builtin format() does string formatting → returns "hello world"

REGRESSION CHECK:
- Other callers of format_lazy(): template rendering in django/template/base.py
  → calls format_lazy() expecting a formatted string → now gets correct string: PRESERVED
- Direct callers of module-level format(): unchanged, not touched by this patch: PRESERVED

EDGE CASES:
- format_lazy() called with no arguments: builtins.format() would raise TypeError. Same behavior as before (module format() also requires arguments). Not a new issue.

VERDICT: CORRECT
CONFIDENCE: high
SUMMARY: Patch correctly bypasses name shadowing by explicitly calling builtins.format().
```

---

## Template 2: Fault Localization

Use when finding which line(s) cause a bug.

### Procedure

**Step 1: State premises.**
Write exactly two lines:
```
P1: The symptom is [what actually happens — the observable bug].
P2: The expected behavior is [what should happen instead].
```

**Step 2: Code path trace.**
Starting from the entry point, trace execution for an input that triggers the bug. For each line that matters, write:
```
LINE [N]: [what the code does] → [result for the buggy input]
```
Maximum 10 lines. Focus on lines where the result is surprising or where behavior diverges from P2.

**Step 3: Divergence analysis.**
For each line that looks suspicious (where the result contradicts P2), write:
```
CANDIDATE LINE [N]: [the code]
  CLAIM: This produces [behavior] which contradicts P2 because [reason].
  SUFFICIENCY TEST: If I fix ONLY this line, does the symptom go away?
    - Yes, because [explanation] → ROOT CAUSE
    - No, because [what else would still be wrong] → CONTRIBUTOR ONLY
```

**Step 4: Output.**
```
BUGGY LINES: [line number(s)]
REASON: [one sentence per line explaining why]
```

### Worked Example: Fault Localization

**Input:** JwtAuthenticator.java (383 lines). Symptom: "Users can gain admin access without proper JWT credentials."

**Correct output:**

```
P1: The symptom is that users with unsigned or plaintext JWTs can bypass authentication and gain admin access.
P2: The expected behavior is that only users with properly signed and verified JWTs can authenticate.

CODE PATH TRACE (for a PlainJWT input — an unsigned token):
LINE 195: jwt = JWTParser.parse(tokenString) → parses successfully, returns PlainJWT object
LINE 198: signedJWT = jwt.toSignedJWT() → PlainJWT has no signature, returns null
LINE 199: if (signedJWT != null) { verifySignature(signedJWT) } → signedJWT is null, skips entire signature verification block
LINE 215: claims = jwt.getJWTClaimsSet() → extracts claims from the unverified PlainJWT
LINE 220: return buildProfile(claims) → builds authenticated profile from unverified claims

DIVERGENCE ANALYSIS:
CANDIDATE LINE 198: jwt.toSignedJWT() returns null for PlainJWT
  CLAIM: Returning null instead of throwing an exception means unsigned tokens silently pass through.
  SUFFICIENCY TEST: If I fix ONLY this line (e.g., throw if null), does the symptom go away?
    - Yes, because unsigned tokens would be rejected here before reaching claims extraction → ROOT CAUSE

CANDIDATE LINE 199: if (signedJWT != null) { verifySignature(signedJWT) }
  CLAIM: The null check skips verification entirely when toSignedJWT returns null.
  SUFFICIENCY TEST: If I fix ONLY this line (e.g., add else { throw }), does the symptom go away?
    - Yes, because the else branch would reject unsigned tokens → ROOT CAUSE

CANDIDATE LINE 215: claims = jwt.getJWTClaimsSet()
  CLAIM: Extracts claims from an unverified token.
  SUFFICIENCY TEST: If I fix ONLY this line, does the symptom go away?
    - No, because the unsigned token was already accepted at line 199. Moving claims extraction wouldn't prevent authentication → CONTRIBUTOR ONLY

BUGGY LINES: 198, 199, 215
REASON: Line 198 returns null for unsigned tokens instead of failing. Line 199 treats null as "skip verification" instead of "reject." Line 215 processes claims from tokens that were never verified.
```

---

## Template 3: Patch Equivalence

Use when determining if two patches produce the same test outcomes.

### Procedure

**Step 1: State premises.**
```
P1: Patch 1 modifies [file(s)] by [what it changes].
P2: Patch 2 modifies [file(s)] by [what it changes].
P3: The tests check [what behavior the tests verify].
```

**Step 2: Function resolution.**
For EACH function call in EACH patch, follow the 5-step resolution procedure from Template 1, Step 2. Write results for both patches.

**Step 3: Per-test analysis.**
For each relevant test, write:
```
TEST: [test name or description]
  Patch 1: [execution trace, 2-3 steps] → [PASS or FAIL]
  Patch 2: [execution trace, 2-3 steps] → [PASS or FAIL]
  Comparison: [SAME or DIFFERENT]
```

**Step 4: Verdict.**
- If ALL tests show SAME → "YES, patches are equivalent modulo tests."
- If ANY test shows DIFFERENT → "NO, patches are not equivalent." Then write:
```
COUNTEREXAMPLE: Test [name] → Patch 1 [PASS/FAIL], Patch 2 [PASS/FAIL] because [trace showing divergence].
```

---

## Common Mistakes to Avoid

1. **Skipping function resolution.** Do not assume a function call refers to the obvious definition. Trace it through the 5-step sequence every time.
2. **Stopping at "contributor."** The sufficiency test ("fix ONLY this line") is mandatory. Finding a suspicious line is not the same as finding the root cause.
3. **Empty regression checks.** "No regressions" is acceptable only after checking at least one downstream caller. If no callers are visible, say so explicitly.
4. **Vague execution traces.** Each step must show a concrete value or state change, not "processes the input" or "handles the request."

# Semi-Formal Code Reasoning

Structured certificate templates for code analysis, based on Ugare & Chandra (2026).

## Provenance

- Paper: Ugare & Chandra, "Agentic Code Reasoning with Semi-Formal Certificates" (arXiv:2603.01896, March 2026)
- Replication: Django name-shadowing (0%→100% fault localization), 3 real bugs (+11pp aggregate)
- CVE validation: CVE-2026-29000 (pac4j-jwt, 383 lines). Haiku: +20pp with template. Sonnet: -20pp with template.
- Finding: Template value is model-capability-dependent. Scaffolding helps weaker models; it becomes overhead for stronger ones.

## Structure

| File | Audience | Purpose |
|------|----------|---------|
| `SKILL.md` | All models | Thin router: skip conditions + model-tier routing |
| `sonnet.md` | Sonnet/Opus | 3 compact verification checkpoints |
| `haiku.md` | Haiku | Full procedural templates with worked examples |

---
name: reasoning-semiformally
description: Apply semi-formal certificate reasoning to code analysis — patch verification, fault localization, patch equivalence. Use when reviewing patches, hunting bugs across scopes, comparing fixes, or when code reasoning requires tracing execution across files/modules. Triggers on code review, bug localization, patch comparison, name shadowing, scope analysis, regression checking.
metadata:
  version: 0.3.1
---

# Semi-Formal Code Reasoning

Structured certificate templates that force mandatory checkpoints before conclusions.

## Skip Conditions

Do NOT apply semi-formal reasoning when:
- The change is trivial: docs, formatting, version bumps, config changes
- The bug is locally obvious: typo, off-by-one in the same function, missing comma
- No execution paths cross scope boundaries
- The task is not code analysis (text editing, data extraction, summarization)

If any skip condition is met, proceed with standard reasoning.

## Model-Specific Instructions

**If you are Haiku-class (Haiku 4.5 or similar):**
Read `haiku.md` in this skill directory. It contains full procedural templates with worked examples.

**If you are Sonnet-class or above (Sonnet 5, Opus):**
Read `sonnet.md` in this skill directory. It contains compact verification checkpoints.

## Composing Tasks

For complex tasks, apply templates sequentially:
1. **Fault localization** to find the bug
2. **Patch verification** to validate a proposed fix
3. **Patch equivalence** to compare alternative fixes

Each output feeds the next as premises.

# Semi-Formal Checkpoints (Sonnet/Opus)

You already reason well about code. These checkpoints catch the specific failure modes where even strong reasoning misses bugs — name shadowing, scope ambiguity, and insufficiency errors.

## Before Any Conclusion

Insert these three checks before delivering a verdict on any code analysis task. Don't template your entire response around them — just verify each one is addressed.

### 1. Function Resolution
For each function or method call in the code under analysis: which definition is actually invoked? Check for name shadowing between local scope, module scope, imports, and builtins. If you can't trace a call to its exact definition, flag it.

### 2. Sufficiency
For fault localization: "Would fixing ONLY this line fix the symptom?" If no, you've found a contributor, not the root cause.
For patch verification: "Does this change fully address the stated problem, or does it fix a symptom while the root cause persists?"

### 3. Regression Paths
For each code path touched by the change: does untouched code that depends on the modified behavior still work? Trace at least one downstream caller.

## Verdict Format

End with exactly:
```
VERDICT: [CORRECT | LIKELY_CORRECT | CONCERNS | BUGGY]
CONFIDENCE: [high | medium | low]
SUMMARY: [one sentence]
```

## When to Expand

If checkpoint 1 reveals actual name shadowing or ambiguous resolution, switch to a full execution trace for the affected paths. The compact format is for verification, not for working through genuinely tangled scope chains.