Get the latest tech news

GenAI-Accelerated TLA+ Challenge

The TLA+ Foundation, in collaboration with NVIDIA, is pleased to announce the GenAI-accelerated TLA+ challenge—an open call for submissions that explore the intersection of TLA+ and generative AI. 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:

Participants are invited to develop engineering-oriented solutions that advance the usability, accessibility, and automation of formal specification through the integration of GenAI. 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 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.

Get the Android app