[tlaplus] Presentation of the TLAi+ Challenge Winning Project – Specula

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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/

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/9F62E06A-DCEA-462A-8574-FC54CC9D9FEF%40lemmster.de.