IMO TLA+ is not very good. It has super weird syntax, and a whole separate DSL (PlusCal) to give it workable syntax for programs. You can really tell it was created by the same mind as LaTeX.
What is the Typst of formal modeling?
Another issue is that you end up with a formal model that passes, but then you have still have to convert that to a real language by hand and not make any mistakes.
For TLA+-styled model checking, though, there is Quint: <a href="https://quint.sh/docs/why" rel="nofollow">https://quint.sh/docs/why
IshKebab · · focus · HN ↗
What is the Typst of formal modeling?
Another issue is that you end up with a formal model that passes, but then you have still have to convert that to a real language by hand and not make any mistakes.
Jtsummers · · focus · HN ↗
I'm not sure there is one, but you can start exploring here:
<a href="https://en.wikipedia.org/wiki/Category:Formal_specification_languages" rel="nofollow">https://en.wikipedia.org/wiki/Category:Formal_specification_...
For TLA+-styled model checking, though, there is Quint: <a href="https://quint.sh/docs/why" rel="nofollow">https://quint.sh/docs/why