Guarded Continuation Checker, powered by CQ-SAT, is an evaluation-ready, proof-carrying bounded verification platform for embedded firmware and RTL.
GCC authenticates a bounded model and reviewed obligation, governs the complete workload before solving, and returns one of three explicit outcomes:
SAFE: no violation exists inside the declared bounded model;UNSAFE: a shortest counterexample is returned for replay; orREFUSED: a policy, resource or input boundary was exceeded, so no logical answer is claimed.
CQ-SAT is GCC's exact continuation-quotient engine. A static structural gate uses it only inside its validated regime. Supported cases outside that regime remain on an exact portfolio backend.
GCC is an evaluation-ready research prototype. It is not yet a production-qualified or certified verification product, a general-purpose replacement for CDCL SAT solvers, or evidence that P = NP.
The production candidate currently supports bounded firmware and RTL safety checking through firmware CLI contract v2 and RTL artifact schema v4. Research interfaces remain available in the repository but are excluded from that support promise.
Read the exact boundaries before evaluation:
- production support profile;
- production-readiness gap register;
- novelty gap register; and
- security policy and threat model.
The producer and checker are separated by a canonical evidence boundary. The checker binds the original source or model, the complete query, the selected route and its result. Resource refusal never becomes a safety answer.
See architecture and trust boundary for the complete system model.
GCC requires Rust 1.97 or newer. RTL synthesis workflows also require Yosys.
git clone https://github.com/kabudu/guarded-continuation-checker.git
cd guarded-continuation-checker
cargo build --release --locked
cargo test --lockedThe executable is:
target/release/guarded-continuation-checker
The bundled product example starts from SystemVerilog, synthesises an AIGER model in an isolated staging directory, checks the bounded safety property and publishes a source-bound evidence bundle:
./target/release/guarded-continuation-checker \
firmware-rtl-safety-gate \
examples/products/infusion-pump/rtl/safe-controller.sv \
infusion_pump_controller 100 target/firmware-safetyValidate the completed bundle before retention or downstream processing:
./target/release/guarded-continuation-checker \
firmware-artifact-validate target/firmware-safetyExit status 0 means bounded safe, 1 means a violation was found, and 2
means the input or tool failed. The example demonstrates integration mechanics,
not medical-device certification. See the
infusion-pump walkthrough.
./target/release/guarded-continuation-checker \
verify-cq-aiger examples/aiger/counter-overflow-4.aag \
137 10 200000 results/local-aiger-counter.csv \
results/local-aiger-counter-safety.txtGCC supports bounded original five-field ASCII aag and binary aig safety
models. Input-driven or wider models route directly to exact CDCL when they do
not satisfy CQ-SAT's static gate.
The profiled production-candidate binary is built with:
cargo build --release --locked --features production-firmwareIt exposes only:
- production and firmware capability discovery;
- single-file, multi-file, configured and constrained RTL safety gates; and
- evidence-bundle validation.
It rejects predicate, event-contract, BTOR2, revision, controller, MTBDD, counterfactual, causal-analysis and benchmark commands before dispatch. Those are research surfaces, not silently supported product capabilities.
The authoritative command list, version semantics and release gates are in the production support profile.
Completed firmware runs publish deterministic source snapshots, synthesis inputs and logs, the bounded model, signal map, report, metrics, provenance and SHA-256-bound manifest.
Linux is the supported production-evaluation host. Its hostile-RTL profile enforces process-tree termination, time, output-file and address-space limits. macOS remains supported for development but does not claim hard memory containment.
SHA-256 detects changes relative to a trusted manifest; it is not a signature. Review RTL artifact schema v4 and the isolation profile before processing untrusted RTL.
Self-service evaluators can select their own firmware or RTL designs, follow the repository procedures and report only outcome and suitability:
- design-partner brief;
- Linux evaluation bundle;
- pilot intake template;
- outcome report template; and
- external evidence protocol.
Independent acceptance remains a release gate. Repository examples and hosted CI runs do not substitute for external evaluation.
The repository retains experimental mechanisms, closest baselines, negative results and retractions. Recent compiled-firmware work includes:
- a source-bound MMIO-to-RTL certificate that composes exact compiled-firmware behavior with independently rebuilt RTL members;
- a dense decode graph reproduced on pinned public Zephyr firmware across arm64 and Linux x86-64; and
- an OpenSBI successor-index replay retained as a negative result after it missed the frozen improvement gate.
These results narrow the next experiments. They do not alter the supported product profile or create a production claim.
See the documentation map, findings and research roadmap for the complete record.
src: library, checker, CLI and research backends.examples/products: product-shaped evaluation examples.examples: executable verification and research probes.corpus: pinned public firmware and RTL inputs.docs: contracts, architecture, qualification evidence and research.results: curated machine-readable evidence supporting bounded claims.scripts: reproduction, qualification and release tooling.
- Documentation map
- Website
- Rust API documentation
- Operations
- Reproducibility
- Contributing
- Brand and naming
Licensed under the Apache License 2.0. See LICENSE.
See CITATION.cff.