TLA+ Spec Generator.
A self-correcting loop writes TLA+, then runs it through SANY and TLC over and over — fixing its own errors — until the specification parses, model-checks, and its invariants hold.
Try:
A self-correcting loop writes TLA+, then runs it through SANY and TLC over and over — fixing its own errors — until the specification parses, model-checks, and its invariants hold.