Compare two code versions for semantic equivalence

A Logic-Lens skill for semantic diffing: comparing two code versions side-by-side via semi-formal tracing to confirm whether behavior is unchanged after a refactor, rewrite, migration, or A/B implementation. It uses lazy loading of shared reference docs (common.md for language, Iron Law, Verdict header, scope routing, and config; logic-diff-guide.md loaded step by step; logic-risks.md, semiformal-guide.md, semiformal-checklist.md, and report-template.md loaded on demand) to keep context usage low. The process runs eight steps: Step 0 detects language and confirms two versions are provided, falling back to logic-review if only one version exists. Step 1 identifies the shared specification - what inputs and outputs both versions should handle - and records any user-declared intentional behavior change as a declared spec change, so divergences within that stated area are treated as expected rather than flagged. Step 2 builds independent premises for each version separately using the Premises Construction Checklist. Step 3 traces both versions in parallel on the common case, noting the first point of divergence. Step 4 traces boundary cases - empty/null/zero, max/min, error inputs, first/last of collections - starting with at most three highest-risk scenarios unless the user asks for exhaustive equivalence. Step 5 classifies each semantic divergence as a finding with the five-field format: Premises, Trace, Divergence, Trigger, Remedy, plus an L-code. Step 6 issues an equivalence verdict: Semantically Equivalent, Conditionally Equivalent (with the condition stated precisely), or Semantically Divergent. Step 7 outputs the Report Template with the Verdict header, localizing headers if the user wrote in Chinese. The mode line in the report reads "Semantic Diff" (语义对比 in Chinese). Formatting is mandatory even for trivially short snippets - every divergence finding must use all five labeled fields, never a plain paragraph or table.

Use it when comparing two code versions for semantic equivalence after a refactor, rewrite, migration, or A/B implementation - the trigger phrases are "did I break anything", "is this equivalent", or similar. Switch to logic-review instead if only one code version is provided rather than two.

Input is two versions of code plus, optionally, a user-declared statement of intentional behavior changes. Output is a structured equivalence report: an Equivalence Verdict line, and for each divergence found, a finding block with Premises, Trace, Divergence, Trigger, and Remedy fields plus an L-code classification.

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-review, logic-locate, and logic-explain, and handing off to logic-review when only one version is available.

Developers who need rigorous confirmation that a refactor, migration, or rewrite preserves behavior - not just a visual diff, but a semi-formal trace of both versions against boundary cases before signing off on equivalence.