Quint

Quint is a formal specification language based on the underlying calculus of TLA+, the temporal logic of actions. Like TLA+, it's designed to help you find subtle bugs in complex systems involving concurrency. Quint distinguishes itself from TLA+ through its readability and developer experience. It has a TypeScript-like syntax that makes review easier, especially when agents write the specification. It also has a type checker, REPL and simulator and can be installed with npm. The simulator exercises the model inexpensively with randomized runs and can also generate traces from the spec to test an implementation. Our teams have found the choice between Quint and TLA+ a close call, weighing Quint's tooling against TLA+'s maturity. We hope that its ongoing development signals growing momentum behind polyglot verification.