Audit Correctness of CBMC backend

RMC uses CBMC as a backend. If CBMC has soundness bugs, RMC will as well.

## Likelihood:

CBMC is a large, complex codebase which has had significant bugs in the past, and will likely continue to do so.

## Mitigation: 

* Careful selection of CBMC versions
* CBMC regression suite

## Path to soundness:

Audit CBMC codebase, trusted model checker.

## Documentation:

