> When I've tried to push TLA+ at work, the mathey syntax is usually a non-starter
Would they be interested in Quint?[0] If I understand correctly, Quint is very similar to TLA+, but with a more "code-looking" notation. And it has some nice dev tooling, like an LSP, which also lowers the barrier to entry.
Would they be interested in Quint?[0] If I understand correctly, Quint is very similar to TLA+, but with a more "code-looking" notation. And it has some nice dev tooling, like an LSP, which also lowers the barrier to entry.
[0]: https://github.com/informalsystems/quint