GenAI-accelerated TLA+ challenge

#tlaplus #hackathon #llm #tooling

Sharing this news here hoping you might find it interesting!

TLDR; if you have some experience with LLMs and TLA+, there is a chance to win some prizes. If you have experience with LLMs but not with TLA+ yet, but you are interested in developing TLA+ tools, apply to the TLA+ grant program.

The original announcement can be found on the TLA+ foundation website: https://foundation.tlapl.us/challenge/index.html

TLA+ is a formal specification language designed for modeling and verifying concurrent and distributed systems.

This initiative aims to foster practical and innovative tooling, workflows, and approaches that bring the capabilities of generative AI and LLMs to TLA+. Participants are invited to develop engineering-oriented solutions that advance the usability, accessibility, and automation of formal specification through the integration of GenAI.

Awards

1st Place: Nvidia GeForce RTX 5090 (sponsored by NVIDIA)
2nd Place: One-year single seat, individual subscription to Github Copilot Pro+ (sponsored by the TLA+ Foundation)
3rd Place: One-year single seat, individual subscription to Github Copilot Pro (sponsored by the TLA+ Foundation)

Example Project Areas

Participants may submit work including, but not limited to:

Intelligent refactoring of TLA+ specifications (e.g., managing UNCHANGED correctly when adding variables)
LLM-enhanced linters, formatters, or other development tools
LLM-driven tools for automated grading in education
Visualizations of specifications or execution traces
Generation of type annotations for tools like Apalache
Synthesis of inductive invariant candidates, validated via TLC or Apalache
Synthesis of TLAPS proofs
Synthesis of entire specifications from source code and design documents

Evaluation

Submissions will be judged by the TLA+ Specification Language Committee (SLC)

The Jury will evaluate submissions based on their functionality, relevance to the TLA+ ecosystem, and the thoughtful use of AI. Submissions must be reproducible by the Jury. Passive formats, such as videos alone, are not sufficient. However, the Jury does not require a fully polished product—a prototype is sufficient. All submissions must be released under the MIT license, and any underlying AI models must be publicly available.

The use of GenAI/LLMs is explicitly encouraged, provided that any AI-generated content—such as specs, invariants, visualizations, … —is checked using some form of verification such as the TLA+ tools.

Catch the live announcement at the TLA+ Community Event 2025!

Participation Criteria

Eligible participants must meet the following:

Prior engagement with the TLA+ community (e.g., contribution to mailing lists, forums, open-source repositories, conference presentations, or academic publications)
Must not be a member of the TLA+ Foundation Board or Specification Language Committee
Must not be subject to any legal, contractual, export control, or jurisdictional restrictions that would preclude participation

Submission Timeline & Announcement

Submissions will open alongside this announcement. The deadline to submit entries for the challenge is two months from the announcement date on 07/03/2025. Submissions must be sent to genai@tlapl.us. The jury will select the winner one month after the submission period closes. We welcome innovative, technically robust, and practically valuable contributions that explore and expand the potential of GenAI within the context of TLA+.

For longer-term or foundational engineering and research efforts related to TLA+, we encourage you to explore the TLA+ grant program.