Strict Check
Stop re-reading your own diff. Make a compiler say it is wrong.
A DeepSeek Harness host plugin that adds one tool, strict_check, which verifies
code and commands with real checkers instead of with another opinion.
English · 简体中文
The problem
An agent that is confidently wrong does not fix itself by looking again. The model
wrote the change, so it agrees with the change. Reading the diff a second time
produces the same answer with more words.
The failures that actually cost turns are also the ones that are mechanically
decidable: a file that no longer parses, a shell construct the harness shell
cannot run, a sorry that makes a proof vacuous, a type error three files away.
None of those need judgement. They need a checker.
What it does
One tool, four actions, cheapest first.
| Action | What it runs | What a pass means |
|---|
status | Probes every checker with --version | What can be checked on this machine, and what cannot |
lean | lean --json with warnings promoted to errors | The Lean kernel accepted the proof |
batch | py_compile, node --check, tsc --noEmit, the PowerShell parser | The language's own compiler accepted the files |
commands | Static rules over shell text, never executed | No known harness-shell hazard matched |
The Lean tier is the strict one
A Lean check is worth having only because it can say no. Two things make that
true here, and both are the opposite of the obvious implementation:
A sorry must fail the check. lean file.lean exits 0 on a file full of
sorry, because an unfinished proof is a warning in Lean. A checker that ran
Lean and read the exit code would report a vacuous theorem as verified. So the
exact run is:
lean --json -DwarningAsError=true -DmaxErrors=0 -DautoImplicit=false -E hasSorry spec.lean
-E hasSorry promotes only the missing-proof kind, so "no unfinished goals" is
demanded without demanding "no warnings at all". The kind really is hasSorry,
not sorry.-DmaxErrors=0 removes the default cap of 100, past which Lean stops reporting
and exits — which would hide every error after the hundredth.-DautoImplicit=false closes a footgun that is on by default in Lean: with
it enabled, a misspelled hypothesis name silently becomes a fresh universally
quantified variable, and the theorem states something weaker than it reads.
The checker itself must be trustworthy. In 2026, eight soundness bugs were
found in the Lean kernel and runtime; each was exploited to make the official
kernel accept a proof of False, and they were fixed in 4.33.1. A proof
accepted by an older toolchain is not evidence of anything, so the version is
checked against that floor, is printed with every result, and an older toolchain
turns a pass into unsafe-toolchain.
Everything is honest about not running
A verdict of unavailable means no checker ran and nothing was proved. It is
never returned as a pass. If tsc is missing, the result says so with the path it
looked for; if the resolved lean is the elan shim with no configured default
toolchain, the result says that too instead of reporting a compiler error.
Install
The plugin is installed as a package into a dsh profile. dsh plugin forwards
to pnpm inside the profile directory, so any spec pnpm accepts works.
# from GitHub (the published form)
dsh plugin --profile web add github:catsenior507/dsh-tool-strict-check
# a local checkout, while developing
dsh plugin --profile web add /absolute/path/to/dsh-tool-strict-check
web is the shipped GUI profile; substitute headless, sdk, acp, or your own
profile name. On Windows, use forward slashes in a path.
Then restart the host and confirm with:
strict_check action=status
Lean is optional, and here is how to add it
The other three tiers work without Lean. status reports Lean as missing, and
the lean action returns unavailable — never a pass.
# 1. elan, the Lean version manager
# Windows (the installer writes to %USERPROFILE%\.elan):
Invoke-WebRequest https://elan.lean-lang.org/elan-init.ps1 -OutFile "$env:TEMP\elan-init.ps1"
& "$env:TEMP\elan-init.ps1" -NoPrompt 1 -DefaultToolchain none
# 2. the toolchain. 4.33.1 is the *minimum*, not a suggestion: see above.
& "$env:USERPROFILE\.elan\bin\elan.exe" toolchain install leanprover/lean4:v4.33.1
The plugin finds Lean without any configuration: it looks for a real compiler
under <ELAN_HOME>/toolchains/*/bin first and only then falls back to PATH. It
does this deliberately — the elan shim on PATH refuses to run until
elan default has been executed once, and that refusal is easy to misread as
"Lean is broken". To pin a specific toolchain, set leanPath in the plugin row.
Behind a proxy? elan downloads through curl, which reads
~/.curlrc. If the toolchain download stalls at 0 bytes while a browser works,
write proxy = "http://127.0.0.1:<port>" into %USERPROFILE%\.curlrc and retry.
What install does not do
- No build step — the published JavaScript is the source; no
prepare script
runs, no bundler is needed.
- No dependencies —
dependencies and peerDependencies are empty. Cordis is
provided by the host at runtime.
- No mathlib — see below for what that costs.
Node.js 20 or newer.
What it does not do
Stated plainly, because a verification tool that oversells itself is worse than
none:
- No mathlib. Core
Init and Std ship with the toolchain, so import Std
and by decide work with no project, no network, and no ~10 GB download. What
you lose is the tactic library: no ring, norm_num, push_neg, field_simp.
Substitutes are grind, decide, by_cases, simp, omega.
- No sandboxed re-check.
lake check, comparator, and nanoda need Linux
namespaces (bwrap) and cannot run on Windows at all. leanchecker re-checks
what the kernel already checked and does not catch sorry, so wrapping it would
be cost without coverage. Lean 4.35 is expected to ship lake check; that is the
right moment to adopt it, not now.
- No statement-vs-intent check. The kernel verifies that the proof proves the
theorem. Whether the theorem is the one you meant is a specification question,
and this tool will not pretend otherwise — which is exactly why the
commands
action prints "a clean scan is weak evidence" rather than "OK".
Configure
dsh plugin add already inserted the plugin row. To change the defaults, edit
that row's config in the profile's cordis.patch.yml:
- insert:
- id: tool-strict-check
name: '@dsh-external/dsh-tool-strict-check'
config:
leanPath: '<ELAN_HOME>/toolchains/<toolchain>/bin/lean.exe'
projectDir: '<path to a Lake project, if your specs import one>'
timeoutMs: 120000
leanPath wins over discovery, which is what pins one toolchain.
Development
npm test # 61 tests; the Lean ones execute the real compiler
The Lean integration tests are skipped, not faked, when no safe toolchain exists.
Parsing tests replay recorded lean --json output from Lean 4.33.1, so they
fail if the wire format changes — including the detail that positions on the wire
are 0-based and are converted to 1-based.
| File | Role |
|---|
lib/runner.js | Executable discovery, bounded process execution, spawn-failure handling |
lib/parse.js | Checker output to normalized diagnostics |
lib/static.js | Defects and policy violations decidable by reading |
lib/language.js | Tier 0: the language's own compiler |
lib/lean.js | The strict tier: flags, version floor, verdict |
lib/tool.js | The strict_check tool |
lib/policy-surface.js | The contract dsh-policy-strict-gate consumes |
License
MIT
