Currently, all existing formal verification tools are designed to serve as formal verifiers, using one implementation or the other.
In order to introduce and implement even the simplest new formal algorithm, the developer has to be completely aware of the entire system she of he is implementing her or his algorithm upon. As if that wasn't enough, from the nature of the formal field, most systems are implemented in a very low level C code. This is since the complexity of such algorithms in exponential to begin with.
Now, let's see you try to implement a new formal algorithm.
JTLV is a new tool aimed to facilitate and provide a unified framework for developing formal verification algorithms in a high level programming environment.
JTLV provides a pure Java user API, while the exponential complexity derived from using BDDs, is actually implemented in C, and is accessed through a JNI to the C libraries (all the underlying BDD implementation are invisible to the user). There are many BDD libraries to pick from, and the BDD package used, can be set during pre-run, or dynamically during runtime. The whole BDD interface is all thanks to the JavaBDD Project.
Using the chosen BDD library, JTLV continues to construct Design Modules. Currently, the design modules can be specified using, SMV, or FDS formats (FDS is a simpler format for specifying Finite State Machines, which was implemented first in order to prove the feasibility of this project). Both parsers were written using ANTLR v3. The SMV parser is also connected to the editor, which enables it to use the nice facilities that eclipse can offer (still lots more to come in this area).
From the other hand, algorithm designers can load Specification file (SPC). JTLV support almost all known temporal specification format. The SPC parser is also connected to eclipse as editor, again giving it the nice facilities that eclipse can offer.
AND THUS, it all sums up to be a Java environment,
Now, That's the way I want to implement my next formal algorithm.