Lambda the Ultimate

Modular Verification of Code with SAT (pdf)

"For this case study, we used a pre-existing specification of the Java List interface written in the Java Modeling Language (JML) ...
an approach to checking object-oriented code against detailed specifications that is fully automatic, demanding from the user only a specification of the method to be checked, an indication of the size of the space to be searched, and for each distinct representation, an abstraction function and representation invariant."

Using Alloy's Kodkod - a new relational engine designed to be a plugin component / backend for other tools. (It solves Sudoku too...)