What exactly is Symbolic Model Checking?
Symbolic model checking can be very useful for verifying the correctness of communications and security protocols. For example:


A symbolic model of an OAUTH2 implementation could help check for unintended consequences where an adversary obtains secret authentication tokens or related circumstantial data that could help them contravene the process.
A symbolic model of a cryptographic protocol, such as a TLS handshake, could help verify that the cryptographic design doesn't have any unintended consequences.


This works by writing a symbolic description of all the primitive functions and protocol algorithms, and then having a symbolic model checker, such as ProVerif, traverse the state space and attempt to detect state combinations that produce unfavorable results. In the case of ProVerif, symbolic models are described using the applied Pi calculus as the modeling language. This allows the description of protocols in a functional, ML-like syntax.