Install

In Docker:

docker run --rm ghcr.io/genproof/quickproof verify rle

It takes a minute or two on x86-64. bug in place of verify rle shows a failing property.

Proving your own code#

Two step-by-step guides:

• With the Docker image: Prove a property of your own code. new starts a project with your function and a spec, check tests the spec, and prove has an AI agent write the proof.
• Without Docker: From a repository to a proof takes a library from its upstream repository to a checked proof with tools/qp.

Proving with agents is the brief for your agent; ours are not included.

Installing#

On macOS or ARM, use the Docker image. On ARM, Docker runs this x86-64 image under emulation, several times slower. On 64-bit x86 Linux (we test on Ubuntu 24.04):

sudo apt-get update && sudo apt-get install opam gcc make git python3 libgmp-dev pkg-config clang
opam init --bare                        # once per machine; inside a container add --disable-sandboxing
opam switch create quickproof 4.14.2    # CompCert 3.15 needs OCaml 4
eval $(opam env --switch=quickproof)
opam repo add rocq-released https://rocq-prover.org/opam/released
opam install coq.8.20.1 coq-compcert.3.15 coq-vst.2.15 coq-hammer-tactics.1.3.2+8.20

This takes about half an hour, most of it building VST (what each package is for). Then run an example and the tests:

git clone https://github.com/genproof/quickproof-public.git quickproof && cd quickproof
tools/qp examples rle
tests/run.sh