Find logic bugs through semi-formal execution tracing

A Logic-Lens skill for logic review: finding logic bugs in a single file or function via semi-formal execution tracing structured as Premises, Trace, Divergence, Trigger, Remedy. It triggers on phrases like "review this" or "does this look right" when a user shares code and suspects something is wrong without naming a concrete failure. The downstream grader, scripts/grade-iteration.py, and sibling Logic-Lens skills consume the report by substring-matching literal field labels defined in common.md - paraphrasing those labels, even with a synonym that reads fine to a human, breaks the contract regardless of analysis quality. Three specific failure modes are called out: synonym substitution for field labels (replacing Premises/前提 with 前置条件构建, or Divergence/偏差 with 根因/核心缺陷) that grader and cross-skill consumers treat as a missing field entirely; demoting a confirmed L-code finding to an "Additional observation" section instead of keeping it inside ## Findings with the five literal fields even at Suggestion severity; and omitting the Divergence: field entirely by writing the divergence as prose or under headings like 根因/故障点 instead of the literal required label, which has no acceptable synonym - no-bug findings use Divergence: None - [why the premise holds].

The process runs nine steps. Step 0 detects language and confirms scope is one file or function, routing to logic-health for a directory, logic-locate for a confirmed failure, or logic-diff for two versions. Step 1 states claimed behavior and selects entry points to trace. Step 2 builds premises including caller/callee contracts. Step 3 builds a risk-path ledger across L1 through L9 categories before writing findings, tagging each path Class A (self-evident) or Class B (invariant-dependent), with detailed disambiguation rules between adjacent L-codes: L4 (single-context mutation of aliased/shared state) versus L7 (any access across thread/goroutine/await/yield boundaries, even single-threaded asyncio interleaving); L1 (name resolving to a different definition than expected, e.g. import shadowing, constructor-scoped const/let) versus L6 (name resolves correctly but callee behavior differs from assumption); L2 (implicit type coercion at the operator level) versus L6 (specific callee behavior mismatch); L5 (single-context error suppression like || true or empty catch) versus L7 (multi-context); and L9 (timezone/locale/encoding lost at the data-type level, e.g. TIMESTAMP vs TIMESTAMPTZ, naive vs aware datetime). Step 4 deep-traces selected paths, resolving every name and type and crossing callee boundaries; for Java/C++ double-checked locking it mandates tracing both the missing-volatile visibility hazard and the non-atomic instance-then-init publish-before-init hazard, reporting both. Step 5 classifies divergences and applies a reachability gate requiring a probe for design-intent questions. Step 5.5 runs an Adversarial Red Team pass, disproving each candidate finding via premise/path/consequence rebuttal questions, withdrawing confirmed defenses and downgrading partial defenses to Suggestion - including a design-intent gate that withdraws L3 Boundary Blindspot findings when code explicitly returns an error at the boundary (e.g. "cache full", 429 Too Many Requests) rather than silently failing past it. Step 6 applies the Iron Law five-field discipline, requiring literal Premises:/Trace:/Divergence:/Trigger:/Remedy: labels (or Chinese equivalents) per finding, rejecting substitute headers like "Execution Path" or "Core Defect". Step 6.5 mentally dry-runs the Remedy against the Trigger input to confirm the divergence is eliminated with no regression. Step 7 computes and emits the literal line **Logic Score:** XX/100 directly under Scope. Step 8, optional, generates a minimal reproducer script per Critical/Warning finding when a runtime is available, executes it to confirm the bug, applies the Remedy, and re-executes to confirm the fix, marking verified findings Execution-verified. The mode line reads "Logic Review" (逻辑审查 in Chinese), and even a zero-divergence result must emit the full template skeleton with Logic Score 100/100 and a Divergence: None finding rather than collapsing into free-form prose.

Use it when a user shares a single file or function and suspects something is wrong without naming a concrete failure. Route to logic-health instead for a whole directory, to logic-locate for a confirmed failure, or to logic-diff when comparing two versions.

Input is one file or function plus, implicitly, its claimed behavior. Output is a full report: Mode line, Scope, a literal **Logic Score:** XX/100 line, and a ## Findings section where every finding - Critical, Warning, Suggestion, or No Bug - carries all five literal fields (Premises, Trace, Divergence, Trigger, Remedy), classified by L-code, with Execution-verified marked when Step 8 confirms it via a reproducer script.

Part of the Logic-Lens skill family, sharing ../_shared/common.md, ../_shared/logic-risks.md, ../_shared/semiformal-guide.md, ../_shared/semiformal-checklist.md, and ../_shared/report-template.md with sibling skills logic-diff, logic-locate, and logic-explain, and consumed downstream by scripts/grade-iteration.py, which substring-matches its literal field labels.

Developers who suspect a logic bug in a specific file or function without a confirmed failure to reproduce, and need a rigorous, gradable, L1-L9-classified trace rather than a free-form code review.