An executable specification language with delightful tooling based on the temporal logic of actions (TLA)
#算法刷题#Dr. TLA+ series - learn an algorithm and protocol, study a specification
A gently curated list of companies using verification formal methods in industry
Tutorial "Weeks of debugging can save you hours of TLA+". Each git commit introduces a new concept => check the git history!
APALACHE: symbolic model checker for TLA+ and Quint
TLA+ snippets, operators, and modules contributed and curated by the TLA+ community
Easiest-ever formal methods language! Designed for developers crafting distributed systems, microservices, and cloud applications
Learn TLA+ for free! No prior experience necessary!
A static web application to explore and animate a TLA+ state graph.
Interactive, web-based tool for exploring, visualizing, and sharing formal specifications in TLA+.
Generate (message) sequence diagrams from TLA+ state traces
A tree-sitter grammar for TLA⁺ and PlusCal
Distributed termination detection on a ring, due to Shmuel Safra:
