The TLA+ Foundation, in collaboration with NVIDIA, is pleased to announce the winners of the first GenAI-accelerated TLA+ Challenge—an open call for submissions showcasing creative and technically impressive work at the intersection of TLA+ and AI-assisted development.
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 checks them against the implementation. It combines an LLM-based generator with a Control Flow Analyzer to ensure syntactic and structural correctness, then uses SandTable for trace validation. Demonstrated on etcd’s Raft (Go) and Asterinas’s SpinLock (Rust), Specula offers a reproducible path toward scaling automated specification to broader codebases and abstracting algorithmic intent.
Award: Nvidia GeForce RTX 5090 (sponsored by NVIDIA)
Andrew tested whether local LLMs can be constrained to produce valid TLA+ by restricting token generation. Using LlamaCpp’s GBNF syntax (context-free) and the Guidance framework (context-sensitive), he showed that grammar-based constraints can reliably enforce syntax and, in some cases, symbol definition. Adding TLA+ documentation to prompts improved results, and the language’s explicit symbol declarations make it well-suited to such constraints. This approach could complement or even surpass fine-tuning for niche languages.
Award: One-year single seat, individual subscription to Github Copilot Pro+ (sponsored by the TLA+ Foundation)
Gregory explored using TLA+ as a blueprint for generating idiomatic, multithreaded Rust code. By applying TLA+’s refinement process in stages, the LLM is guided toward correct and efficient implementations, avoiding the ambiguity of natural language instructions. If this approach were combined with new TLA+ MCP server integrations, it could pave the way to fully verified, spec-driven code generation.
Award: One-year single seat, individual subscription to Github Copilot Pro (sponsored by the TLA+ Foundation)
We warmly thank all participants for their submissions. The challenge was made possible thanks to NVIDIA and the TLA+ Foundation, whose generous sponsorship funded the prizes. We also invite other companies to consider donating prizes for future challenges to help grow the TLA+ ecosystem. For those with larger, longer-term projects in mind, remember that the TLA+ Grants Program is open for proposals year-round.