Если использовать взаимодействия на сообщениях изолированных процессов, то один из методов доказательства корректности - построение модели на какой-нибудь Promela и далее автоматизированный Model-Checking.