Showing 2025 · cs.LOShow all
2 papers · 2 filters
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
Accelerating Protocol Synthesis and Detecting Unrealizability with Interpretation Reduction
Derek Egolf, Stavros Tripakis
We present a novel counterexample-guided, sketch-based method for the synthesis of symbolic distributed protocols in TLA+. Our method's chief novelty lies in a new search space red…