Nunchaku

A counter-example finder for higher-order logic, designed to be used from various proof assistants, and a spiritual successor to Nitpick. See also the README ().

https://nunchaku-inria.github.io/nunchaku/

The development repository is hosted on github. Nunchaku is written in OCaml, funded by Inria and released under the BSD license.

• Input formats: input_lang (draft)
• Model format: model_syntax (draft)
• Pipeline of Transformations: pipeline
• Higher Order aspects: higher_order
• Inductive predicates: inductive predicates
• Internal API documentation:
  • 0.6
  • 0.5
  • 0.4
  • 0.3

Contact

Bugs should be reported on https://github.com/nunchaku-inria/nunchaku/issues

There is a mailing list for users and proof assistants developers, nunchaku-users@lists.gforge.inria.fr (subscription).