Find logic bugs through semi-formal execution tracing

Logic Review examines a single file or function using semi-formal execution tracing. It connects claimed behavior to concrete entry points, establishes premises, enumerates risky paths, traces execution, identifies divergences, and proposes a remedy. Each conclusion must expose the reasoning needed to distinguish an actual failure from an intentional or correctly defended behavior.

A risk-path ledger precedes the findings. Candidate paths are classified as self-evident Class A or invariant-dependent Class B, and analysis covers normal execution plus high-risk edges. Traces resolve names and types, cross relevant callee boundaries, and end at a confirmed divergence or safe post-condition. Caller and callee contracts belong among the premises when local dependencies affect the result.

Use this skill when someone suspects a logic problem but has not supplied a confirmed failure, and the scope is one file or function. Directory-wide assessment belongs to logic-health, a known failing behavior belongs to logic-locate, and comparison of two versions belongs to logic-diff. State a selected subset when a file exceeds the supported scope.

Do not import or execute the reviewed program merely to trace it. Optional runtime verification is a separate controlled step using a minimal reproducer. The Logic Score summarizes confirmed findings within the declared scope; it is uncalibrated and is neither a correctness probability nor merge authority.

Inputs are the code, its claimed behavior, selected entry points, language, and relevant contracts. Outputs are structured findings with the literal labels Premises:, Trace:, Divergence:, Trigger:, and Remedy: at the start of lines inside every finding block. A descriptive heading or a shared preamble cannot replace these per-finding fields, and confirmed findings remain inside Findings even at Suggestion severity.

The report uses the mode line Logic Review, declares Scope, and places the literal Logic Score label directly below it. Headers and field labels follow the user's language using the prescribed tokens. A no-bug result still includes Findings and all five labels, with an explicit absence of divergence and the defense explained in Trace. Its non-reproduction field can be:

Trigger: N/A (no bug to reproduce).

A no-divergence report uses 100/100 while retaining the traced scope and qualifications. Critical and Warning findings require concrete triggering inputs. The remedy should be paste-ready, then mentally retraced against that input to check that the divergence disappears, the happy path remains valid, and no regression is introduced.

Classification uses L1-L9 with important distinctions. Single-context mutation of shared or aliased state is L4; intentional in-place APIs are valid. State interactions across threads, goroutines, await, or yield are L7, including interleaved single-threaded coroutines. Scoping and unexpected name resolution are L1, while N+1 query inefficiency is L3.

Operator-level implicit coercion and casts bypassing runtime checks are L2. L6 concerns a correctly resolved callee behaving differently from the caller's assumption. Sequential suppression of errors or exit statuses is L5 rather than L7. Timezone, locale, or encoding information lost at the data-type level is L9.

For Java or C++ double-checked locking, trace both missing visibility barriers and publication before a separate initialization completes. Addressing only one hazard leaves the analysis incomplete.

Class B candidates require a reachability probe: a discovered invariant enforcement removes the candidate; absent enforcement retains its severity; partial enforcement limits it to Warning with manual verification recommended. An adversarial pass then challenges premises, paths, and consequences. Confirmed defenses withdraw findings; partial defenses reduce them to Suggestion. Deliberate boundary error returns are not L3 blindspots, while attempts to continue beyond a boundary and crash, loop, or silently fail remain candidates.

The skill serves focused code reviewers who need auditable findings and explicit false-positive checks. Optional execution verification reproduces a Critical or Warning finding, applies the remedy, and reruns it, withdrawing false positives.

The grader, shared header map, report template, risk tables, and additional step guides are external prerequisites rather than bundled assets. Obtain and inspect the actual upstream installation before invoking its grader or claiming template compatibility. Inline five-field guidance supports an independent review, but full score calculation and cross-skill compatibility require those supporting files. The upstream project uses the MIT License.