[isabelle-dev] Nitpick counterexample generator now available

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Thu Feb 26 11:55:03 CET 2009

I am pleased to announce the first release of Nitpick, a Kodkod  
(Alloy) based counterexample generator for Isabelle/HOL on which I've  
been working since October. (The name Nitpick is shamelessly stolen  
from an obsolete MIT tool.) The tool is similar to Refute in principle  
but it scales better and produces more genuine counterexamples for  
inductive datatypes.

You can download Nitpick from


It requires a recent snapshot of Isabelle2009. The package contains  
everything you need: Nitpick (.thy + SML), Kodkod (Java), and a SAT  
solver (Java). To install it, just type './build'. The manual is  
included in the package and is also available at


The plan is to release Nitpick 1.1 to the wider public alongside the  
Isabelle2009 "winter" release, and then to incorporate it directly in  
Isabelle from then on.

Please let me know if you have any feedback or bug reports concerning  
Nitpick, or if you find typos in the manual.



More information about the isabelle-dev mailing list