Autonomous coding agents increasingly execute multi-step software work. However, lifecycle states such as reviewed, tested, done, and ready-to-merge remain claims unless a downstream system can decide whether those claims are supported by current evidence. In this work, we present Proof-or-Stop Lifecycle Control, a method in which lifecycle transitions are admitted only when fresh, tracked-source-state-bound, mechanically verifiable evidence satisfies the relevant gate. The method instantiates an agent-as-claim lifecycle semantics: agent outputs may propose lifecycle claims, but do not themselves constitute lifecycle state. Here, “proof” is used operationally to mean gate-admissible evidence under a stated trust model, not a proof of semantic program correctness.

Hunting a 16-year-old SQLite bug with TLA+: We model the WAL race condition to reproduce the issue, verify the fix, and analyze if dqlite is vulnerable.

For me, the question of memory is the most interesting subfield of AI. The first time I interacted with MemGPT (now Letta), I felt like I had crossed a Rubicon: memory transformed a simple question and answer bot into (what appeared to be) a being.

AI can generate code faster than humans can understand it. What does software ownership mean when engineers no longer write most of the code?

One of the most important, and yet potentially frustrating, tasks that is required to allow any make-based build environment to function properly is the correct listing of dependencies in the makef…

A gentle introduction to the Pi coding agent and why I think it’s a glimpse into the future of software.

It's better if the message comes in an expensive box.

While working on an article for the Monad.Reader, I've had the opportunity to think about how people learn and gain intuition for abstraction, and the implications for pedagogy. The heart of the matter is that people begin with the concrete, and move to the abstract. Humans are very good at pattern recognition, so this is…

A deep dive into how Linux manages process memory, page tables, and virtual address spaces

An interactive deep dive into how the Burrows-Wheeler transform works for compression and for genomics sequence alignment algorithms.

tl;dr: Having swap is a reasonably important part of a well functioning system. Without it, sane memory management becomes harder to achieve.

Exploring the world of constraint solvers with very simple examples.

A blog about making culture. Since 1999.

In my previous blog post I stated that I started defaulting to Rust for my personal projects. While I really like Rust for its type-system, I'm not a huge fan of its learning curve. There is definitely a bit of a sunk-cost with a dash of Stockholm syndrome whenever I say I love Rust.

Srihari Srirama...