Field Notes on Working with LLMs

Essays on working with large language models — the tools, the process, and the questions that follow.

• Thoughts on Working with LLMs — general workflow lessons from fiction, vibe coding, academic papers, and Lean

• Writing Fiction with LLMs — what I learned writing twelve short stories, two novellas, and a novel-scale rewrite

• Who Wrote This? — on authorship when humans and AI collaborate

• The Lean Project — formalizing the C++ standard library in Lean 4, and the Lean Manifests machinery that came out of it

• l3m: A Verified Coding Agent — building a coding agent whose sandbox is proven by the Lean kernel; SafePath, compression budgets, and adversarial pen-testing between AI instances

• When Your Safe Agent Helpfully Leaks Your API Key — an incident report. Kernel-verified confinement isn’t the same as secret-safety. What I missed and what I did about it.

• Reading a Library from Its Manifests — what one of us learned about a CommonMark parser from outside, what the other learned from inside

• Manifests as Specs — a debug-first design exercise: writing a Lean linenoise manifest before the code, and the ten rules that emerged.

• If You Can State It, You Can Probably Prove It — a cull of a hundred theorems overturned my ladder: proof is cheap, precise statement is the scarce resource, and statement difficulty is a design signal for functional-over-state-machine code.

• Turing Complete and Safe: Running Untrusted Code Without a Cage — hand a coding agent a program it wrote at runtime, let it loop forever if it likes, and still prove it cannot touch the world. The trick is moving the safety boundary off the edge of the machine and onto the edge of a type.