crosscheck

Orchestrator for formal verification and semi-formal code reasoning. Classifies tasks, routes to appropriate verification or reasoning skills, and validates output quality. Use for any formal verification, structured code reasoning, fault localization, patch comparison, or specification management task. Named after Dustin Byfuglien — the crosschecking enforcer.

Scan the spec registry for verified Dafny specs whose associated source files have changed. Re-verify affected specs and report which properties still hold. Use for regression detection after code changes, pre-commit checks, or spec maintenance. Triggers: "check regressions", "did my changes break specs", "re-verify", "spec status", pre-commit review.

Determine whether two code patches are semantically equivalent by tracing execution through the test suite using semi-formal reasoning. Produces a structured proof of equivalence or a specific counterexample. Triggers: "compare patches", "are these equivalent", "same behavior", "diff comparison".

Compile verified Dafny to Python or Go with Dafny runtime boilerplate stripped. Presents clean output ready for project integration, with type mappings and property-based test suggestions. Use after /generate-verified produces a verified implementation. Triggers: "extract to python", "extract to go", "compile dafny".

Generate a Dafny implementation body that satisfies a verified spec. Iteratively adds proof hints, loop invariants, and lemmas until the verifier accepts. Use after /spec-iterate produces an approved spec. Triggers: "implement the spec", "generate verified code", "prove the implementation".

Generate lightweight verification artifacts for functions where full formal verification is overkill: design-by-contract assertions, property-based tests, and documented runtime invariant checks. Use for simple transformations, CRUD, concurrency, or floating-point code that Dafny cannot verify. Triggers: "lightweight verify", "add contracts", "property-based tests", "assertions".