First-Order Logic Modelchecker
Revision 106 of OpenGT introduces an FO Modelchecker :-)