Nitpick Home Page


Coming Soon!!!
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.

The Nitpick checker is freely available in binary form for the Macintosh.

More information about Nitpick

Obtaining Nitpick executables and the NP reference manual

Some publications about Nitpick

For more information, contact

Nitpick was brought to you by:

    Daniel Jackson (
    Craig A. Damon (
In conjunction with
    Composable Software Systems Group


    School of Computer Science
    Carnegie Mellon University