Presentation of the TLAi+ Challenge Winning Project – Specula

[Markus Kuppe]

The winners of the 1st TLA+ GenAI Challenge [1] presented their winning submission, Specula [2], at the recent TLA+ Community meeting. You can watch the recording here: https://lnkd.in/gZ2kd67G


Specula, developed by Qian Cheng, Dr. Tianyin Xu, and Dr. Yu Huang, is an open-source framework that automatically derives TLA+ specifications from source code and verifies them against the implementation.

By combining an LLM-based specification generator with a Control Flow Analyzer, Specula ensures syntactic and structural correctness, while trace validation establishes semantic alignment between specification and code.

Demonstrated on etcd’s Raft (Go) and Asterinas’s SpinLock (Rust), Specula represents a major advance toward scaling automated formal specification and bridging formal methods with AI-driven development.


Specula started as a hackathon project for the TLAi+ Challenge, but has since grown into a cross-institution collaboration with Nanjing University, Microsoft Research Asia, University of British Columbia, and University of Illinois Urbana-Champaign [3].


[1] https://foundation.tlapl.us/challenge/index.html
[2] https://github.com/specula-org/Specula/
[3] https://www.linkedin.com/feed/update/urn:li:activity:7394550698715234304/