Specula: Scaling formal specifications for autonomous model checking of system code

The blog post critically evaluates "Specula," a system for automated software bug finding via TLA+ specifications. While it highlights Specula's impressive capabilities and technical novelty, such as finding bugs across diverse open-source systems and its push-button automation, the author raises concerns about the lack of principled justifications for its methods, potential for circular reasoning, and challenges surrounding compositional verification in multi-service environments. The critique oscillates between admiration for Specula's achievements and skepticism about its theoretical foundations.