---
title: "Loyola Study Finds LLMs Fail Formal Verification With Only 8.6% Success"
subtitle: "A 30-model benchmark reveals LLMs top out at 8.6% semantic correctness on TLA+ specs, exposing a hard gap between code generation and formal verification"
url: "https://alphasignal.ai/news/loyola-study-finds-llms-fail-formal-verification-with-only-8-6-success"
author: "AlphaSignal Newsroom"
author_url: "https://alphasignal.ai/editorial-team"
company: "AlphaSignal"
company_url: "https://alphasignal.ai/company/alphasignal"
published: "2026-06-04T00:00:00.000Z"
updated: "2026-06-12T01:19:20.445Z"
type: "Paper"
topics:
  - "Benchmarks"
  - "Llms"
subtopics:
  - "Hallucinations"
  - "Structured Output"
upvotes: 1177
source_url: "https://arxiv.org/abs/2606.05792"
comments: 0
truncated: true
---

# Loyola Study Finds LLMs Fail Formal Verification With Only 8.6% Success

> A 30-model benchmark reveals LLMs top out at 8.6% semantic correctness on TLA+ specs, exposing a hard gap between code generation and formal verification

If you've ever tried to write a [TLA+ specification](https://en.wikipedia.org/wiki/TLA+) for a distributed system, you know the pain: the language is precise, mathematically grounded, and unforgiving. Now imagine asking an LLM to do it for you. A new paper from Loyola University Chicago is the first to rigorously measure whether that's actually feasible, and the answer is a sobering no, at least not without a human expert in the loop.

## Why TLA+ is worth fighting for

TLA+ is a formal specification language developed by Leslie Lamport, used for designing, modelling, and verifying programs, especially concurrent and distributed systems. Think of it as executable blueprints for software: you describe what your system is allowed to do mathematically, and a tool exhaustively checks whether it ever violates your rules. Amazon Web Services has used TLA+ since 2011, and TLA+ model checking has uncovered bugs in DynamoDB, S3, EBS, and an internal distributed lock manager, with some bugs requiring state traces of 35 steps. 

TLA+ is widely used by software companies like Amazon, Microsoft, Nvidia, Google, and Oracle to check and verify critical infrastructure systems such as distributed consensus systems, confidential consortium frameworks, databases, OS kernel synchronization, and cache coherence. The catch? Writing correct TLA+ specifications from natural language still requires time and expertise, which limits adoption. That bottleneck is exactly what this paper tries to address.

## The two-layer verification problem

Before diving into results, it helps to understand how TLA+ validation works, because the paper uses a two-stage pipeline that maps directly onto two very different failure modes for LLMs.

* **Syntactic correctness (SANY):**SANY is the syntactic analyzer that parses and checks the spec for syntax errors. Passing SANY just means the code is grammatically valid TLA+.
* **Semantic correctness (TLC):**TLC verifies temporal logic properties by exhaustively exploring the state space of a specification. The TLC model checker builds a finite state model of TLA+ specifications for checking invariance properties, generating a set of initial states and performing a breadth-first search over all defined state transitions. Passing TLC means the spec actually captures the intended behavior of the system.

_Preview only. Full text requires an AlphaSignal Pro account._

## Sources

- [Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation](https://arxiv.org/abs/2606.05792)
- [TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation](https://arxiv.org/abs/2606.06133v1)
- [Industrial Use of TLA+ :: TLA+ Foundation](https://foundation.tlapl.us/industry/index.html)
- [How Amazon Web Services Uses Formal Methods – Communications of the ACM](https://cacm.acm.org/research/how-amazon-web-services-uses-formal-methods/)
- [Can LLMs model real-world systems in TLA+? – ACM SIGOPS](https://www.sigops.org/2026/can-llms-model-real-world-systems-in-tla/)