dsh-tool-strict-check

An agent that re-reads its own diff gets a longer version of the same mistake. The failures that actually burn turns—a file that no longer parses, a shell construct the harness shell cannot run, a sorry hiding in a Lean proof, a type error three files away—are mechanically decidable. They do not need judgement; they need a compiler.

strict_check hands the work to each language's own checker. The batch tier runs py_compile, node --check, tsc --noEmit, and the PowerShell parser. The commands tier applies static rules over shell text without ever executing it. Status probes what is available on the machine and reports honestly. The most rigorous tier is Lean: hasSorry promotes unfinished goals to failure, -DmaxErrors=0 lifts the default hundred-error cap, -DautoImplicit=false closes the footgun where a misspelled hypothesis silently becomes a fresh universally quantified variable, and the toolchain version is anchored at 4.33.1 because eight soundness bugs before that release each allowed the kernel to accept a proof of False. When a checker is missing, the result says unavailable and prints the path it looked for; it never disguises an unverified file as a pass.

Built for developers working in DeepSeek Harness who write multi-language code or Lean proofs and want every agent output adjudicated by a real compiler rather than by the model re-reading its own words.