BPMN Analyzer: Formal analysis of BPMN process models 
The Business Process Modeling Notation (BPMN) is a widely used standard notation for defining intra- and inter-organizational workflows. It is used heavily for process automation and orchestration in many businesses. Formalizing BPMN reduces the cost of business process automation by facilitating the detection of errors and optimization potentials in process models already during design time before the implementation starts. The BPMN Analyzer is an open-source tool to analyze BPMN process models formally.
The tool supports most BPMN constructs used in practice and allows checking behavioral properties. Especially, it can check if a BPMN model contains dead activities (activities which can never execute) or cannot terminate. The following screenshot shows the detection of a dead activity in a BPMN model. The activity can never execute due to wrong gateway usage.
I published a research paper about the formalization used in the tool at the 16th International Conference on Graph Transformation (ICGT 2023). The paper won the ★ Best Paper Award ★. You can read the preprint of the paper for free.