Identified during the 2026 soundness review (#1582, SOUNDNESS.md).
CBMC proof configurations (Makefiles, harness settings, unwinding bounds, etc.) are currently specified in a format that is not easily machine-parseable or human-reviewable in aggregate. This makes it difficult to audit the configuration for soundness.
Derive the CBMC configuration from a structured, machine- and human-readable source to enable automated analysis and easier review.
Identified during the 2026 soundness review (#1582, SOUNDNESS.md).
CBMC proof configurations (Makefiles, harness settings, unwinding bounds, etc.) are currently specified in a format that is not easily machine-parseable or human-reviewable in aggregate. This makes it difficult to audit the configuration for soundness.
Derive the CBMC configuration from a structured, machine- and human-readable source to enable automated analysis and easier review.