correctness
the methods that make agent-written software hold up: proofs, properties, replay, and receipts.
software an agent wrote in an afternoon is cheap to produce and expensive to trust. the answer is not to write less of it; it is to make wrongness cheap to find. every lesson in this category names a specific mechanism that catches a specific class of error, drawn from the projects Hraness actually runs.
the series starts from a working definition of unreasonably robust programming, then walks the toolbox: formal proofs, stateful testing, property tests, mutation, claims ledgers, replay, and the release machinery that proves where bytes came from. each lesson links the projects that use the technique, and each says what the technique cannot show.
lessons
- unreasonably robust programming: a working definitionstart here · make invalid states unrepresentable and wrongness cheap to find
- lean: proving the books balance before the tests runsubscriber · a proof checker as a build step
- tla+: checking every interleaving a test can't reachsubscriber · the bug is in the order, not the code
- hegel: stateful tests that find the three-step bugsubscriber · crash between commit and fsync, then come back
- property tests everywhere: parsers, projections, and round tripssubscriber · a thousand adversarial inputs beat a hundred examples
- kani: checking every possible number a function can seesubscriber · bounded model checking for the arithmetic tests only sample
- claims ledgers: writing down what you did not provesubscriber · the audit table that ends hand-waving
- planted bugs: how to test the testssubscriber · a suite that can't catch a bug on purpose catches none by accident
- invalid states: types, result, and parsing from unknownsubscriber · the best error is the one you cannot construct
- two implementations, one spec: parity as a test oraclesubscriber · when typescript and rust disagree, one of them is lying
- replay without clocks: deterministic reruns as evidencesubscriber · if you can replay it, you can debug it
- direct: every screen by url, deterministicallysubscriber · screenshots you can trust because the world is fake
- stylex: one typed design system across every sitesubscriber · compile-time css with the portfolio palette
- releases that prove their originsubscriber · the artifact is only trustworthy if you can prove where it came from
- rust where it earns its place: kernels, not cargo cultssubscriber · the memory-safety bill only pays where the stakes are real
projects
- algal · organisms whose runs produce receipts you can replay offline, byte for byte.
- gobstopper · a local vault for agent sessions with proofs over its transcripts.
- vhalla · peer-to-peer rooms with specs, mutants, and quorum-checked delivery.
drafted with ai assistance by ben guo