Heifer is a new verifier for effectful, higher-order OCaml programs.

You will need OCaml 5.

opam install . --deps-only

Use dune exec main/hip.exe $EXAMPLE to run examples. Effect-related programs are in test/evaluation, higher-order programs are in test/examples.

• Development
• Why3
• How the web build works
• Docker packaging