§ Writing
Writing
Notes on proving things about numeric code, generating code from ontologies, and measuring what models produce.
July 31, 2026 · 6 min read
A gateway is a control point, not a proof
Reading the docs for Google's Agent Gateway. Some of what it enforces is a genuine invariant. Some of it is a language model grading another language model, which the docs are refreshingly honest about.
July 31, 2026 · 9 min read
Four ways to prove a program right
Kani, Verus, Dafny, and Lean prove different things, and only one of them proves something about the binary you ship. A comparison written from the position of having used exactly one of them.
July 31, 2026 · 6 min read
Where the ghost code goes
Verus erases proofs before compilation, which sounds like a metaphor until you go read the macro that does it. What I learned about ghost types from fixing a turbofish that fell off during expansion.
July 20, 2026 · 4 min read
Proving a permutation is a bijection
A statistics library is a bad fit for testing alone. The interesting failures are index arithmetic and structural invariants nobody writes a test for — so I model-check them instead.
July 6, 2026 · 4 min read
An ontology as a type system
The type layer of a Rust statistics library, generated from a TypeDB ontology. Not codegen for its own sake — a place to put domain knowledge where the compiler can enforce it.
June 18, 2026 · 4 min read
Fine-tuning for COBOL, and the harness that measures it
A 0.5B model for COBOL system understanding is the easy half. The hard half is knowing whether it got better — which means fixing the benchmark first.
May 12, 2026 · 6 min read
Wrapping an agent in MCP is a schema problem
Exposing a LangChain agent over the Model Context Protocol. The transport is the easy half — the contract is a JSON Schema read by a model that will take every field in it literally.
March 24, 2026 · 6 min read
When the user table becomes a cache
Putting Auth0 in front of Payload CMS is about forty lines of code. The decision underneath it is which system owns the user — and whether you're willing to answer that once.
February 10, 2026 · 6 min read
Most automation is a query on a timer
Jira and Confluence automation rules are sold as Trigger, Condition, Action. Count the real ones and the trigger turns out to be the least interesting part.