Identified during the 2026 soundness review (#1582, SOUNDNESS.md).
Our use of CBMC focuses on memory safety and type safety — absence of undefined behavior including out-of-bounds access, integer overflow, null pointer dereference, etc. It does not currently verify functional correctness of the C code.
Consider introducing additional verification tooling that allows us to express and verify functional correctness properties for the C code.
Identified during the 2026 soundness review (#1582, SOUNDNESS.md).
Our use of CBMC focuses on memory safety and type safety — absence of undefined behavior including out-of-bounds access, integer overflow, null pointer dereference, etc. It does not currently verify functional correctness of the C code.
Consider introducing additional verification tooling that allows us to express and verify functional correctness properties for the C code.