Note presence of Proof README and Proof Guide and add links to these …

…documents.

Signed-off-by: Rod Chapman <[email protected]>

README.md

@@ -33,7 +33,6 @@ At this point, we do not provide implementations optimized for memory usage (cod
 
 Eventually, we aim to unify the (shared) C-part of the implementations provided by **mlkem-c-aarch64** with the implementations in [mlkem-c-generic](https://github.com/pq-code-package/mlkem-c-generic). Initially, however, we will allow some divergence, e.g. to explore interfaces to 2-/4-/8-way parallel Keccak implementations which are essential for high-performance implementations of MLKEM.
 
-
 ## Current state
 
 **mlkem-c-aarch64** is currently a work in progress and we do not recommend relying on it at this point.
@@ -66,6 +65,14 @@ After running `nix develop` you should automatically have a number of support sc
 - [`format`](scripts/format) formats all files. The format is enforced by our CI, so you should run this script prior to committing.
 - [`tests`](scripts/tests) run functional, kat tests natively or emulate them using `QEMU`. For information on how to use the script, please refer to the `--help` option.
 
+## Formal Verification
+
+We are currently aiming to prove that the C code is memory-safe, type-safe, and free of undefined behaviour, using the [CBMC](https://github.com/diffblue/cbmc) verification tool.
+The nix environment automatically installs CBMC and related tools.
+
+See the [Proof README](cbmc/proofs/README.md) and [Proof Guide](cbmc/proofs/proof_guide.md) for more details.
+
+
 ## Call for contributors
 
 We are actively seeking contributors who can help us build **mlkem-c-aarch64**.

cbmc/proofs/README.md

@@ -11,7 +11,8 @@ of certain classes of undefined behaviour for parts of the C-code in MLKEM-C-AAr
 Proofs are organized by functions, with the harnesses and proofs for each function
 in a separate directory.
 
-TODO: Provide more information about CBMC and the properties it proves
+See the [Proof Guide](proof_guide.md) for a walkthrough of how to use CBMC and
+develop new proofs.
 
 # Usage
 
@@ -26,6 +27,10 @@ If `GITHUB_STEP_SUMMARY` is set, the proof summary will be appended to it.
 
 # Covered functions
 
-The following functions are currently covered:
+Each proved function has a eponymous sub-directory of its own. The shell command
 
-- `poly.c`: `poly_compress`
+```
+find . -name cbmc-proof.txt
+```
+
+yields a list of the subdirectories, and thus function names, that have a proof.