git:20260402.5ee41f6 to git:20260402.25614a4

18 added, 130 removed. Audit A to A.

---

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.

---

# Semi-Formal Code Reasoning

- Structured certificate templates that force mandatory checkpoints before conclusions. Based on Ugare & Chandra (2026), validated in our replication experiments.

- ## Core Principle

- These templates are **cognitive forcing functions**. They change what the model thinks about before concluding — not its reasoning ability. Standard chain-of-thought lets pattern-matching to plausible answers. Structured templates insert mandatory scope checks, execution traces, and sufficiency verifications.

- **Value scales with reasoning distance.** Locally-obvious bugs show no improvement. Cross-scope, cross-file, and architectural bugs show dramatic gains (+11pp fault localization in our experiments).

- ## When to Apply

+ Structured certificate templates that force mandatory checkpoints before conclusions. Based on Ugare & Chandra (2026), validated in replication experiments.

- Apply semi-formal reasoning when:

- - Tracing execution across module boundaries or class hierarchies

- - Name shadowing or scope ambiguity is possible

- - A fix might introduce regressions in untouched code paths

- - Comparing two patches for behavioral equivalence

- - Bug symptoms are distant from root cause (cross-file, cross-scope)

+ ## Skip Conditions

- Skip when:

- - Bug is locally obvious (typo, off-by-one in same function)

- - Change is trivial (docs, formatting, version bumps)

+ 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

- ## Model-Tier Considerations

- Template value is model-capability-dependent, not just reasoning-distance-dependent.

- **Smaller models (Haiku-class):** Templates provide the most value. On CVE-2026-29000 (383-line JWT auth bypass), Haiku went from 80% → 100% fault localization with the template (+20pp). The template forces execution tracing that the model wouldn't do unprompted.

- **Larger models (Sonnet-class):** Templates can add overhead on bugs the model already handles. Same CVE, Sonnet scored 100% standard but 80% with the template (-20pp). The structured format consumed tokens that the model would have used for reasoning.

- **Cost optimization:** Haiku + semi-formal ≈ Sonnet standard, at ~1/10th the cost. When using sub-agents for verification (e.g., verify_patch), consider Haiku + template instead of Sonnet + standard prompting.

- **Decision framework:**

- - Bug seems hard (cross-scope, cross-file, architectural) + using a smaller model → apply template

- - Bug seems hard + using a frontier model → apply template (net positive expected)

- - Bug seems tractable + using a frontier model → skip template (overhead may hurt)

- - Cost-sensitive workflow → use smaller model + template

- ## Templates

- Three templates for different tasks. Each follows the certificate pattern: premises → mandatory traces → formal conclusion.

- ### Patch Verification

- For reviewing diffs. Forces function resolution, execution tracing, regression checking.

- **Automated path:** `from muninn_utils.verify_patch import verify_patch` — wraps this template in a sub-agent call with outcome tracking. Use for PR workflows.

- **Direct application:** When reasoning about a patch inline (no sub-agent), follow this structure:

- ```

- PREMISES:

- P1: The patch modifies [what files/functions]

- P2: The intended fix is [what it should do]

- P3: Must not break [existing behavior]

- FUNCTION RESOLUTION:

- For each function call in the patch — trace which definition is actually invoked.

- Check imports, module scope, class scope, builtins. Flag any name shadowing.

- EXECUTION TRACE:

- Before: [input] → [buggy behavior]

- After: [input] → [expected behavior]

- REGRESSION CHECK:

- For each touched code path: [preserved / broken] because [evidence]

- EDGE CASES:

- [Any unhandled scenarios]

- VERDICT: [CORRECT | LIKELY_CORRECT | CONCERNS | BUGGY]

- CONFIDENCE: [high | medium | low]

- SUMMARY: [one sentence]

- ```

- The critical checkpoint: **FUNCTION RESOLUTION**. "Which function is actually being called?" catches name shadowing and import errors that narrative reasoning misses.

- ### Fault Localization

- For finding which line(s) cause a bug. Forces divergence analysis and sufficiency verification.

- ```

- PREMISES:

- P1: The symptom is [what happens]

- P2: The expected behavior is [what should happen]

- CODE PATH TRACE:

- For each relevant line:

- LINE [N]: [what it does] → [result for buggy input]

- DIVERGENCE ANALYSIS:

- For each candidate buggy line:

- CLAIM D[N]: At line [N], [code] produces [behavior]

- which contradicts P2 because [reason]

- VERIFICATION: Would fixing ONLY this line fix the symptom? [yes/no + why]

- BUGGY LINES: [number(s)] — [reason]

- ```

- The critical checkpoint: **"Would fixing ONLY this line fix the symptom?"** Forces sufficiency verification — prevents identifying a line that contributes to the bug but isn't the root cause.

- ### Patch Equivalence

- For determining if two patches produce identical test outcomes. Forces per-test execution tracing for both patches.

- ```

- DEFINITIONS:

- D1: Two patches are EQUIVALENT MODULO TESTS iff the test suite produces

- identical pass/fail outcomes for both patches.

- PREMISES:

- P1: Patch 1 modifies [file(s)] by [change]

- P2: Patch 2 modifies [file(s)] by [change]

- P3: The tests check [behavior]

+ - The task is not code analysis (text editing, data extraction, summarization)

- FUNCTION RESOLUTION:

- For EACH function call in each patch:

- - Trace Python name resolution (local → enclosing → module → builtins)

- - Check for module-level definitions that might shadow builtins

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

- ANALYSIS OF TEST BEHAVIOR:

- For each test:

- Claim 1: With Patch 1, test will [PASS/FAIL] because [execution trace]

- Claim 2: With Patch 2, test will [PASS/FAIL] because [execution trace]

- Comparison: [SAME / DIFFERENT]

+ ## Model-Specific Instructions

- COUNTEREXAMPLE (if different):

- Test [name] → different outcomes because [trace]

+ **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.

- ANSWER: [YES equivalent | NO not equivalent]

- ```

+ **If you are Sonnet-class or above (Sonnet 4.6, Opus):**

+ Read `sonnet.md` in this skill directory. It contains compact verification checkpoints.

- ## Composing Templates

+ ## Composing Tasks

- For complex tasks, compose templates sequentially:

+ 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 template output feeds the next as premises.

+ Each output feeds the next as premises.

## Provenance

- Paper: Ugare & Chandra, "Agentic Code Reasoning with Semi-Formal Certificates" (arXiv:2603.01896, March 2026)

- - Replication: Validated on Django name-shadowing (0%→100% fault localization) and 3 real bugs from private repos (+11pp aggregate)

- - CVE validation: CVE-2026-29000 (pac4j-jwt, CVSS 10.0, 383 lines). Haiku: +20pp with template. Sonnet: -20pp (template overhead). Finding: value is model-tier-dependent.

- - Blog: austegard.com/blog/replicating-agentic-code-reasoning/

+ - 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.