{
  "lab_version": "0.3.0",
  "evidence_status": "FINITE_MODEL_AND_SYNTHETIC_DESIGN_ONLY",
  "model_calls": 0,
  "checker_results": [
    {
      "status": "FINITE_MODEL_CERTIFIED",
      "policy": "history_gate",
      "states": 51,
      "edges": 663,
      "allowed_transfer_edges": 3,
      "allowed_cooling_edges": 15,
      "scope": "PINNED_FINITE_MODEL_ONLY",
      "liveness_proved": false,
      "runtime_refinement_proved": false
    },
    {
      "status": "FINITE_MODEL_CERTIFIED",
      "policy": "ordinary_gate",
      "states": 51,
      "edges": 663,
      "allowed_transfer_edges": 3,
      "allowed_cooling_edges": 15,
      "scope": "PINNED_FINITE_MODEL_ONLY",
      "liveness_proved": false,
      "runtime_refinement_proved": false
    },
    {
      "status": "COUNTEREXAMPLE_VERIFIED",
      "policy": "current_only",
      "steps": 3,
      "scope": "PINNED_FINITE_MODEL_ONLY"
    },
    {
      "status": "COUNTEREXAMPLE_VERIFIED",
      "policy": "report_gate",
      "steps": 3,
      "scope": "PINNED_FINITE_MODEL_ONLY"
    },
    {
      "status": "COUNTEREXAMPLE_VERIFIED",
      "policy": "always_continue",
      "steps": 2,
      "scope": "PINNED_FINITE_MODEL_ONLY"
    },
    {
      "status": "FINITE_MODEL_CERTIFIED",
      "policy": "deny_all",
      "states": 51,
      "edges": 663,
      "allowed_transfer_edges": 0,
      "allowed_cooling_edges": 0,
      "scope": "PINNED_FINITE_MODEL_ONLY",
      "liveness_proved": false,
      "runtime_refinement_proved": false
    }
  ],
  "conventional_baseline_equivalent": true,
  "all_expected_outcomes_reproduced": true,
  "warning": "A reproduced counterexample is an expected policy failure, not a safety certification. No runtime-code refinement has been proved."
}
