I have become mildly obsessed with Milner's Pi Calculus, and while I can have lots of fun drawing out little diagrams on my whiteboard, I was curious if there are any good (or bad even) modeling systems for it to do checking against your logic, in a similar fashion to something like TLA+.
If such a system does not exist or is not necessary due to reason x, I would love an explanation to why if possible.