Multi-Agent Communicating Process Choreography Prover. Faithful BEAM realization of Weske (2019) and Lohmann, Wolf, and Dijkman (2009).

Composes asynchronous communicating workflow nets across message channels (NA ⊗_Channel NB) and formally verifies:

1. Communicating Soundness: Global final marking reachable with all local nets complete.
2. Message Buffer Safety: No message overflow on asynchronous channels.
3. No Orphan Messages: When all agents complete, message channels must be completely empty.
4. Absence of Asymmetric Deadlocks: Neither agent is blocked waiting for messages that will never be sent.