Systems software, formal methods, and the BEAM. Notes on what I'm building.
Two controls every production agent needs, a hard per-run spend cap and a human gate in front of irreversible actions, keep getting bolted on at the LLM gateway or the observability dashboard. Both are the wrong layer. Here is why they belong on the job, with the pattern in Belay.
I built a static analyzer for OTP supervision trees and ran it over thirty-some well-known open-source Elixir projects. It found real cross-tree coupling in Livebook, TeslaMate, Teiserver, and Electric: the kind a restart turns into an error somewhere that looks unrelated.
I gave a tool the execution traces of a small etcd program and no properties to check. It wrote a TLA+ specification, invented its own safety invariant, ran a model checker, and produced a counterexample. That counterexample matches an open, unfixed etcd issue, filed in April 2026, after the training cutoff of the model it used, Claude Sonnet 4.5.
What two Nobel economists, Elinor Ostrom and Oliver Williamson, get right about keeping a codebase coherent when AI agents write a lot of it.