GCC 0.32.0 connects bounded compiled-firmware evidence to source-bound RTL behavior and extends exact firmware replay across independently maintained Zephyr and OpenSBI sources.
Release highlights
- Firmware-to-RTL certificates: Bind the complete 256-input OpenTitan PWM firmware partition to six source-derived RTL members in one canonical, independently checkable artifact.
- Maintained-tool agreement: Reconstruct the same bounded semantics with pinned angr, Yosys and Z3 without consuming GCC certificates or replayed traces.
- Fail-closed trust boundary: Reject all retained source, codec, identity and checksum-valid semantic forgeries before returning a verification answer.
- Public firmware transfer: Reproduce exact dense decode-graph behavior for the Zephyr v4.2.0 SiFive GPIO driver on arm64 and hosted Linux x86-64.
- RV32M arithmetic: Add exact RISC-V division and remainder semantics, including divide-by-zero and signed-overflow cases, to admit the unchanged OpenSBI UART cohort.
- Measured limits retained: Keep the existing dense route because OpenSBI successor-index replay missed its predeclared 20 percent improvement gate.
- Research transport refresh: Update optional QatQ transport compatibility to 0.3.0 while keeping it outside the production firmware feature.
Bounded evidence
| Result | Retained observation |
|---|---|
| OpenTitan firmware inputs | 256 |
| Reconstructed RTL members | 6 |
| RTL transitions | 198 |
| RTL observations | 204 |
| Zephyr graph nodes and edges | 94 and 99 |
| Zephyr hostile refusals | 22,908 |
| OpenSBI hostile refusals | 112,072 |
The maintained OpenTitan comparison agrees byte-for-byte across two clean cycles and refuses all eleven retained drift controls. The measurements apply only to the pinned sources, bounded callers, tool versions and observation windows documented in the repository.
Install
Complete research build:
cargo install guarded-continuation-checker --version 0.32.0 --lockedFrozen firmware and RTL profile:
cargo install guarded-continuation-checker --version 0.32.0 --locked \
--features production-firmware
guarded-continuation-checker production-profile-versionStatus and scope
GCC is an evaluation-ready research prototype, not a production-qualified or certified verification product.
This release establishes a bounded proof-carrying firmware-to-RTL composition path and exact public-source firmware replay. It does not claim arbitrary firmware or RTL support, a universal solver speedup, or production suitability without independent evaluation.