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
Flagship: tlatools-rs
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
| Repository | What it makes checkable |
|---|---|
| agent-calc | An agent's arithmetic — exact, typed JSON math instead of a model's guess at a number |
| solve-score | Exploit-difficulty scoring — an independent SOLVE v0.5 implementation that reproduces all 16 published calibration assessments |
| anomalyx | Anomaly claims — contract-first detection across ~30 log, network and data formats; deterministic, mutation-tested |
| whatthediff | Drift across N files — consensus, outliers and variant families, every finding backed by evidence |
| entropyx | A codebase's history — a forensic instrument for who changed what, how, and how it is holding up |
| vajra | Structured data — deterministic reduction that breaks the noise and preserves what's true |
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.
| Repository | Description | Lang | Last push |
|---|---|---|---|
| leet-index | Activity-aware rankings for US-based GitHub developers, with transparent scoring and… | 2026-10-28 | |
| copyleftdev.github.io | Canonical, self-regenerating identity page for copyleftdev — schema.org Person, llms.txt, and… | 2026-10-27 | |
| vulngraph-data | Deterministic data pipeline for VulnGraph — ingests 11 vulnerability sources, publishes… | 2026-10-27 | |
| poise-rs | Composable, rigorously verified load-balancing primitives for Rust | 2026-10-26 | |
| kilo-data | Open threat-intelligence and IP-reputation ETL for phishing and abuse screening, with BGP and… | 2026-10-26 | |
| braess-router | Bounded semantic routing with Jev and Poise. Rust, single-server, alpha. | 2026-10-25 |
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.
Everything else — security tooling, systems utilities, agent infrastructure, and the absurd
Security & Detection
| Repository | Description | Language |
|---|---|---|
| floq | C2 beacon detection via Floquet spectral analysis — pcap, live capture, or OTLP; 274 KB binary | |
| fatt | Distributed async scanner for exposed files across millions of domains | |
| fuf | Fast next-generation web fuzzer | |
| robin-smesh | Decentralized dark web OSINT framework — Tor crawling, artifact extraction | |
| mini-shai-hulud-dragnet | Forensic dataset + live dashboard for the 2026 npm supply-chain worm — 1,117 dropbox repos, 47 IOCs |
Systems & Developer Tools
| Repository | Description | Language |
|---|---|---|
| tailx | Live system cognition engine — tail reimagined: anomalies, traces, structured JSON; 144 KB |
|
| coelacanth | AI-first Unix primitives, clean-room reimplemented under one machine-checkable contract | |
| palimpsest | Deterministic crawl kernel — same seed, identical crawl; JA3/JA4 impersonation, WARC++ | |
| hook-bin | Single-binary webhook inbox — embedded SQLite, live dashboard, zero deps | |
| zgrok | Self-hosted ngrok alternative built on Tokio | |
| cora | Multi-pattern fixed-string matcher — Aho-Corasick + SIMD on mmap'd files, NDJSON output |
AI & Agent Infrastructure
| Repository | Description | Language |
|---|---|---|
| smesh-rust | Decentralized coordination protocol for multi-agent LLM systems — QUIC P2P, sub-µs signal diffusion | |
| sigmos | DSL for defining AI-native, composable, reactive systems | |
| mcp-flow | WebTransport binding for MCP — QUIC streams, no head-of-line blocking | |
| toon-zig | TOON (Token-Oriented Object Notation) — 30–60% token reduction for LLMs |
Education & the Absurd
| Repository | Description | Language |
|---|---|---|
| humanlang | Token bucket rate limiter implemented in 37 languages (1957–2016) | |
| git-archaeology-lab | Hands-on exercises for forgotten git commands — crafted history, real bugs, real bisect targets | |
| gitfoo_episode_1 | Git Black Belt Masterclass — the other 90% of git most devs never use | |
| OverHelloWorld | Intentionally over-engineered Hello World — DDD, CQRS, event sourcing, telemetry | |
| fafoaas | FAFO as a Service — spec-first engineering masterclass; AsyncAPI 3 + MCP, 98/98 mutation score | |
| tip-to-tip-efficiency | Mathematically serious crate for a deeply unserious Silicon Valley efficiency empire |
If any of this saved you time, you can fund the compute behind it — tips become AI inference credit.
