dsh-tool-strict-check

Agent 写完代码再回头看一遍 diff，得到的只是更长的同一份错误。真正浪费轮次的失误——文件不再可解析、shell 语法不被宿主壳执行、Lean 证明里藏着一个 sorry、三个文件之外的一条类型错误——本质上是机械可判定的，不需要判断力，需要的是编译器。

strict_check 把这件事交给各语言自己的检查器：batch 层跑 py_compile、node --check、tsc --noEmit 和 PowerShell 解析器；commands 层用静态规则扫描 shell 文本，绝不执行；status 层探测本机有哪些检查器可用。最严格的是 Lean 层：通过 hasSorry 把未完成目标提升为失败、-DmaxErrors=0 取消默认百条上限、-DautoImplicit=false 堵住拼错假设名却静默变成全称量词的陷阱，并把工具链版本锚定在 4.33.1 之上——因为 2026 年在该版本前共修复了八个可让内核接受 False 证明的 soundness 漏洞。检查器缺失时结果报告 unavailable 并说明查找路径，绝不把未验证包装成通过。

适合在 DeepSeek Harness 中写多语言代码或 Lean 证明的开发者：你希望 agent 的每一次输出都经过真实编译器的裁决，而不是再读一遍自己写下的文字。