Shadowgraph
TrendingAbout
Sign in

nunchaku-inria/nunchaku

Model finder for higher-order logic

OCaml

52

1,500 commits

updated Jul 11, 2026

nunchaku-inria.github.io/nunchaku

See the code

README

Build status on GitHub

A counter-example finder for higher-order logic, designed to be used from various proof assistants. A spiritual successor to Nitpick. Documentation at https://nunchaku-inria.github.io/nunchaku/.

Nunchaku requires CVC4 1.5 or later. Alternatively, it can use other backends:

We have a set of problems for tests and regressions, that can also be helpful to grasp the input syntax and see how to use the constructs of Nunchaku.

Table of Contents

Basic Usage

After installing nunchaku (see Build/Install) and at least one backend, call the tool on problem files written in one of the accepted syntaxes (Input/Output/Solvers) as follows:

$ git clone https://github.com/nunchaku-inria/nunchaku-problems
$ nunchaku nunchaku-problems/tests/first_order.nun
SAT: {
  type term := {$term_0, $term_1}.
  type list := {$list_0, $list_1}.
  val nil := $list_1.
  val a := $term_1.
  val b := $term_0.
  val cons :=
    (fun (v_0/75:term) (v_1/76:list).
       if v_0/75 = $term_0 then $list_0 else if v_1/76 = $list_0 then $list_1
       else $list_0).}
{backend:smbc, time:0.0s}

A list of options can be obtained by calling nunchaku --help. A few particularly useful options are:

  • --help for listing options.

  • --timeout <n> (or -t <n>): maximal amount of seconds before returning "unknown"

  • j <n> for controlling the number of backend solvers active at the same time.

  • --solvers s1,s2 (or -s s1,s2) for using only the listed solvers.

  • --debug <n> (where n=1,2,…5) to enable debug printing. The maximal verbosity level is 5, and it is very verbose. Consider using nunchaku --debug 5 foo.nun | less -R to not drown in pages of text.

  • --pp-all (and each --pp-<pass>) for printing the problem after each transformation.

  • -nc to disable colored output if your terminal does not support it..

Contact

There is a dedicated mailing list at nunchaku-users@lists.gforge.inria.fr (register). The issue tracker can be used for reporting bugs.

Documentation

See the website https://nunchaku-inria.github.io/nunchaku/ and the documentation sources.

Build/Install

To build Nunchaku, there are several ways.

Released versions

Releases can be found on https://gforge.inria.fr/projects/nunchaku .

Opam

The easiest way is to use opam, the package manager for OCaml. Once opam is installed (don’t forget to run eval `opam config env` when you want to use opam), the following should suffice:

opam pin add -k git nunchaku https://github.com/nunchaku-inria/nunchaku.git#master

then opam should propose to install nunchaku and its dependencies. To upgrade:

opam update
opam upgrade nunchaku

Note that the binary is called 'nunchaku.native' until is it installed.

Manually

You need to install the dependencies first, namely:

Once you have entered the source directory, type:

make

License

Free software under the BSD license. See file 'LICENSE' for more details.

Input/Output/Solvers

Supported input formats are:

  • nunchaku’s own input format, ML-like (extension .nun)

  • TPTP (very partial support, extension .p)

  • TIP (extension .smt2)

Supported solver backends:

How to make a release

  • udpate the repository itself

    • edit nunchaku.opam to change version number

    • git commit --amend to update the commit

    • git tag 0.42

    • git push origin stable --tags

  • make an archive:

    • tar.gz: git archive --prefix=nunchaku/ 0.42 -o nunchaku-0.42.tar.gz

    • zip: git archive --prefix=nunchaku/ 0.42 -o nunchaku-0.42.zip

  • upload the archive on gforge, write some release notes, send a mail.

cvc4
higher-order
hol
isabelle
logic
model-finding
proof-assistant
sat

Contributors

c-cube

1,436 commits

blanchette

45 commits

hargoniX

18 commits

fpottier

1 commits

Similar repos

OCamlPro/alt-ergo

OCamlPro public development repository for Alt-Ergo

148

formalsec/smtml

An SMT solver frontend for OCaml

81

epfl-lara/stainless

Verification framework and tool for higher-order Scala programs.…

404

Gbury/mSAT

A modular sat/smt solver with proof output.

106

msakai/toysolver

My sandbox for experimenting with solver algorithms.

159

input-output-hk/Lean-blaster

SMT-based reasoning core for Lean4

58

boogie-org/corral

solver for the reachability modulo theories problem

64

lukaszcz/coqhammer

CoqHammer: An Automated Reasoning Hammer Tool for Rocq - Proof Automation for Dependent Type Theory

248

Languages

OCaml

97.3%

SMT

2.2%

nunchaku-inria/nunchaku

Model finder for higher-order logic

OCaml

52

1,500 commits

updated Jul 11, 2026

nunchaku-inria.github.io/nunchaku

See the code

README

Build status on GitHub

A counter-example finder for higher-order logic, designed to be used from various proof assistants. A spiritual successor to Nitpick. Documentation at https://nunchaku-inria.github.io/nunchaku/.

Nunchaku requires CVC4 1.5 or later. Alternatively, it can use other backends:

We have a set of problems for tests and regressions, that can also be helpful to grasp the input syntax and see how to use the constructs of Nunchaku.

Table of Contents

Basic Usage

After installing nunchaku (see Build/Install) and at least one backend, call the tool on problem files written in one of the accepted syntaxes (Input/Output/Solvers) as follows:

$ git clone https://github.com/nunchaku-inria/nunchaku-problems
$ nunchaku nunchaku-problems/tests/first_order.nun
SAT: {
  type term := {$term_0, $term_1}.
  type list := {$list_0, $list_1}.
  val nil := $list_1.
  val a := $term_1.
  val b := $term_0.
  val cons :=
    (fun (v_0/75:term) (v_1/76:list).
       if v_0/75 = $term_0 then $list_0 else if v_1/76 = $list_0 then $list_1
       else $list_0).}
{backend:smbc, time:0.0s}

A list of options can be obtained by calling nunchaku --help. A few particularly useful options are:

  • --help for listing options.

  • --timeout <n> (or -t <n>): maximal amount of seconds before returning "unknown"

  • j <n> for controlling the number of backend solvers active at the same time.

  • --solvers s1,s2 (or -s s1,s2) for using only the listed solvers.

  • --debug <n> (where n=1,2,…5) to enable debug printing. The maximal verbosity level is 5, and it is very verbose. Consider using nunchaku --debug 5 foo.nun | less -R to not drown in pages of text.

  • --pp-all (and each --pp-<pass>) for printing the problem after each transformation.

  • -nc to disable colored output if your terminal does not support it..

Contact

There is a dedicated mailing list at nunchaku-users@lists.gforge.inria.fr (register). The issue tracker can be used for reporting bugs.

Documentation

See the website https://nunchaku-inria.github.io/nunchaku/ and the documentation sources.

Build/Install

To build Nunchaku, there are several ways.

Released versions

Releases can be found on https://gforge.inria.fr/projects/nunchaku .

Opam

The easiest way is to use opam, the package manager for OCaml. Once opam is installed (don’t forget to run eval `opam config env` when you want to use opam), the following should suffice:

opam pin add -k git nunchaku https://github.com/nunchaku-inria/nunchaku.git#master

then opam should propose to install nunchaku and its dependencies. To upgrade:

opam update
opam upgrade nunchaku

Note that the binary is called 'nunchaku.native' until is it installed.

Manually

You need to install the dependencies first, namely:

Once you have entered the source directory, type:

make

License

Free software under the BSD license. See file 'LICENSE' for more details.

Input/Output/Solvers

Supported input formats are:

  • nunchaku’s own input format, ML-like (extension .nun)

  • TPTP (very partial support, extension .p)

  • TIP (extension .smt2)

Supported solver backends:

How to make a release

  • udpate the repository itself

    • edit nunchaku.opam to change version number

    • git commit --amend to update the commit

    • git tag 0.42

    • git push origin stable --tags

  • make an archive:

    • tar.gz: git archive --prefix=nunchaku/ 0.42 -o nunchaku-0.42.tar.gz

    • zip: git archive --prefix=nunchaku/ 0.42 -o nunchaku-0.42.zip

  • upload the archive on gforge, write some release notes, send a mail.

cvc4
higher-order
hol
isabelle
logic
model-finding
proof-assistant
sat

Similar repos

OCamlPro/alt-ergo

OCamlPro public development repository for Alt-Ergo

148

formalsec/smtml

An SMT solver frontend for OCaml

81

epfl-lara/stainless

Verification framework and tool for higher-order Scala programs.…

404

Gbury/mSAT

A modular sat/smt solver with proof output.

106

msakai/toysolver

My sandbox for experimenting with solver algorithms.

159

input-output-hk/Lean-blaster

SMT-based reasoning core for Lean4

58

boogie-org/corral

solver for the reachability modulo theories problem

64

lukaszcz/coqhammer

CoqHammer: An Automated Reasoning Hammer Tool for Rocq - Proof Automation for Dependent Type Theory

248

Contributors

c-cube

1,436 commits

blanchette

45 commits

hargoniX

18 commits

fpottier

1 commits

Languages

OCaml

97.3%

SMT

2.2%