Showing 2025Show all
2 papers · 1 filter
cs.LO2025
Towards Language Model Guided TLA+ Proof Automation
Yuhao Zhou, Stavros Tripakis
Formal theorem proving with TLA+ provides rigorous guarantees for system specifications, but constructing proofs requires substantial expertise and effort. While large language mod…
cs.LO2025
Retrieval-Augmented TLAPS Proof Generation with Large Language Models
Yuhao Zhou
We present a novel approach to automated proof generation for the TLA+ Proof System (TLAPS) using Large Language Models (LLMs). Our method combines two key components: a sub-proof…