Identified during the 2026 soundness review (#1582, SOUNDNESS.md).
HOL Light and CBMC verify different properties of the codebase, but their specifications overlap — for example, both encode functional behavior of assembly routines and their C callers. Currently, there is no machine-checked link ensuring consistency between HOL Light specifications and CBMC contracts. An inconsistency between them could mean that properties verified in isolation do not compose into an end-to-end guarantee.
Establish a machine-checked connection between the two verification frameworks.
Identified during the 2026 soundness review (#1582, SOUNDNESS.md).
HOL Light and CBMC verify different properties of the codebase, but their specifications overlap — for example, both encode functional behavior of assembly routines and their C callers. Currently, there is no machine-checked link ensuring consistency between HOL Light specifications and CBMC contracts. An inconsistency between them could mean that properties verified in isolation do not compose into an end-to-end guarantee.
Establish a machine-checked connection between the two verification frameworks.