Proving with agents

Give your AI agent this brief and the path of a proof repository as qp assemble writes it (From a repository to a proof), or follow it yourself; QuickProof does not include the agents we use. qp assemble --templates DIR can put a copy, with the project's names filled in, into every proof repository (The qp command).

Below, a spec is the C program that states a property (qp calls it a law), LAW is the name of one (its file is harness/LAW.c), and LOGICAL is the Coq name of the repository's src/ directory (see _CoqProject). Nothing the agent writes is trusted; the work counts only when qp verify accepts it ("Done"). The spec is not the agent's to change: people review it, because it is exactly what the theorem states.

The theorems#

For each spec LAW the file src/contracts/LAW.v ends with

Theorem LAW : harness_safe whole_prog.
Proof.
Admitted.

whole_prog is the spec linked with the code it calls, and harness_safe whole_prog is VST's whole-program judgement for it. Read through VST's adequacy theorem, it says that no run of the program has undefined behaviour in CompCert's C semantics (x86-64), for every value the nondet_* calls may return (What a proof means has the exact meaning). A failing gp_assert is undefined behaviour, so every assertion holds, and out-of-bounds accesses, uses after free, signed overflow and the like are ruled out. gp_assume(c) cuts off the runs where c is false. quickproof/coq/QuickProof/Contract.v defines the theorem, and Env.v there the specifications of nondet_*, gp_assert, gp_assume, malloc and free. Specs write these two as qp_assert and qp_assume, macros for gp_assert and gp_assume; the Clight, Env.v and older specs use the gp_ names.

Where things are#

• harness/LAW.c: the spec. Read it first.
• The code under test: the C files named in quickproof.conf.
• src/contracts/LAW.v: the contract. Everything above the banner THE THEOREM is generated (the program, whole_prog, and a check of the globals it leaves undefined). Then comes the theorem.
• src/<dir>/code.v: the Clight (CompCert's C dialect) of each C file, generated by clightgen and never edited. The function f is f_f there, its name is _f, its local i is _i, and clightgen's temporaries are _t'1, _t'2, and so on. Each C file is a unit, with a module in src/units/ that defines its CS : compspecs and its program qp. Only the functions of the units named in a contract file's top comment are in whole_prog.
• _CoqProject: src/ is the Coq library LOGICAL, so src/proof/Foo.v is LOGICAL.proof.Foo.
• quickproof/: the framework at the commit the proof is checked with.
• quickproof/examples/ (see its README.md): worked examples, each with the code, the spec in harness/, a VST specification and a body proof per C function in proof/src/proof/, and the proof of main and of the theorem in proof/src/contracts/. rle is a loop over a byte buffer, with malloc, nondet_bytes, qp_assume, qp_assert and free in its spec. adler32 has a functional model in Coq, a buffer split in two and three calls in one spec. find_byte, a search loop that exits early, is the smallest complete example.

What you may change#

• Add Coq files under src/, with specifications and lemmas in src/proof/.
• In src/contracts/LAW.v, add your proof between the generated part and the banner THE THEOREM, and replace the Admitted. of the theorem by a proof (usually Proof. exact LAW_proved. Qed.).

Nothing else. In particular:

• Never change the statement of a theorem, anything above THE THEOREM, the specs, the C code, quickproof/, quickproof.conf, _CoqProject, .gitmodules, or any generated code.v or src/units/*.v.
• Never use Admitted, admit, Axiom, Parameter, Conjecture, or anything else that assumes what it should prove. Only the standard axioms and VST's malloc library are accepted.
• Never rewrite git history, move or delete the tag contract, or commit changes outside src/ other than notes such as COUNTEREXAMPLE.md.
• Do not weaken a specification until it says nothing useful about the code. It only has to be strong enough to prove the fixed theorem, but it must be true of the code.

How to prove a property#

1. Read the spec and the code. Find which C functions the spec calls, directly and indirectly.

2. For each of them, write a VST specification in src/proof/<Name>.v, then prove its body. The file starts like the examples:

   Rocq

   Require Import VST.floyd.proofauto.
   Require Import VST.floyd.VSU.
   Require LOGICAL.units.<Unit>.
   Require Import LOGICAL.<dir>.code.
   #[export] Instance CS : compspecs := LOGICAL.units.<Unit>.CS.
   Definition Vprog : varspecs. mk_varspecs LOGICAL.<dir>.code.prog. Defined.

   A specification:

   Rocq

   Definition f_spec :=
     DECLARE _f
     WITH p: val, sh: share, bs: list Z
     PRE [ tptr tuchar, tulong ]
       PROP (readable_share sh; Zlength bs <= Int64.max_unsigned;
             Forall (fun b => 0 <= b <= Byte.max_unsigned) bs)
       PARAMS (p; Vlong (Int64.repr (Zlength bs)))
       SEP (data_at sh (tarray tuchar (Zlength bs)) (map (fun b => Vint (Int.repr b)) bs) p)
     POST [ tulong ]
       EX r: Z,
       PROP (0 <= r <= Zlength bs)
       RETURN (Vlong (Int64.repr r))
       SEP (data_at sh (tarray tuchar (Zlength bs)) (map (fun b => Vint (Int.repr b)) bs) p).
   Definition Gprog : funspecs := [f_spec].
   Lemma body_f: semax_body Vprog Gprog f_f f_spec.
   Proof. start_function. ... Qed.

   C types in VST: size_t is tulong with values Vlong (Int64.repr n); uint8_t is tuchar and int is tint, both with values Vint (Int.repr n); uint32_t is tuint; a pointer to uint8_t is tptr tuchar. Memory: data_at sh t v p (initialised), data_at_ sh t p (any contents).

3. Write every loop invariant before you prove the loop; most failed attempts come from a weak invariant. It must give the bounds every array access needs and keep what the postcondition needs. Use forward_loop Inv break: Post, or forward_for_simple_bound n Inv for a counting for loop. forward_if needs a join postcondition when both branches continue.

4. Prove main in the contract file against main_spec_std p (with Definition p := whole_prog.). Start with start_function. sep_apply (create_mem_mgr gv)., then use one forward_call per call. The environment functions have the specifications nondet_size_spec, nondet_u8_spec, nondet_u32_spec, nondet_bytes_spec, gp_assume_spec, gp_assert_spec, and malloc_spec'/free_spec' under the names _quickproof_malloc and _quickproof_free. A gp_assert call leaves the obligation that its condition is not zero, and that is where the property is proved. The examples show the whole pattern, including the compspecs of whole_prog and change_composite_env from the unit's CS.

5. Assemble the theorem as the examples do:

   Rocq

   Lemma LAW_proved : harness_safe whole_prog.
   Proof.
     harness_safe_by_specs CS G main_post_TT.
     - reflexivity.
     - entry_shared (semax_body_main_std _ _ p _ _ body_main eq_refl).
       entry_shared F.body_f.                      (one per C function of whole_prog)
       entry_external (@external_ok_size CS).      (one per environment function it calls)
       ...
       apply Forall_nil.
   Qed.

   G lists main's specification (QPmain_spec_ext' p tt main_post_TT), your function specifications and those of the environment functions the program calls.

Useful tactics: forward, forward_call, forward_if, forward_loop, Intros, Exists, entailer!, cancel, sep_apply, list_solve, rep_lia, lia, Znth_map, Int64.unsigned_repr. Unsigned comparisons of size_t appear as Int64.ltu; the examples show how to turn them into < on Z. Several properties, one library explains how one body proof serves several specs.

Checking your work#

Build everything at the root of the repository:

coq_makefile -f _CoqProject -o CoqMakefile
make -f CoqMakefile -j4

The first build also builds the framework's library in quickproof/coq/QuickProof. grep -rn Admitted src shows what is left to prove. After you change a file that others import, build again before you look at the files that import it.

Interactive work is much faster than recompiling. Use any Coq environment that reads _CoqProject: coq-lsp or VsCoq in an editor, or an MCP server for Coq such as rocq-mcp. Without one, put Show. in a proof and compile to print the goals. Only qp verify is the acceptance check.

Done#

The work is done when

quickproof/tools/qp verify .

prints PASS after your changes are committed. It checks everything again on a fresh clone (The qp command). Only proof sources (src/**.v) and notes may have changed since the tag contract. The regenerated Clight and every theorem's statement must be unchanged. Print Assumptions may name only the standard axioms and VST's malloc library. The check fails if the proof's own sources (src/ and the other files of _CoqProject, comments excluded) contain any Admitted, admit, Axiom, Parameter or Conjecture, even in a lemma that no theorem uses; only in a run/prebuild project, a vendored library, are they just listed.

Any other claim of success does not count. Run it at the end, and again after any change.

If the property is false#

A property can be false. If a proof gets stuck because the code really can break the property, look for a concrete input that does it, write it with the reason into COUNTEREXAMPLE.md, and stop. That is a result. Never weaken the property, the spec or the code to get around it. If you can run qp on the project's workspace, qp check NAME LAW runs the spec natively and under CompCert's interpreter, and qp fuzz NAME LAW --libfuzzer searches for a failing input (The qp command).

Running your agent#

The agent needs to read the repository, write files under src/, commit them with git, and run make, coqc and qp verify with the toolchain (Coq 8.20.1, CompCert 3.15, VST 2.15) in its PATH. Allow nothing else. When the toolchain runs in a container, run these commands through it, with the repository mounted at the same path on both sides.

An agent can get stuck on a loop invariant or run out of budget.