Electrod is a model finder for first-order linear temporal logic with relations, transitive closure and partial domains.
Electrod is not released yet.
As of now, Electrod relies on NuSMV or nuXmv (default), so you must at least install one of them.
Electrod is primarily aimed at being called by external, more abstract tools, such as the Electrum Analyzer. However, it can also be run as a standalone program.