SPECULA: SCALING FORMAL SPECIFICATIONS FOR AUTONOMOUS MODEL CHECKING OF SYSTEM CODE

Summary from the TLDR AI newsletter

Specula is an agentic system that automates the process of software bug finding through authoring and model-checking a spec for the code. It derives TLA+ specifications automatically from the code, checks code-spec conformance through trace validation, model checks the spec to find concurrency bugs, and reproduces the bug at the code layer by writing integration tests with precise timing. This post looks at what Specula gets right, its major contributions, and unresolved questions about the terrain. Specula is a great pragmatic idea, and it works for what it does, but it still skirts the real hard problem of composition, so it cannot say anything about whether per-module guarantees add up to a system-level guarantee.