v0.1.0 - first public release

First public release.

dsh-tool-strict-check adds one tool, strict_check, which verifies code and
commands with real checkers instead of with another opinion. An agent that is
confidently wrong does not fix itself by reading the diff again: it wrote the
change, so it agrees with the change.

Four actions, cheapest first

Action	What it runs	What a pass means
status	Probes every checker with --version	What can be checked here, 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 compiler accepted the files
commands	Static rules over shell text, never executed	No known harness-shell hazard matched

The Lean tier is built around two facts

lean file.lean exits 0 on a file full of sorry, because an unfinished
proof is a warning in Lean. A checker that read the exit code would report a
vacuous theorem as verified. So the run is:

lean --json -DwarningAsError=true -DmaxErrors=0 -DautoImplicit=false -E hasSorry spec.lean

-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 is itself an attack surface. Eight kernel and runtime soundness
bugs were found in 2026, each exploited to make the official kernel accept a proof
of False; they were fixed in 4.33.1. The version is checked against that
floor and printed with every result, and an older toolchain turns a pass into
unsafe-toolchain.

A verdict of unavailable means no checker ran and nothing was proved. It is
never returned as a pass.

Install

dsh plugin --profile web add github:catsenior507/dsh-tool-strict-check

Lean is optional; without it the other tiers still work. To add it:
elan toolchain install leanprover/lean4:v4.33.1.

Verified

61 tests (npm test). The parsing tests replay recorded lean --json output
from Lean 4.33.1 — including the detail that positions on the wire are 0-based
and are converted to 1-based — and the integration tests execute the real
compiler.

Lean is optional; the other three tiers work without it. To add it:
elan toolchain install leanprover/lean4:v4.33.1 (4.33.1 is the minimum, not a
suggestion — eight kernel soundness bugs fixed there each allowed a proof of
False). Then restart the host and run strict_check action=status.