Models write fluent code and confident answers. Fluent isn't proven.
I build the deterministic tools that check — exact math, formal specifications, reproducible evidence —
so what an AI produced can be verified instead of trusted.

copyleftdev.github.io · dev.to · linkedin · don@codetestcode.io

Ask a TLA+ specification about a state, and get an answer. A parser and evaluator for TLA+ in Rust — not a model checker. Hand it a trace from production or a step from your implementation, and it tells you whether the spec permits it, and which conjunct refused it.

$ tlatools check job.json
no action of the specification takes [...] to [...]. The closest was
`BecomeLeader(c = "s1")`, which was not available here:
`Cardinality(votesGranted[c]) * 2 > Cardinality(Server)` does not hold
(3 of its 4 conjuncts hold)

Reads 1,256 of 1,258 specifications across three public TLA+ corpora; the two it rejects, SANY rejects too. No JVM. cargo install tlatools

Writing on it: Vibe Coding with Intent · Vibe Was Never the Problem · A Vibe Is Not a Verdict

Systems engineer on GitHub since 2008, Rust-first with production work in Zig, Go, Python and TypeScript. My background is testing and security research, which is where the habit comes from: a claim isn't done until something other than its author can check it. Everything ships as a small single binary with minimal dependencies, and the gate is mutation testing, not coverage.

_{This section and the metrics panel above are regenerated nightly by a stdlib-only Python script querying the GitHub API — no third-party stats services, nothing to go stale.}