Specula: Scaling Formal Specifications for Autonomous Model Checking of System Code

Specula uses coding agents to generate and validate TLA+ specifications for real system code, model-checks the specifications to discover violations, and reproduces confirmed findings at the implementation level.