TTT2
Visit the Tyrolean Termination Tool 2 (TTT2).
IsaFoR/CeTA
Visit the Isabelle Formalization of Rewriting and its accompanying tool for Certified Tool Assertions (IsaFoR/CeTA).
ConCon
Visit the tool for proving Conditional Confluence (ConCon).