Skip to content

Commit

Permalink
Add links for CBMC, the proof README and the Proof Guide document.
Browse files Browse the repository at this point in the history
Signed-off-by: Rod Chapman <[email protected]>
  • Loading branch information
rod-chapman committed Oct 17, 2024
1 parent 7fc1030 commit dffe1c4
Showing 1 changed file with 4 additions and 1 deletion.
5 changes: 4 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit dffe1c4

Please sign in to comment.