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.