From dffe1c41d712c85f93ba52d7d98323346753adbb Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Thu, 17 Oct 2024 09:08:11 +0100 Subject: [PATCH] Add links for CBMC, the proof README and the Proof Guide document. Signed-off-by: Rod Chapman --- README.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index efb085ac4..b13f70344 100644 --- a/README.md +++ b/README.md @@ -34,9 +34,12 @@ ENVIRONMENT OR TO PROTECT ANY SENSITIVE DATA.** Once we have the first stable ve #### Verification -Mostly TODO. We apply CBMC to verify the absence of UB in a few basic C routines, but the bulk of the C verification +Mostly TODO. We apply [CBMC](https://github.com/diffblue/cbmc) to verify type-safety and the absence of +UB in a few basic C routines, but the bulk of the C verification is outstanding. No formal verification has yet been applied to the backends. +See the [Proof README](cbmc/proofs/README.md) and [Proof Guide](cbmc/proofs/proof_guide.md) for more details. + ### Getting started ### Nix setup