I too am still investigating the space, but what's attractive to me about CPNs is that they can be both the specification and the implementation. How you describe the CPN in code matters, but I'm toying with a rust + SQL-macros version that makes describing invariants etc natural. My understanding is that for TLA+ you'd need to write the spec, and then write an implementation for it. This might be another path for "describe formally verifiable shape then agentic code it", but it smells to me a little like it wouldn't be doing as much work as it could. I think in this there's an opportunity to create a "state store" where the network topology and invariants ensure the consistency of the "marking" (e.g. state of the database here) and that its in a valid state based on the current network definition. You could say "well SQL databases already have check constraints", and we'd probably use those under the hood, but I am betting on the ergonomics of putting the constraints right next to the things/actions relevant to them.

Yeah, as far as I can tell TLA+ can accomplish more or less the same stuff as Colored Petri Nets. You get a pretty graph with CPNs and it can be interesting to watch the data flow around in the animators, but I've had trouble doing anything terribly useful with Petri Nets.

I haven't really done anything with it, but I've heard Alloy gives you a graphical animation while giving you similar utility to TLA+.

There were a number of methods for doing TLA-like stuff. Others included SPIN/Promela, Pi Calculus (IIRC), and Event-B.