From around the web
Articles worth keeping, with a few words on why I saved them.
9 saved articles
Newest saves firstWhy I saved it
A practical introduction to TLA+ through leader election, safety, and liveness. The discussion of Verus and proof-generating agents makes it especially useful for understanding what remains between checking a finite model and verifying the software that implements it.
Why I saved it
A useful reference for designing agent permissions around the data an agent has already seen. The Trust Ratchet makes the timing of access restrictions concrete: enforcement must be in place before sensitive responses reach the model.
Why I saved it
A compelling way to think about AI-generated code: use models to explore optimizations while explicit contracts and semantic checks constrain the result. The compiler analogy clarifies why understanding the high-level program can matter more than reading every generated instruction.
Why I saved it
A valuable account of both the power and the limits of automated formal methods. The trace, model-checking, and reproduction loops are worth studying, while the critique keeps a crucial distinction in view: finding reproducible bugs does not establish that inferred specifications capture the intended behavior.
Why I saved it
Explains why agentic coding changes the economics of formal methods: proof tools can become easier to use just as generated code makes verification more urgent. Especially relevant to treating specifications and proofs as feedback infrastructure for coding agents.
Why I saved it
A useful challenge to treating small PRs as a universal rule. As AI makes large changes cheaper to generate, the harder engineering problem becomes reviewing, validating, and rejecting experiments quickly enough to let good designs emerge.
Why I saved it
A clear account of why traces need quality signals. Connecting user feedback and evaluations to runs turns observability into a way to improve the model, harness, and context—useful when designing an agent platform beyond logs and dashboards.
Why I saved it
A useful distinction for system design: some states must never occur, while others need to be visible and eventually resolved. It connects everyday product decisions to safety and liveness without treating every awkward intermediate state as a modeling mistake.
Why I saved it
Worth reading for its view of CI scheduling as a decision problem: prioritize the set of build results needed to safely merge a change, rather than just the most likely path. The SubmitQueue case makes the trade-off between speculative work, latency, and correctness concrete.