refinement checking and model verification tool that analyzes CSP models to confirm that one process is a valid refinement of another. FDR is used to examine distributed communication architectures, identify protocol vulnerabilities, and verify the correctness of complex state systems before deployment. Formal Systems also offers ProBe (Process Behaviour Explorer), an animation and inspection companion tool used to explore step-by-step executions of CSP specifications. These tools are used by organizations working on high-assurance and mission-critical computing systems that require mathematically rigorous analysis.