Blog

Self-Hosted Inference on Apple Silicon

2026-10-20

Part 5 of Oracles, Traces, Triage. Returning to the agent experiments with a local model server: what runs on my Macs, and what needs testing before I can use it for that work.

The Theorem Holds for the Wrong Function

2026-10-10

Part 3 of What a Proof Covers. The proof from the previous post also goes through for a function that reverses nothing. What a proof covers is its statement, about its definitions, under its assumptions.

Every List

2026-09-10

Part 2 of What a Proof Covers. A complete Lean proof, by induction, that reversing a list twice gives back the list, read one step at a time.

One List, a Thousand Lists

2026-08-10

Part 1 of What a Proof Covers. An example test checks a rule for one list and a property test checks it for the lists it happened to generate. Neither says anything about the lists nobody tried.

What a Proof Covers

2026-07-10

A short series that takes one small rule through an example test, a property test and a Lean proof, and then asks what each of them actually established about the code that runs.

Agents as Fuzzers

2026-02-16

Part 4 of the Oracles, Traces, Triage series. A fuzzer is a search tool whose results must be triaged. An AI agent is a search tool whose results must be triaged. Perhaps that's not a coincidence.

Testing the Bugs Between Calls

2026-02-15

Part 3 of the Oracles, Traces, Triage series. On combining agent swarms and agent skills with stateful property-based testing to find the consensus bugs that live in sequences, not single calls.