Skip to main content
Ctrl+K
AI4FM | AI for Formal Methods - Home
  • GitHub

  • Pages

    • About
    • Team
    • Software and Datasets
    • Funding
    • Get Involved

  • Research Papers

    • All Papers
    • TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation
    • Can LLMs Write Correct TLA+ Specifications?
    • ChatTLA+: Using LLMs for TLA+ Formal Specification Generation and Verification
    • Large Language Models (LLM) and Temporal Logic of Actions (TLA): How Effective are LLMs for Verification Systems
    • Automating TLA+ Model Synthesis with Large Language Models and Formal Verification Pipelines
    • TLA+ for All: Running Model Checking in a Python Notebook

  • Research Updates

    • All Posts
    • TLA-Prover Paper Accepted to ICSOFT 2026
    • Our Paper on LLM-Based TLA+ Specification Generation Has Been Accepted
    • New Paper: TLA-Prover — Fine-Tuning LLMs for Verifiable TLA+ Specification Synthesis
    • Eric Spencer Presents ChatTLA+ at Loyola University Chicago
    • Brian Ortiz Presents Poster at Graduate School Interdisciplinary Research Symposium 2026
    • Can LLMs Write Correct TLA+ Specifications? Our New Evaluation Study
    • Brian Ortiz Presents Poster at GCASR 2025
    • Eric Spencer Awarded Mulcahy Scholar Stipend
    • TLA+ for All: Running Model Checking in a Python Notebook

Posts tagged GRPO

New Paper: TLA-Prover — Fine-Tuning LLMs for Verifiable TLA+ Specification Synthesis

  • 16 May 2026
  • Author: Arslan Bisharat
  • Language: English
  • Category: Research Update
  • Tags: Formal Methods TLA+ LLMs Fine-Tuning GRPO DPO

Building on our evaluation study that showed the best public LLMs achieve only 8.6% semantic correctness on TLA+ specification generation, we present TLA-Prover: a 20-billion-parameter model trained specifically for TLA+ specification synthesis.

Read more ...

By AI4FM Research Group

© Copyright 2026, AI4FM Research Group.