The books

• All the Ways It Can Break — a progressive working route through TLA+, TLC, Apalache, Alloy, Stateright, Kani, and Loom. Every tool begins from a blank project, exposes a deliberate failure, repairs it, and ends with an unlike transfer. Growing — the conceptual foundation is published.

• Before the Machine Acts — nine executable workshops on formal modeling for web security, concurrency, distributed storage, and agent control systems. Each workshop includes checked source, a command, a known defect, a repair, practice, and a worked answer. Budding — executable workshop edition.

• Hidden Machines — twenty-one compact chapters on recovering the formal structures already implicit in fragile code: alternatives, machines, identity, lifetimes, deltas, convergence, protocols, geometry, and the discipline of leaving a tangle alone when extraction would cost more than it returns. Budding — complete first-edition route; delayed reader validation pending.

• The Art of Not Looking — search from first principles through thirty-five interactive chapters on exact retrieval, ranking, safe pruning, compression, human input, machine evidence, images, audio, video, and authorization. Growing — the complete first edition and its retrieval route are published.

• The Concrete Discrete Math of Real Systems — six chapters from suitcase-packing and fridge sticky notes up to the exact structures running Git, CRDTs, build systems, packet filters, shell completion, and MapReduce. Five bring-your-own-input evaluators: a law checker, a dependency-graph analyzer, a feasible-region carver, a decision-diagram comparator, and a residual-grammar stepper. Budding — raw, interactive, revised in place.

• Learning Bazel — fifteen chapters for Go and TypeScript programmers who have never used a build system that enforces its own dependency graph. Opens on a five-line Makefile that lies and closes on one schema feeding two languages. You type every file; nothing is cloned. The machines here are the builds themselves — a macro expander that shows what your build file becomes, and a graph walker for asking what breaks if you change this. Seedling — mapped and verified, prose under way.

How to read these

In order or by itch — every chapter stands alone, and the connective tissue ("you have seen this shape before") is linked where it helps. Chapters are undated and revised in place; their garden status (budding → growing → evergreen) is the honesty mechanism. Nothing here tracks you: no accounts, no streaks, no telemetry — progress lives in your head, where it belongs.

What qualifies for this shelf

One rule: an interactive spine. A resident of this shelf teaches by letting you falsify your own mental model against a live machine — if a piece is prose alone, however good, it lives on the blog instead. The shelf grows as trips complete; no tables of contents are promised before their chapters exist.