* [http://javapathfinder.org/jpf-hj HJ-V]: Habanero Java Verification Runtime for JPF
* [https://github.com/ericmercer/4M 4M]: modeling language for API specification and verification.
* [http://github.com/ericmercer/MP-trace-language?source=c MP Trace Language]: Trace language for message passing programs
* [http://babelfish.arc.nasa.gov/hg/jpf/jpf-guided-test jpf-guided-test]: guided test extensions for JPF
* [http://github.com/ericmercer/javalite Javalite]: Javalite formalism in both Redex and Coq.
* [[Modeling Operator Workload]] ([https://github.com/ericmercer/workload Workload]--github): Workload extensions for JPF and Brahms.