Jahob

Jahob is a verification system for programs written in a subset of Java. Using Jahob, developers can statically prove that methods satisfy their contracts in all possible executions, as well as that they preserve essential structural invariants and design constraints.