Issues

• Run dafny_verify, dafny_compile and the Lean tools with the sandbox flags dafny_evidence uses

  nicholls-inc/crosscheck#94 · Filter by author hnipps opened on Oct 7, 2026

• CGV: decide whether bool is accepted where int or float is required

  nicholls-inc/crosscheck#86 · Filter by author hnipps opened on Oct 6, 2026

• The Dafny specs under crosscheck/mcp-server/specs do not verify

  nicholls-inc/crosscheck#81 · Filter by author hnipps opened on Oct 6, 2026

• Wire /generate-verified to emit an evidence record with dafny_evidence

  nicholls-inc/crosscheck#80 · Filter by author hnipps opened on Oct 6, 2026

• CGV bench: add cases for the type checker patterns of #10, and keep the README table current

  nicholls-inc/crosscheck#74 · Filter by author hnipps opened on Oct 6, 2026

• CGV: reject implemented_by / extern on constants the soundness theorems reach

  enhancement
  nicholls-inc/crosscheck#48 · Filter by author hnipps opened on Sep 29, 2026

• CGV CI: replay the Lean kernel so skipKernelTC declarations cannot pass the axiom check

  enhancement
  nicholls-inc/crosscheck#47 · Filter by author hnipps opened on Sep 29, 2026

• Prove extraction: close the untrusted gap between Python source and the checked graph

  nicholls-inc/crosscheck#16 · Filter by author hnipps opened on Sep 29, 2026

• README: state what the tool is for relative to type checkers, and qualify the exit-0 claim

  nicholls-inc/crosscheck#10 · Filter by author hnipps opened on Sep 29, 2026
  2

• Hide missing-guarantee warnings by default and report them as coverage per module

  nicholls-inc/crosscheck#9 · Filter by author hnipps opened on Sep 29, 2026

• Give each error a checkable witness: concrete value or generated failing test

  nicholls-inc/crosscheck#8 · Filter by author hnipps opened on Sep 29, 2026

• Baseline / diff mode: report only findings a change introduces

  nicholls-inc/crosscheck#7 · Filter by author hnipps opened on Sep 29, 2026

• Extractor gaps that turn real nullability bugs into warnings

  nicholls-inc/crosscheck#6 · Filter by author hnipps opened on Sep 29, 2026

• Reduce false-positive errors: numeric tower, object params, NoReturn, narrowing, pydantic validation

  nicholls-inc/crosscheck#5 · Filter by author hnipps opened on Sep 29, 2026

• Auditor: write a rerunnable record next to the report, at one decided path

  enhancement
  nicholls-inc/crosscheck#19 · Filter by author fabricator-nicholls opened on Jun 1, 2026

• Auditor: never report settled for an artefact the auditor could not check

  enhancement
  nicholls-inc/crosscheck#20 · Filter by author fabricator-nicholls opened on Jun 1, 2026

• lowry: enter the loop when any D2 gate is red, not only the build

  bug
  nicholls-inc/crosscheck#21 · Filter by author fabricator-nicholls opened on Jun 1, 2026

• ADD acceptance oracles: no LLM judge as a pass condition

  enhancement
  nicholls-inc/crosscheck#22 · Filter by author fabricator-nicholls opened on Jun 1, 2026

• ADD Step 0: choose the operating mode with a pure function of repository state

  enhancement
  nicholls-inc/crosscheck#23 · Filter by author fabricator-nicholls opened on Jun 1, 2026

• Conformance AUTO 5: read the routing forms that documented() accepts, and agent-to-agent edges

  enhancement
  nicholls-inc/crosscheck#24 · Filter by author fabricator-nicholls opened on Jun 1, 2026

• Invariant headings: one grammar for the gate, the templates and the real docs

  bug
  nicholls-inc/crosscheck#26 · Filter by author fabricator-nicholls opened on Jun 1, 2026

• AD-1: review the imported Crosscheck backlog against the vision

  enhancement
  nicholls-inc/crosscheck#27 · Filter by author hnipps opened on May 30, 2026
  2

• add-orchestrator: state when ADD pays for itself

  documentation
  nicholls-inc/crosscheck#28 · Filter by author fabricator-nicholls opened on May 15, 2026

• add-orchestrator: name the modules to probe before probing, for a person to confirm

  nicholls-inc/crosscheck#29 · Filter by author fabricator-nicholls opened on May 15, 2026

• add-orchestrator: retrofit Invariant comments only where a mutant shows the test checks the invariant

  nicholls-inc/crosscheck#30 · Filter by author fabricator-nicholls opened on May 15, 2026