Every claim is scoped
Source snapshots, parameters, assumptions, named bad outputs, reset policy and bounded horizon travel with the result.
Powered by CQ-SAT
Bounded verification that carries its evidence.
Guarded Continuation Checker is an evaluation-ready platform for embedded firmware and RTL. It records the model, assumptions, property, horizon, result and replay evidence, then fails closed to an exact backend outside CQ-SAT's validated regime.
Claim boundary: This is an evaluation-ready research prototype, not certified or production-qualified. A SAFE result is bounded by the reviewed model, assumptions, property and horizon; it is not evidence that an entire device is safe.
Platform architecture
One bounded claim. Two exact routes. One independent check.
Guarded Continuation Checker authenticates the model and obligation, governs resources before solving, and selects CQ-SAT only when a static structural gate admits it. Every other supported case stays on an exact fallback. Both routes must produce evidence that a separate checker can recompute, prove or replay.
Evidence, not assertion
A result you can inspect, replay and independently challenge.
Proof-carrying checks
Deterministic certificates and replayable counterexamples are checked independently of the specialised producer path.
Exact when specialisation ends
A static, explainable gate selects CQ-SAT only in its measured structural regime and otherwise uses persistent CDCL.
A product-shaped example
Infusion-pump configuration safety
Check whether configuration and control logic can reach a declared hazardous delivery state within a reviewed startup and operating horizon, under explicit environmental assumptions.
property over_delivery
result SAFE · bounded
evidence model + assumptions + horizon
review independently replayable
Illustrative workflow only, not a medical-device certification claim.
Independent evaluation
Use your design. Keep your RTL private.
Run the published workflow on a partner-owned ephemeral Linux worker. Return only a non-confidential outcome and suitability assessment.
Read the self-service pathVersioned public reference