We present a type-based methodology for the verification of Message Passing Interface (MPI) programs written in C. The aim is to statically verify programs against protocol specifications, enforcing properties such as fidelity and absence of deadlocks. We make use of a protocol language based on a dependent type system for message-passing parallel programs, which include various communication operators, such as point-to-point messages, broadcast, reduce, and array scatter and gather. For the verification of a program against a given protocol, the protocol is first translated into a representation read by VCC, a software verifier for the C programming language. We successfully verified MPI programs in a running time that is independent of the number of processes or other input parameters. This contrasts with other techniques, notably model checking and runtime verification, that suffer from the state-explosion problem or that otherwise depend on parameters to the program itself. We experimentally evaluated our approach against state-of- the-art tools for MPI to conclude that our approach offers a scalable solution.