Ladybug - an even faster tool written in java for portability
Nitpick is a tool for analyzing software specifications. Like a model checker, it is fully automatic, and generates counterexamples when claims about a specification do not hold. Unlike most model checkers though, Nitpick is designed for specifications that involve data structures.
Its specification language NP is, roughly, a subset of Z. It is strictly first-order: there are no functions over functions, for example. NP has schema structuring, like Z, so specification fragments can be composed with conjunction. Unlike Z, claims about a specification are written in the specification language itself; there's no extra meta language to learn.
Nitpick performs elementary syntax and type checking on NP specifications. It can simulate schemas by generating examples of states satisfying an invariant, or transitions of an operation. It can check claims about a specification (such as that an operation preserves an invariant), and generates counterexamples when a claim is found not to hold. By employing a variety of reduction mechanisms, Nitpick examines millions of cases in seconds.
Nitpick/NP has been applied to a variety of small case studies and has been used in course projects in the masters of software engineering program at CMU.