Inspired by Emilio Gallego’s guide and repo for developing Coq plugins, I created a template repository showing how one can organize a Coq program verification project according to current best practices, using Coq 8.12:

To go marginally above the toy example level, the project verifies a classic program in C using the Verified Software Toolchain (VST). When compiled with CompCert, the program’s contract - briefly explained below - is therefore guaranteed to hold down to machine code level (under reasonable assumptions).

The project uses continuous integration (CI) on GitHub made possible by recent packaging of CompCert and VST by @MSoegtropIMC and the Coq Docker Action by @erikmd. The project can be built using either coq_makefile or Dune, at the developer’s discretion; CI uses Dune.

The key C function is as follows, adapted from Joshua Bloch’s Java version:

```
int binary_search(int a[], int len, int key) {
int low = 0;
int high = len - 1;
while (low <= high) {
int mid = ((unsigned int)low + (unsigned int)high) >> 1;
int mid_val = a[mid];
if (mid_val < key)
low = mid + 1;
else if (mid_val > key)
high = mid - 1;
else
return mid;
}
return -low - 1;
}
```

The Coq contract for the function follows the informal contract in the Java standard library API closely. More specifically, the array `a`

(Coq integer list) is assumed to be sorted, and the output is either the array index of some element with value equal to the parameter `key`

, or an “insertion point” where such an element would have appeared.

Feedback on the template is welcome, either here or as issues on GitHub.