This TLA+ model represents the first formalization of a very large subset of MPI-2.0. It extends our previous work, in which we captured around 10% of the MPI-1.0 primitives.
MPI TLA+ Specification (PDF | TAR)
A Formal Specification of MPI 2.0
Formal Specification of the MPI-2.0 Standard in TLA+
Semantics Driven Partial-order Reduction for MPI-based Parallel Programs
An Approach to Formalization and Analysis of Message Passing Libraries