You should look into Quint: https://github.com/quint-co/quint. It comes with simple syntax and very good developer tooling. Quint to TLA+ is what Typst is to Latex.

I feel like PlusCal and TLA+ operate at a different level. I use PlusCal primarily when what I'm modeling has a lot of sequential "A then B then C..." steps. With PlusCal a program counter is implied and it maps more directly to sequential algorithms.

When I write regular TLA+, it's usually for things that aren't nearly as "order-dependent".

> What is the Typst of formal modeling?

I'm not sure there is one, but you can start exploring here:

https://en.wikipedia.org/wiki/Category:Formal_specification_...

For TLA+-styled model checking, though, there is Quint: https://quint.sh/docs/why

It's a reasonable question. There are novel things I like about the syntax - like vertically-aligned conjunction & disjunction lists - but I don't really want to defend syntax that still uses all-caps KEYWORDS like it's the COBOL era and makes you use string values for enums. The underlying formalism is, however, amazing for thinking in, and it's used by P, Quint, and FizBee which all to varying degrees paint themselves as TLA+ successor languages.

I agree that spec/implementation conformance checking is also an issue. P has apparently had some success with PObserve for trace validation (checking whether the log of a running system is a valid execution of a P spec) but it is still not a well-known method with these tools in the same way that fuzzing or property-based testing have become. This requires some real product-level thinking to make usable and possibly full ownership of the system execution environment inside a VM or something like that.