Writing
- How to validate AI-written code: tests, mutation testing, proofsWhen coding agents write more code than anyone can read, checking it becomes the main job. The validation stack from types to proofs: what each layer catches and misses, what it costs, how well agents write it, how agents game their own checks, and what to use for which code. Every rule is graded by its evidence.Article
- Formal verification in TypeScript: what you can prove in 2026TypeScript's types are unsound by design, and the only maintained tool we found that proves TypeScript itself, LemmaScript, is a tech preview. The other options: a Dafny or Lean core compiled to JavaScript, a proved model with differential tests, and branded types, Zod and fast-check at the edges. Each is labelled proof or not, with worked examples we ran.Article
- Formal verification in practice: what to prove and how far to goA ladder from stronger types to full proofs, with what each rung catches, what it costs and how well AI agents handle it: how to choose what to prove, write specs, prove a model or the code, keep proofs working in CI, and use agents without trusting them for the spec. Every rule is graded by its evidence.Article
