Another interesting tool is ProB[1]. I believe it does symbolic model checking and supports partial order reduction. It works on specifications in multiple languages, including TLA+, but I haven&#x27;t had the chance to use it myself because it doesn&#x27;t support all TLA+ features. In particular, it doesn&#x27;t support TLA+&#x27;s higher-order operators, which my specifications use.<p>[1]: Cool visualizations: <a href="https:&#x2F;&#x2F;www3.hhu.de&#x2F;stups&#x2F;prob&#x2F;index.php&#x2F;State_space_visualization_examples" rel="nofollow">https:&#x2F;&#x2F;www3.hhu.de&#x2F;stups&#x2F;prob&#x2F;index.php&#x2F;State_space_visuali...</a>