Description
Checks models of distributed software systems for correctness properties such as deadlocks, race conditions, and protocol mistakes. Developers and researchers use it to reason about designs before implementation or deployment.
Formal verification depends on the model being accurate. A successful check does not prove the real implementation is safe unless the model, assumptions, and properties match the system.