These sources are about verification in the broad sense. They cover proofs, tests, benchmarks, review and sampling. Several argue about what a check can really show.
A spec the agent can't run isn't a spec yet
A short case for acceptance criteria that an agent can execute.
An Empirical Study: AI Agent Rules Need Context and Layered Enforcement
A blog post summarizing the ActPlane study of agent rules and kernel-level enforcement.
Computational Effects (Proof-Oriented Programming in F*)
The opening page of the effects part of the F* tutorial book.
DSLs Enable Reliable Use of LLMs
An argument that small languages give generated code firm boundaries.
Formal methods and the future of programming
A Jane Street post explaining why the firm now wants a formal methods team.
Hunting a 16-year-old SQLite bug with TLA+: is dqlite affected?
A Canonical post that models a SQLite bug in TLA+ to test dqlite.
Linearizability! Refinement! Prophecy!
A long explainer on proving a queue linearizable with TLA+ refinement and prophecy.
On the Unreasonable Effectiveness of Property-Based Testing for Validating Formal Specifications
Using random tests to catch formal specs that are too strong or too weak.
The Case Against Formal Verification, 50 Years Later
An essay that re-reads a 1979 paper against formal verification in light of AI coding.
The hitchhiker's guide to reading Lean 4 theorems
A short guide that teaches programmers to read Lean 4 theorems as typed code.
Theorems for Free!
A short timeline entry that introduces Philip Wadler's 1989 paper on free theorems.
Tutorial: Introduction to Formal Verification with Lean (Part 1)
A code-along tutorial that proves the one-time pad correct in Lean 4.
Your type checker may be wrong - an introduction to formal proof verification and the Curry-Howard Correspondence
A blog explainer on Curry-Howard and why type checkers may reject correct code.
Treat Agent Output Like Compiler Output
A company blog post arguing that agent-written code should be verified, not read.
Prefer STRICT tables in SQLite
A short opinion post arguing for adding STRICT to SQLite table definitions.
Build your own vulnerability harness
A Cloudflare post on its multi-stage harness for finding and triaging code vulnerabilities.
Structural Backpressure Beats Smarter Agents
A blog post arguing that machine-checked gates in coding loops matter more than smarter models.
The quality of AI-assisted software depends on unit of work management
A blog post arguing that breaking AI coding work into small, human-legible units drives quality.
agents need control flow, not more prompts
A short blog post arguing that reliable agents need control flow in code, not prompts.
From Benchmarks to Skills: Low-Rank Factors for LLM Evaluation
A preprint that finds a few latent skills behind LLM benchmark scores.
RLAIF vs. RLHF: Scaling Reinforcement Learning from Human Feedback with AI Feedback
A Google paper testing whether AI-written preference labels can replace human labels in RLHF.
A mathematical formalisation of dimensional analysis
A blog post giving two mathematical models for physical units and dimensions.
How Gödel’s Proof Works
A magazine explainer walking through the main steps of Gödel's incompleteness proof.
There is more to code review than (automatable) detection
A response arguing that a paper wrongly treats code review as only defect detection.
You can't unit test for taste
A developer's write-up of a map pipeline built with Claude and its evaluation problems.
The Return of Rigorous Full-System Timing Simulation
A blog post arguing that computer architects should measure full systems with statistically sound sampling.