Proof evaluation
This is a check list intended for
 proof writers to use before checking a proof into a repository and
 proof reviewers to use during the code review of a pull request containing a proof.
This check list is intended to ensure clear answers to two questions:
 What properties are being checked by the proof?
 What assumptions are being made by the proof?
and that these answers can be found in one of three places:
 The proof harness,
 The proof makefiles (and, with the starter kit, these makefiles are the proof Makefile, the project Makefileprojectdefines, and the project Makefile.common), and perhaps
 The proof readme file.
The best practices for writing a proof are described in Write a good proof. Reviewers should keep these best practices in mind when reading a proof. We recommend that any deviations from best practices be explained in the readme file.
Properties checked
Check the following:

All of the standard propertychecking flags are used:
* boundscheck * conversioncheck * divbyzerocheck * floatoverflowcheck * mallocfailnull * mallocmayfail * nancheck * pointercheck * pointeroverflowcheck * pointerprimitivecheck * signedoverflowcheck * undefinedshiftcheck * unsignedoverflowcheck
Note that the starter kit uses these flags by default. The properties checked by these flags is documented on the CPROVER website. Note, however, that a developer may disable any one of these flags by editing project Makefile.common or by setting a makefile variable to the empty string (as in
CBMC_FLAG_MALLOC_MAY_FAIL =
) in the project Makefileprojectdefines or a proof Makefile. These are the places to look for deviations. 
All deviations from the standard propertychecking flags are documented.
There are valid reasons to omit flags either for a project or for an individual proof. But the decision and the reason for the decision must be documented either in a project readme or a proof readme file.
CBMC checks assertions in the code. This is understood and need not be documented.
Assumptions made
Check the following:

All nontrivial data structures have an
ensure_allocated
function as described in the training material.Feel free to use any naming scheme that makes sense for your project  some projects use
allocate_X
in place ofensure_allocated_X
 but be consistent. 
All nontrivial data structures have an
is_valid()
predicate as described in the training material for every nontrivial data structure. 
All definitions of
ensure_allocated
functions andis_valid
predicates appear in a common location.These definitions are most commonly stored in the
proofs/sources
subdirectory of the starter kit. Definitions are stored here and used consistently in the proofs. 
All pointers passed as input are allocated on the heap with
malloc
.One common mistake is to allocate a buffer
buf
on the stack and to pass&buf
to the function under test in the proof harness. This prevents the proof from considering the case of a NULL pointer. 
All instances of
__CPROVER_assume
appear in a proof harness.Note that some exceptions are required. For example, it may be necessary in an
ensure_allocated
to assumelength < CBMC_MAX_OBJECT_SIZE
before invokingmalloc(length)
to avoid a false positive about malloc'ing a toobig object. But every instance of__CPROVER_assume
in supporting code should be copied into the proof harness. The goal is for all proof assumptions to be documented in one place. 
All preprocessor definitions related to bounds on input size or otherwise related to proof assumptions appear in the proof Makefile.
In particular, do not embed definitions in the supporting code or header files. The goal is for all proof assumptions to be documented in one place.

Confirm that all stubs used in the proof are acceptable abstractions of the actual code.
Acceptable could mean simply that every behavior of the original code is a behavior of the abstraction.
Results checked
Look at the report in the checks attached to the pull request.

Confirm that the coverage is acceptable and confirm that the readme file explains the reason for any lines not covered.

Confirm that the list of missing functions is acceptable.

Confirm that there are no errors reported.
Other things to consider

Consider writing function contracts for the function under test as described in Write a good proof. The check list above ensures that the properties (including the assumptions about the input) that must be true before function invocation are clearly stated in the proof harness. Consider adding a statement of what properties must be true after function invocation as assertions at the end of the proof harness.

Consider adding the assumptions made by the proof harness for a function under test to the source code for the function in the form of assertions in the code. This will validate that the assumptions made by the proof of a function are satisfied by each invocation of the function (at least during testing).