https://foundation.tlapl.us/challenge/index.html

 1. TLA+ Foundation > 
 2. GenAI-accelerated TLA+ challenge

GenAI-accelerated TLA+ challenge

My image description

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:

  * 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.

---------------------------------------------------------------------

Copyright (c) 2025 The Linux Foundation (r). All rights reserved. The
Linux Foundation has registered trademarks and uses trademarks. For a
list of trademarks of The Linux Foundation, please see our Trademark
Usage page.

The TLA+ logo

  * Home

---------------------------------------------------------------------

  * TLA+ Blog
      + April 2025 Monthly Development Update
      + March 2025 Monthly Development Update
      + February 2025 Monthly Development Update
      + January 2025 Monthly Development Update
      + December 2024 Monthly Development Update
  * TLA+ Foundation Grants
      + TLA+ Foundation Grant Program Call for Proposals
  * GenAI-accelerated TLA+ challenge

More

  * GitHub
  * Mailing List
  * Mailing List Archive
  * Conferences and Events

---------------------------------------------------------------------

  *  
    Language []
  *  
    Theme [Tlaplus]
  *  
    Clear History