Workpack P6
File publique des 0 exigences P6 restantes : priorités, lanes de fermeture et actions requises, sans claim de clôture P6.
p6_local_audit_closure_workpack_only_no_gap_closure_claim
Work the remaining queue by lane: primary evidence, scope activation, requirement rewrite, assumption acceptance, and re-audit of present artifacts; then rerun the P6 audit and sovereign readiness gates.
Lanes de fermeture
Groupes
Classes de remédiation
Admissions formelles étroites
Les exigences GL-181, GL-182, GL-183, GL-184 et GL-191 sont admises comme résultats formels locaux bornés. Cette admission ne prouve ni l'équivalence avec l'implémentation de production, ni la clôture P6 globale.
·
·
Suite sûreté code bornée GL-028..GL-033/GL-037
Ces sept preuves locales bornées rejouent Lean, scans source et probes rustc ciblés pour arithmétique, bornes, panic surface et initialisation. Elles rendent la revue plus exploitable, mais elles ne remplacent pas une preuve whole-program ni une clôture P6.
GL-028bornéno P6 closure
Integer overflow
ready=false · lean=false · typed=false · checks=false
·
GL-029bornéno P6 closure
Integer underflow
ready=false · lean=false · typed=false · checks=false
·
GL-030bornéno P6 closure
Division by zero
ready=false · lean=false · typed=false · checks=false
·
GL-031bornéno P6 closure
Invalid bit shift
ready=false · lean=false · typed=false · checks=false
·
GL-032bornéno P6 closure
Array bounds
ready=false · lean=false · typed=false · checks=false
·
GL-033bornéno P6 closure
Panic surface
ready=false · lean=false · typed=false · checks=false
·
GL-037bornéno P6 closure
Definite initialization
ready=false · lean=false · typed=false · checks=false
·
bounded_code_safety_suite_local_lean_scan_and_rustc_probes_only_no_whole_program_p6_closure_claim
GL-034 sûreté mémoire unsafe
Premier item critique rendu exécutable : chaque boundary unsafe est dans une queue Creusot/Ruler, mais le théorème mémoire reste ouvert tant que le toolchain requis ne rejoue pas la preuve.
·
·
·
·
GL-039 zéroisation anti-DSE
Deuxième item critique rendu public : Lean rejoue le modèle borné, le probe assembleur vérifie les stores zéro volatiles et l'absence de memset éliminable, mais cela ne prouve pas encore la zéroisation whole-program.
·
·
GL-181 modèle Tamarin échange de clés
Le modèle symbolique d'échange de clés a été rejoué par Tamarin et tous ses lemmes exigés sont vérifiés. Ce résultat porte sur le workbench formel ; il ne constitue pas une preuve PFS, mTLS/mAK ou production de bout en bout.
·
·
GL-182 modèle ProVerif échange de clés
ProVerif a rejoué le secret applicatif et les deux correspondances d'authentification du modèle symbolique. Cette admission étroite ne prouve ni la sécurité calculatoire, ni la PFS après compromission, ni l'authentification mutuelle de la pile de production.
·
·
·
GL-183 preuve PFS Tamarin
Le modèle symbolique PFS fail-closed a été rejoué par Tamarin et tous ses lemmes exigés sont vérifiés. La preuve reste limitée au workbench et ne ferme pas la PFS de l'implémentation de production.
·
·
GL-184 authentification mutuelle Tamarin
Le modèle mTLS/mAK lie les signatures initiateur/répondeur aux événements d'accord mutuel ; Tamarin a rejoué et vérifié tous les lemmes exigés. La correspondance avec la pile mTLS/mAK de production reste ouverte.
·
·
GL-185/186/187/188/189 résistance attaques protocole
Les propriétés MitM, replay, désynchronisation, downgrade et indépendance de session ont été rejouées dans Tamarin, puis leurs contrats Lean ont été vérifiés. Les preuves de résistance de la pile de production restent ouvertes.
·
·
·
GL-190 dérivation HKDF
Le modèle HKDF lie Extract, Expand, salt, session, transcript et labels de domaine ; Tamarin et Lean ont rejoué les obligations exigées. Une preuve calculatoire complète de sécurité HKDF/HMAC pour la production n'est pas encore admise.
·
·
·
GL-191 modèle CSPRNG/PRNG
Le modèle CSPRNG expose initialisation, génération, révélation d'état, reseed et sortie post-reseed ; Tamarin a vérifié tous les lemmes exigés. Les garanties forward/backward de l'implémentation de production ne sont pas déduites de ce seul modèle.
·
·
GL-192 forward resistance CSPRNG
Le modèle lie sortie passée, avancement d'état, effacement du prédécesseur et révélation ultérieure de l'état courant ; Tamarin et Lean ont vérifié les obligations exigées. La preuve forward-resistance de production reste ouverte.
·
·
·
GL-193 backward resistance CSPRNG
Le modèle lie compromission d'état, injection de nouvelle entropie, mix de récupération et sortie post-récupération ; Tamarin et Lean ont vérifié les obligations exigées. La preuve de break-in recovery de production reste ouverte.
·
·
·
GL-194 PRG/DRBG borné
La propriété PRG/DRBG sous hypothèses déclarées, sa frontière de min-entropie et sa politique de reseed ont été rejouées dans Tamarin et Lean. Aucune preuve quantitative de min-entropie ni certification DRBG/PRG de production n'en découle.
·
·
·
GL-195/196/198/199 entropie états atomicité
Le modèle de min-entropie déclarée, conditionnement borné, rejet des états invalides et atomicité commit/abort a été rejoué dans Tamarin et Lean. Les preuves quantitatives et d'atomicité de la pile de production restent ouvertes.
·
·
·
GL-197 cycle de vie clés
Le modèle lie génération, activation, rotation, retraite, révocation terminale et refus d'usage après révocation ; Tamarin et Lean ont vérifié les obligations exigées. La machine à états de production n'est pas encore couverte par une preuve de raffinement.
·
·
·
GL-200 composition globale
Le modèle de composition lie protocole, RNG/cycle de vie, implémentation, raffinement binaire et reçu cible ; Tamarin et Lean ont vérifié ses obligations de workbench. Les sous-preuves de production et la composition bout-en-bout restent ouvertes.
·
·
·
GL-205 théorème système borné
Douzième item critique préparé : le théorème système S0 est formulé sous H1..H13 avec structure ε_total et dépendances méta rejouées. Il reste fail-closed tant qu'un paquet de preuve S0 theorem-grade, une borne numérique ε_total et les fermetures production des composants ne sont pas admis.
·
·
·
·
GL-206 borne ε_total
Treizième item critique préparé : la borne composée ε_total est tracée terme par terme dans une somme explicite sans bucket caché. Elle reste fail-closed tant que les bornes numériques locales, l'arithmétique totale et le contrôle machine ne sont pas admis.
·
·
·
GL-208 raffinement bout-en-bout
Quatorzième item critique préparé : la couverture de raffinement C1..C6, l'audit local, les dépendances GL-201/GL-203 et le contrat Lean sont rejoués. Le bloc reste fail-closed tant qu'une preuve mécanisée du binaire exécuté, liée au hash de production et au domaine de validité, n'est pas admise.
·
·
·
·
GL-207 multi-utilisateur / multi-session
Quinzième item préparé : le theorem cible S1 est cadré au-dessus de S0 pour les utilisateurs concurrents, sessions, époques de révocation et tentatives de rejeu. Le bloc reste fail-closed tant qu'une preuve theorem-grade S1, une borne probabiliste multi-utilisateur et une preuve de concurrence de flotte production ne sont pas admises.
·
·
·
·
GL-214 invariants API / typestate
Seizième item préparé : l'artefact d'intégration manquant est restauré, les 11 refus documentés sont comptés, les 12 probes API sont rejouées, et le contrat Lean borne strictement le bloc. Il reste fail-closed tant qu'une preuve typestate couvrant toute l'API publique n'est pas admise.
·
·
·
·
·
GL-215 fermeture etats
Dix-septième item préparé : l'inventaire des automates critiques, les marqueurs de transition CP-ABE/GPQVE, les prérequis GL-197/198/199, deux tests Rust ciblés et le contrat Lean sont rejoués. Le bloc reste fail-closed tant qu'une preuve de totalisation de tous les états critiques n'est pas admise.
·
·
·
·
GL-218 pont logiciel / materiel
Dix-huitième item préparé : le pont entre S0, A_sc, epsilon_side_channel, les hypothèses H9/H11/H12, le modèle de fautes et la couverture plateforme locale est rejoué. Les prérequis side-channel GL-163/164/165/166 restent affichés comme bloqueurs tant qu'aucune preuve formelle logiciel-matériel n'est admise.
·
·
·
·
·
·
GL-224 politique fail-safe
Dix-neuvieme item prepare : les refus selectionnes couvrent decapsulation exacte, verification protocole, entropie et validation API avec quatre replays Rust et un contrat Lean borne. Le bloc reste fail-closed tant qu'une preuve formelle unique de non-exploitabilite n'est pas admise.
·
·
·
·
GL-225 contrat assurance
Vingtieme item prepare : le contrat d'assurance publie et rejoue l'enonce S0, les hypotheses H1..H13, le perimetre, les exclusions et les artefacts de verification. Les prerequis GL-205 et GL-206 restent visibles comme non clos : aucun S0 theorem-grade, aucune borne epsilon_total numerique et aucune fermeture P6 ne sont revendiques.
·
·
·
·
·
·
GL-161 branchements secrets Binsec/Rel
Treizième item critique préparé : le contrat Binsec/Rel classe entrées secrètes, forme publique, conditions de branchement, sauts indirects et bornes de boucle pour viser l'absence de branchements dépendants des secrets. Il reste fail-closed tant que binsec -sse -checkct ne rejoue pas l'artefact sur le binaire production et la plateforme cible.
·
·
·
GL-162 accès mémoire secrets Binsec/Rel
Treizième item critique préparé : le contrat Binsec/Rel classe adresses de load/store, pointeurs de base, offsets, indices de table, lignes cache et forme mémoire publique pour viser l'absence d'accès mémoire dépendants des secrets. Il reste fail-closed tant que binsec -sse -checkct ne rejoue pas l'artefact sur le binaire production et la plateforme cible.
·
·
·
GL-121 conformité FIPS 203 ML-KEM
Quatorzième item critique préparé : les sources tierces ML-KEM exactes sont présentes, liées localement par Cargo et vérifiées contre les archives verrouillées avec un probe de falsification. Le contrat Lean rejoue la forme publique ML-KEM-768/1024, mais la limite vendor-backed/non-autonomous reste explicite et aucune preuve formelle stricte FIPS 203 n'est admise.
·
·
·
·
GL-125/126/127 algorithmes ML-KEM
Quinzième item critique préparé : le source vendor exact est vérifié contre l'archive verrouillée, les bindings KeyGen, Encaps et Decaps du wrapper sont tracés vers ce backend, et le contrat Lean rejoue la frontière algorithmique. Il reste fail-closed tant qu'une preuve formelle KeyGen/Encaps/Decaps de production n'est pas admise.
·
·
·
·
GL-141/142/143/144 ML-DSA FIPS 204
Seizième item critique préparé : les paramètres ML-DSA-65/87, les surfaces KeyGen-derived Sign/Verify, le certificat natif, le corpus de rejet et le contrat Lean sont reliés au profil FIPS 204. Il reste fail-closed tant qu'une preuve stricte de conformité FIPS 204 et les preuves formelles ML-DSA.KeyGen/Sign/Verify de production ne sont pas admises.
·
·
·
·
Tête critique de file
Pare-feu de claims
JSON public
{
"version": "guardlatice/public-p6-local-audit-workpack/v1",
"generated_at": "2026-07-09T10:39:06Z",
"public_product_anchor": "https://ddbs.guardlatice.com/",
"page": "https://ddbs.guardlatice.com/p6/workpack",
"machine_readable": "https://ddbs.guardlatice.com/api/public/p6/local-audit-workpack",
"source_audit_summary": "",
"source_audit_summary_sha256": "",
"source_workpack": "",
"source_workpack_present": false,
"source_workpack_sha256": "",
"source_matrix_version": "",
"first_audit_path": "",
"first_audit_sha256": "",
"model_path": "",
"model_sha256": "",
"closure_workpack_ready": false,
"queue_item_count": 0,
"total_open_requirement_count": 0,
"priority_counts": {},
"closure_lane_counts": {},
"group_counts": {},
"audit_status_counts": {},
"formal_model_admission": {
"current": false,
"summary": "",
"summary_sha256": "",
"register": "",
"register_sha256": "",
"admitted_requirement_ids": [],
"admitted_requirement_count": 0,
"counts_as_global_p6_closure": false,
"production_security_claim_allowed": false
},
"theorem_proof_admission": {
"current": false,
"summary": "",
"summary_sha256": "",
"register": "",
"register_sha256": "",
"failclosed_probe": "",
"failclosed_probe_sha256": "",
"failclosed_probe_current": false,
"failclosed_probe_case_count": 0,
"failclosed_probe_valid_case_count": 0,
"failclosed_probe_negative_case_count": 0,
"failclosed_probe_all_cases_passed": false,
"admitted_requirement_ids": [],
"admitted_requirement_count": 0,
"production_implementation_equivalent": false,
"counts_as_global_p6_closure": false,
"production_security_claim_allowed": false
},
"remediation_class_counts": {},
"group_lane_counts": {},
"group_status_counts": {},
"critical_item_count": 0,
"high_item_count": 0,
"medium_item_count": 0,
"gl_bounded_code_safety_suite": {
"version": "guardlatice/p6-local-audit-bounded-code-safety-suite/v1",
"suite_title": "Suite sûreté code bornée GL-028..GL-033/GL-037",
"suite_ready": false,
"item_count": 7,
"ready_item_count": 0,
"bounded_evidence_ready_count": 0,
"lean_replay_ok_count": 0,
"typed_evidence_compiles_count": 0,
"check_ok_count": 0,
"claim_boundary_failclosed_count": 0,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"whole_program_safety_claim_allowed": false,
"claim_boundary": "bounded_code_safety_suite_local_lean_scan_and_rustc_probes_only_no_whole_program_p6_closure_claim",
"items": [
{
"id": "GL-028",
"title": "Integer overflow",
"version": "",
"summary": "",
"summary_sha256": "",
"ready_key": "gl028_integer_overflow_gate_ready",
"gate_ready": false,
"lean_available": false,
"lean_replay_ok": false,
"lean_source_path": "",
"lean_source_sha256": "",
"ops_lean_replay_json_sha256": "",
"ops_lean_replay_md_sha256": "",
"source_scan_json_sha256": "",
"typed_evidence_compiles": false,
"claim_boundary": "",
"counts_as_p6_closure": false,
"p6_closure_claim_allowed": false,
"true_checks": {
"lean_replay_ok": false,
"rustc_rejects_const_integer_overflow": false,
"rust_checked_add_probe_ok": false,
"source_typed_literal_overflow_absent": false,
"typed_evidence_compiles": false
},
"false_checks": {},
"zero_counts": {},
"counts": {
"source_rust_file_count": 0,
"source_arithmetic_token_count": 0,
"source_checked_arithmetic_call_count": 0,
"source_wrapping_arithmetic_call_count": 0,
"source_typed_integer_literal_count": 0,
"source_typed_literal_overflow_count": 0
},
"check_ok": false,
"bounded_evidence_ready": false
},
{
"id": "GL-029",
"title": "Integer underflow",
"version": "",
"summary": "",
"summary_sha256": "",
"ready_key": "gl029_integer_underflow_gate_ready",
"gate_ready": false,
"lean_available": false,
"lean_replay_ok": false,
"lean_source_path": "",
"lean_source_sha256": "",
"ops_lean_replay_json_sha256": "",
"ops_lean_replay_md_sha256": "",
"source_scan_json_sha256": "",
"typed_evidence_compiles": false,
"claim_boundary": "",
"counts_as_p6_closure": false,
"p6_closure_claim_allowed": false,
"true_checks": {
"lean_replay_ok": false,
"rustc_rejects_const_integer_underflow": false,
"rust_checked_sub_probe_ok": false,
"source_typed_literal_underflow_absent": false,
"typed_evidence_compiles": false
},
"false_checks": {},
"zero_counts": {},
"counts": {
"source_minus_token_count": 0,
"source_checked_sub_call_count": 0,
"source_wrapping_sub_call_count": 0,
"source_saturating_sub_call_count": 0,
"source_overflowing_sub_call_count": 0,
"source_typed_integer_literal_count": 0,
"source_same_type_typed_literal_subtraction_count": 0,
"source_typed_literal_underflow_count": 0
},
"check_ok": false,
"bounded_evidence_ready": false
},
{
"id": "GL-030",
"title": "Division by zero",
"version": "",
"summary": "",
"summary_sha256": "",
"ready_key": "gl030_division_by_zero_gate_ready",
"gate_ready": false,
"lean_available": false,
"lean_replay_ok": false,
"lean_source_path": "",
"lean_source_sha256": "",
"ops_lean_replay_json_sha256": "",
"ops_lean_replay_md_sha256": "",
"source_scan_json_sha256": "",
"typed_evidence_compiles": false,
"claim_boundary": "",
"counts_as_p6_closure": false,
"p6_closure_claim_allowed": false,
"true_checks": {
"lean_replay_ok": false,
"rustc_rejects_const_zero_divisor": false,
"rust_nonzero_divisor_probe_ok": false,
"source_literal_zero_divisor_absent": false,
"typed_evidence_compiles": false
},
"false_checks": {},
"zero_counts": {},
"counts": {
"source_division_token_count": 0,
"source_remainder_token_count": 0,
"source_literal_zero_division_token_count": 0,
"source_literal_zero_remainder_token_count": 0,
"source_literal_zero_divisor_token_count": 0
},
"check_ok": false,
"bounded_evidence_ready": false
},
{
"id": "GL-031",
"title": "Invalid bit shift",
"version": "",
"summary": "",
"summary_sha256": "",
"ready_key": "gl031_invalid_bit_shift_gate_ready",
"gate_ready": false,
"lean_available": false,
"lean_replay_ok": false,
"lean_source_path": "",
"lean_source_sha256": "",
"ops_lean_replay_json_sha256": "",
"ops_lean_replay_md_sha256": "",
"source_scan_json_sha256": "",
"typed_evidence_compiles": false,
"claim_boundary": "",
"counts_as_p6_closure": false,
"p6_closure_claim_allowed": false,
"true_checks": {
"lean_replay_ok": false,
"rustc_rejects_const_invalid_shift": false,
"rust_checked_shift_probe_ok": false,
"source_literal_invalid_shift_absent": false,
"typed_evidence_compiles": false
},
"false_checks": {},
"zero_counts": {},
"counts": {
"source_shift_token_count": 0,
"source_literal_shift_rhs_ge_128_count": 0,
"source_typed_literal_lhs_invalid_shift_count": 0,
"source_cast_lhs_invalid_shift_count": 0,
"source_literal_invalid_shift_token_count": 0
},
"check_ok": false,
"bounded_evidence_ready": false
},
{
"id": "GL-032",
"title": "Array bounds",
"version": "",
"summary": "",
"summary_sha256": "",
"ready_key": "gl032_array_bounds_gate_ready",
"gate_ready": false,
"lean_available": false,
"lean_replay_ok": false,
"lean_source_path": "",
"lean_source_sha256": "",
"ops_lean_replay_json_sha256": "",
"ops_lean_replay_md_sha256": "",
"source_scan_json_sha256": "",
"typed_evidence_compiles": false,
"claim_boundary": "",
"counts_as_p6_closure": false,
"p6_closure_claim_allowed": false,
"true_checks": {
"lean_replay_ok": false,
"rustc_rejects_const_out_of_bounds": false,
"rust_checked_index_probe_ok": false,
"source_literal_array_index_oob_absent": false,
"typed_evidence_compiles": false
},
"false_checks": {},
"zero_counts": {
"source_get_unchecked_call_count": 0,
"source_literal_array_index_oob_count": 0
},
"counts": {
"source_index_syntax_token_count": 0,
"source_get_call_count": 0,
"source_get_unchecked_call_count": 0,
"source_literal_array_index_expression_count": 0,
"source_literal_array_index_oob_count": 0
},
"check_ok": false,
"bounded_evidence_ready": false
},
{
"id": "GL-033",
"title": "Panic surface",
"version": "",
"summary": "",
"summary_sha256": "",
"ready_key": "gl033_panic_surface_gate_ready",
"gate_ready": false,
"lean_available": false,
"lean_replay_ok": false,
"lean_source_path": "",
"lean_source_sha256": "",
"ops_lean_replay_json_sha256": "",
"ops_lean_replay_md_sha256": "",
"source_scan_json_sha256": "",
"typed_evidence_compiles": false,
"claim_boundary": "",
"counts_as_p6_closure": false,
"p6_closure_claim_allowed": false,
"true_checks": {
"lean_replay_ok": false,
"source_library_runtime_direct_panic_like_absent": false,
"typed_evidence_compiles": false
},
"false_checks": {
"gl033_panic_freedom_claim_allowed": false
},
"zero_counts": {},
"counts": {
"source_panic_macro_count": 0,
"source_unwrap_call_count": 0,
"source_expect_call_count": 0,
"source_todo_macro_count": 0,
"source_unimplemented_macro_count": 0,
"source_unreachable_macro_count": 0,
"source_assert_macro_count": 0,
"source_debug_assert_macro_count": 0,
"source_direct_panic_like_total_count": 0,
"source_library_runtime_direct_panic_like_count": 0,
"source_library_runtime_assertion_macro_count": 0,
"source_library_runtime_panic_like_total_count": 0
},
"check_ok": false,
"bounded_evidence_ready": false
},
{
"id": "GL-037",
"title": "Definite initialization",
"version": "",
"summary": "",
"summary_sha256": "",
"ready_key": "gl037_definite_initialization_gate_ready",
"gate_ready": false,
"lean_available": false,
"lean_replay_ok": false,
"lean_source_path": "",
"lean_source_sha256": "",
"ops_lean_replay_json_sha256": "",
"ops_lean_replay_md_sha256": "",
"source_scan_json_sha256": "",
"typed_evidence_compiles": false,
"claim_boundary": "",
"counts_as_p6_closure": false,
"p6_closure_claim_allowed": false,
"true_checks": {
"lean_replay_ok": false,
"rustc_rejects_safe_use_before_init": false,
"rustc_accepts_initialized_all_paths": false,
"source_explicit_uninit_primitives_absent": false,
"typed_evidence_compiles": false
},
"false_checks": {},
"zero_counts": {
"source_maybeuninit_count": 0,
"source_mem_uninitialized_count": 0,
"source_assume_init_count": 0,
"source_mem_zeroed_count": 0,
"source_vec_set_len_count": 0,
"source_spare_capacity_mut_count": 0
},
"counts": {
"source_explicit_uninit_primitive_count": 0,
"source_maybeuninit_count": 0,
"source_mem_uninitialized_count": 0,
"source_assume_init_count": 0,
"source_mem_zeroed_count": 0,
"source_vec_set_len_count": 0,
"source_spare_capacity_mut_count": 0
},
"check_ok": false,
"bounded_evidence_ready": false
}
]
},
"gl034_memory_safety_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"contract_source_ready": false,
"contract_doc_path": "",
"contract_doc_sha256": "",
"contract_doc_ready": false,
"lean_contract_path": "",
"lean_contract_sha256": "",
"lean_contract_terms_present": false,
"lean_replay_ok": false,
"ops_contract_path": "",
"ops_contract_sha256": "",
"ops_contract_ready": false,
"unsafe_boundary_count": 0,
"unsafe_source_file_count": 0,
"proof_queue_item_count": 0,
"verified_boundary_count": 0,
"pending_boundary_count": 0,
"creusot_available": false,
"cargo_creusot_available": false,
"ruler_available": false,
"required_toolchain_available": false,
"memory_safety_theorem_closed": false,
"verified_by_required_toolchain": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"proof_queue_path": "",
"workbench_directory": "",
"evidence_json_path": "",
"verifier_command": "",
"claim_boundary": ""
},
"gl039_zeroization_dse": {
"version": "",
"summary": "",
"summary_sha256": "",
"gate_ready": false,
"lean_available": false,
"lean_replay_ok": false,
"lean_source_path": "",
"lean_source_sha256": "",
"lean_terms_present": false,
"rustc_available": false,
"rust_probe_compile_ok": false,
"rust_probe_asm_path": "",
"rust_probe_asm_sha256": "",
"rust_probe_asm_function_symbol_present": false,
"rust_probe_asm_store_zero_present": false,
"rust_probe_asm_loop_or_branch_present": false,
"rust_probe_asm_memset_absent": false,
"source_zeroize_path": "",
"source_zeroize_sha256": "",
"source_zeroize_uses_write_volatile": false,
"source_zeroize_uses_compiler_fence": false,
"source_zeroize_slice_impl_present": false,
"source_zeroize_array_impl_present": false,
"source_zeroize_vec_impl_present": false,
"ops_lean_replay_json_path": "",
"ops_lean_replay_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": "",
"bounded_zeroization_dse_proof_ready": false,
"whole_program_zeroization_proof": false,
"counts_as_p6_closure": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false
},
"gl181_key_exchange_tamarin_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_id": "",
"acceptance_template": "",
"required_tool_family": "",
"obligation_path": "",
"obligation_sha256": "",
"obligation_matches": false,
"model_path": "",
"model_sha256": "",
"model_static_ready": false,
"required_rule_count": 0,
"required_rule_present_count": 0,
"required_event_count": 0,
"required_event_present_count": 0,
"required_lemma_count": 0,
"required_lemma_present_count": 0,
"placeholder_absent": false,
"boundary_comment_present": false,
"tamarin_available": false,
"tamarin_replay_attempted": false,
"tamarin_replay_ok": false,
"verified_by_required_toolchain": false,
"formal_model_requirement_admitted": false,
"effective_audit_status": "missing_evidence",
"counts_as_narrow_requirement_closure": false,
"counts_as_global_p6_closure": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"evidence_json_path": "",
"evidence_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"gl182_key_exchange_proverif_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_id": "",
"acceptance_template": "",
"required_tool_family": "",
"obligation_path": "",
"obligation_sha256": "",
"obligation_matches": false,
"model_path": "",
"model_sha256": "",
"model_static_ready": false,
"required_term_count": 0,
"required_term_present_count": 0,
"required_event_count": 0,
"required_event_present_count": 0,
"required_query_count": 0,
"required_query_present_count": 0,
"declared_query_count": 0,
"verified_query_count": 0,
"placeholder_absent": false,
"boundary_comment_present": false,
"proverif_available": false,
"proverif_path": "",
"proverif_sha256": "",
"proverif_version": "",
"proverif_replay_attempted": false,
"proverif_replay_ok": false,
"proverif_returncode": -1,
"proverif_timeout": false,
"proverif_result_count": 0,
"proverif_true_result_count": 0,
"proverif_failure_markers_absent": false,
"application_secret_secrecy_verified": false,
"initiator_accept_implies_responder_accept_verified": false,
"responder_accept_implies_initiator_started_pair_verified": false,
"verified_by_required_toolchain": false,
"formal_model_requirement_admitted": false,
"effective_audit_status": "missing_evidence",
"counts_as_narrow_requirement_closure": false,
"counts_as_global_p6_closure": false,
"computational_security_proof": false,
"production_pfs_proof": false,
"production_mutual_auth_proof": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"external_operator_evidence_count": 0,
"true_decentralization_proven": false,
"public_endpoint_admits_sovereign_claims": false,
"counts_as_sovereign_closure_count": 0,
"evidence_json_path": "",
"evidence_json_sha256": "",
"proverif_log_path": "",
"proverif_log_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"gl183_pfs_tamarin_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_id": "",
"acceptance_template": "",
"required_tool_family": "",
"obligation_path": "",
"obligation_sha256": "",
"obligation_matches": false,
"model_path": "",
"model_sha256": "",
"model_static_ready": false,
"required_rule_count": 0,
"required_rule_present_count": 0,
"required_event_count": 0,
"required_event_present_count": 0,
"required_lemma_count": 0,
"required_lemma_present_count": 0,
"placeholder_absent": false,
"boundary_comment_present": false,
"tamarin_available": false,
"tamarin_replay_attempted": false,
"tamarin_replay_ok": false,
"tamarin_failure_markers_absent": false,
"verified_by_required_toolchain": false,
"theorem_proof_requirement_admitted": false,
"effective_audit_status": "missing_evidence",
"counts_as_narrow_requirement_closure": false,
"counts_as_global_p6_closure": false,
"production_pfs_proof": false,
"production_implementation_equivalent": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"external_operator_evidence_count": 0,
"true_decentralization_proven": false,
"public_endpoint_admits_sovereign_claims": false,
"counts_as_sovereign_closure_count": 0,
"evidence_json_path": "",
"evidence_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"gl184_mutual_auth_tamarin_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_id": "",
"acceptance_template": "",
"required_tool_family": "",
"obligation_path": "",
"obligation_sha256": "",
"obligation_matches": false,
"model_path": "",
"model_sha256": "",
"model_static_ready": false,
"required_rule_count": 0,
"required_rule_present_count": 0,
"required_event_count": 0,
"required_event_present_count": 0,
"required_lemma_count": 0,
"required_lemma_present_count": 0,
"placeholder_absent": false,
"boundary_comment_present": false,
"tamarin_available": false,
"tamarin_replay_attempted": false,
"tamarin_replay_ok": false,
"tamarin_failure_markers_absent": false,
"verified_by_required_toolchain": false,
"theorem_proof_requirement_admitted": false,
"effective_audit_status": "missing_evidence",
"counts_as_narrow_requirement_closure": false,
"counts_as_global_p6_closure": false,
"production_mutual_auth_proof": false,
"production_mtls_mak_proof": false,
"production_implementation_equivalent": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"external_operator_evidence_count": 0,
"true_decentralization_proven": false,
"public_endpoint_admits_sovereign_claims": false,
"counts_as_sovereign_closure_count": 0,
"evidence_json_path": "",
"evidence_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"gl185_189_protocol_attack_resistance_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_ids": "",
"acceptance_template": "",
"required_tool_family_symbolic": "",
"required_tool_family_proof_assistant": "",
"obligation_count": 0,
"obligation_match_count": 0,
"model_path": "",
"model_sha256": "",
"lean_path": "",
"lean_sha256": "",
"model_static_ready": false,
"lean_static_ready": false,
"required_rule_count": 0,
"required_rule_present_count": 0,
"required_event_count": 0,
"required_event_present_count": 0,
"required_lemma_count": 0,
"required_lemma_present_count": 0,
"lean_theorem_count": 0,
"lean_theorem_present_count": 0,
"placeholder_absent": false,
"boundary_comment_present": false,
"tamarin_available": false,
"tamarin_replay_attempted": false,
"tamarin_replay_ok": false,
"tamarin_failure_markers_absent": false,
"proverif_available": false,
"proverif_model_present": false,
"proverif_replay_attempted": false,
"proverif_replay_ok": false,
"symbolic_protocol_replay_ok": false,
"lean_available": false,
"lean_replay_attempted": false,
"lean_replay_ok": false,
"verified_by_required_toolchain": false,
"theorem_proof_requirements_admitted": false,
"theorem_proof_admitted_requirement_ids": [],
"theorem_proof_admitted_requirement_count": 0,
"effective_audit_status": "missing_evidence",
"counts_as_narrow_requirement_closure": false,
"counts_as_narrow_requirement_closure_count": 0,
"counts_as_global_p6_closure": false,
"production_mitm_resistance_proof": false,
"production_replay_resistance_proof": false,
"production_desync_resistance_proof": false,
"production_downgrade_resistance_proof": false,
"production_session_independence_proof": false,
"production_protocol_attack_resistance_proof": false,
"production_implementation_equivalent": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"external_audit_evidence": false,
"external_operator_evidence_count": 0,
"true_decentralization_proven": false,
"public_endpoint_admits_sovereign_claims": false,
"counts_as_sovereign_closure_count": 0,
"evidence_json_path": "",
"evidence_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"gl190_hkdf_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_id": "",
"acceptance_template": "",
"required_tool_family_symbolic": "",
"required_tool_family_proof_assistant": "",
"obligation_path": "",
"obligation_sha256": "",
"obligation_matches": false,
"model_path": "",
"model_sha256": "",
"lean_path": "",
"lean_sha256": "",
"model_static_ready": false,
"lean_static_ready": false,
"required_rule_count": 0,
"required_rule_present_count": 0,
"required_event_count": 0,
"required_event_present_count": 0,
"required_lemma_count": 0,
"required_lemma_present_count": 0,
"lean_theorem_count": 0,
"lean_theorem_present_count": 0,
"placeholder_absent": false,
"boundary_comment_present": false,
"tamarin_available": false,
"tamarin_replay_attempted": false,
"tamarin_replay_ok": false,
"tamarin_failure_markers_absent": false,
"proverif_available": false,
"proverif_model_present": false,
"proverif_replay_attempted": false,
"proverif_replay_ok": false,
"symbolic_protocol_replay_ok": false,
"lean_available": false,
"lean_replay_attempted": false,
"lean_replay_ok": false,
"verified_by_required_toolchain": false,
"theorem_proof_requirement_admitted": false,
"effective_audit_status": "missing_evidence",
"counts_as_narrow_requirement_closure": false,
"counts_as_global_p6_closure": false,
"production_hkdf_security_proof": false,
"computational_hmac_prf_proof": false,
"production_implementation_equivalent": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"external_operator_evidence_count": 0,
"true_decentralization_proven": false,
"public_endpoint_admits_sovereign_claims": false,
"counts_as_sovereign_closure_count": 0,
"evidence_json_path": "",
"evidence_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"gl191_csprng_formal_model_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_id": "",
"acceptance_template": "",
"required_tool_family_symbolic": "",
"obligation_path": "",
"obligation_sha256": "",
"obligation_matches": false,
"model_path": "",
"model_sha256": "",
"model_static_ready": false,
"required_rule_count": 0,
"required_rule_present_count": 0,
"required_event_count": 0,
"required_event_present_count": 0,
"required_lemma_count": 0,
"required_lemma_present_count": 0,
"placeholder_absent": false,
"boundary_comment_present": false,
"tamarin_available": false,
"tamarin_replay_attempted": false,
"tamarin_replay_ok": false,
"proverif_available": false,
"proverif_model_present": false,
"proverif_replay_attempted": false,
"proverif_replay_ok": false,
"symbolic_protocol_replay_ok": false,
"verified_by_required_toolchain": false,
"formal_model_requirement_admitted": false,
"effective_audit_status": "missing_evidence",
"counts_as_narrow_requirement_closure": false,
"counts_as_global_p6_closure": false,
"production_csprng_model_proof": false,
"forward_resistance_proof": false,
"backward_resistance_proof": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"evidence_json_path": "",
"evidence_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"gl192_csprng_forward_resistance_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_id": "",
"acceptance_template": "",
"required_tool_family_symbolic": "",
"required_tool_family_proof_assistant": "",
"obligation_path": "",
"obligation_sha256": "",
"obligation_matches": false,
"model_path": "",
"model_sha256": "",
"lean_path": "",
"lean_sha256": "",
"model_static_ready": false,
"lean_static_ready": false,
"required_rule_count": 0,
"required_rule_present_count": 0,
"required_event_count": 0,
"required_event_present_count": 0,
"required_lemma_count": 0,
"required_lemma_present_count": 0,
"lean_theorem_count": 0,
"lean_theorem_present_count": 0,
"placeholder_absent": false,
"boundary_comment_present": false,
"tamarin_available": false,
"tamarin_replay_attempted": false,
"tamarin_replay_ok": false,
"proverif_available": false,
"proverif_model_present": false,
"proverif_replay_attempted": false,
"proverif_replay_ok": false,
"symbolic_protocol_replay_ok": false,
"lean_available": false,
"lean_replay_attempted": false,
"lean_replay_ok": false,
"verified_by_required_toolchain": false,
"runtime_summary_path": "",
"runtime_summary_sha256": "",
"runtime_evidence_json_path": "",
"runtime_evidence_json_sha256": "",
"runtime_source_hashes_match": false,
"runtime_boundary_valid": false,
"source_level_runtime_binding": false,
"theorem_proof_requirement_admitted": false,
"effective_audit_status": "missing_evidence",
"counts_as_narrow_requirement_closure": false,
"counts_as_global_p6_closure": false,
"production_csprng_forward_resistance_proof": false,
"computational_hmac_prf_proof": false,
"forward_resistance_proof": false,
"production_implementation_equivalent": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"evidence_json_path": "",
"evidence_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"gl193_csprng_backward_resistance_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_id": "",
"acceptance_template": "",
"required_tool_family_symbolic": "",
"required_tool_family_proof_assistant": "",
"obligation_path": "",
"obligation_sha256": "",
"obligation_matches": false,
"model_path": "",
"model_sha256": "",
"lean_path": "",
"lean_sha256": "",
"model_static_ready": false,
"lean_static_ready": false,
"required_rule_count": 0,
"required_rule_present_count": 0,
"required_event_count": 0,
"required_event_present_count": 0,
"required_lemma_count": 0,
"required_lemma_present_count": 0,
"lean_theorem_count": 0,
"lean_theorem_present_count": 0,
"placeholder_absent": false,
"boundary_comment_present": false,
"tamarin_available": false,
"tamarin_replay_attempted": false,
"tamarin_replay_ok": false,
"proverif_available": false,
"proverif_model_present": false,
"proverif_replay_attempted": false,
"proverif_replay_ok": false,
"symbolic_protocol_replay_ok": false,
"lean_available": false,
"lean_replay_attempted": false,
"lean_replay_ok": false,
"verified_by_required_toolchain": false,
"runtime_summary_path": "",
"runtime_summary_sha256": "",
"runtime_evidence_json_path": "",
"runtime_evidence_json_sha256": "",
"runtime_source_hashes_match": false,
"runtime_boundary_valid": false,
"source_level_runtime_binding": false,
"theorem_proof_requirement_admitted": false,
"effective_audit_status": "missing_evidence",
"counts_as_narrow_requirement_closure": false,
"counts_as_global_p6_closure": false,
"production_csprng_backward_resistance_proof": false,
"computational_hmac_prf_proof": false,
"break_in_recovery_proof": false,
"production_implementation_equivalent": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"evidence_json_path": "",
"evidence_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"gl194_prg_drbg_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_id": "",
"acceptance_template": "",
"required_tool_family_symbolic": "",
"required_tool_family_proof_assistant": "",
"source_rewrite_evidence_path": "",
"source_rewrite_evidence_sha256": "",
"source_rewrite_evidence_matches": false,
"source_overlay_path": "",
"source_overlay_sha256": "",
"source_overlay_matches": false,
"model_path": "",
"model_sha256": "",
"lean_path": "",
"lean_sha256": "",
"model_static_ready": false,
"lean_static_ready": false,
"required_rule_count": 0,
"required_rule_present_count": 0,
"required_event_count": 0,
"required_event_present_count": 0,
"required_lemma_count": 0,
"required_lemma_present_count": 0,
"lean_theorem_count": 0,
"lean_theorem_present_count": 0,
"placeholder_absent": false,
"boundary_comment_present": false,
"tamarin_available": false,
"tamarin_replay_attempted": false,
"tamarin_replay_ok": false,
"proverif_available": false,
"proverif_model_present": false,
"proverif_replay_attempted": false,
"proverif_replay_ok": false,
"symbolic_protocol_replay_ok": false,
"lean_available": false,
"lean_replay_attempted": false,
"lean_replay_ok": false,
"verified_by_required_toolchain": false,
"accepted_theorem_evidence_present": false,
"production_prg_drbg_security_proof": false,
"quantitative_min_entropy_proof": false,
"reseed_policy_acceptance_proof": false,
"fleet_entropy_measurements_or_external_audit": false,
"true_random_indistinguishability_claim_allowed": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"evidence_json_path": "",
"evidence_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"gl195_196_198_199_entropy_state_atomicity_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_ids": "",
"acceptance_template": "",
"required_tool_family_symbolic": "",
"required_tool_family_proof_assistant": "",
"obligation_count": 0,
"obligation_match_count": 0,
"model_path": "",
"model_sha256": "",
"lean_path": "",
"lean_sha256": "",
"model_static_ready": false,
"lean_static_ready": false,
"required_rule_count": 0,
"required_rule_present_count": 0,
"required_event_count": 0,
"required_event_present_count": 0,
"required_lemma_count": 0,
"required_lemma_present_count": 0,
"lean_theorem_count": 0,
"lean_theorem_present_count": 0,
"placeholder_absent": false,
"boundary_comment_present": false,
"tamarin_available": false,
"tamarin_replay_attempted": false,
"tamarin_replay_ok": false,
"proverif_available": false,
"proverif_model_present": false,
"proverif_replay_attempted": false,
"proverif_replay_ok": false,
"symbolic_protocol_replay_ok": false,
"lean_available": false,
"lean_replay_attempted": false,
"lean_replay_ok": false,
"verified_by_required_toolchain": false,
"production_min_entropy_proof": false,
"production_unbiased_conditioning_proof": false,
"production_unreachable_state_proof": false,
"production_key_update_atomicity_proof": false,
"production_entropy_state_atomicity_proof": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"evidence_json_path": "",
"evidence_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"gl197_key_lifecycle_state_machine_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_id": "",
"acceptance_template": "",
"required_tool_family_symbolic": "",
"required_tool_family_proof_assistant": "",
"obligation_path": "",
"obligation_sha256": "",
"obligation_matches": false,
"model_path": "",
"model_sha256": "",
"lean_path": "",
"lean_sha256": "",
"model_static_ready": false,
"lean_static_ready": false,
"required_rule_count": 0,
"required_rule_present_count": 0,
"required_event_count": 0,
"required_event_present_count": 0,
"required_lemma_count": 0,
"required_lemma_present_count": 0,
"lean_theorem_count": 0,
"lean_theorem_present_count": 0,
"placeholder_absent": false,
"boundary_comment_present": false,
"tamarin_available": false,
"tamarin_replay_attempted": false,
"tamarin_replay_ok": false,
"proverif_available": false,
"proverif_model_present": false,
"proverif_replay_attempted": false,
"proverif_replay_ok": false,
"symbolic_protocol_replay_ok": false,
"lean_available": false,
"lean_replay_attempted": false,
"lean_replay_ok": false,
"verified_by_required_toolchain": false,
"production_key_lifecycle_state_machine_proof": false,
"key_lifecycle_state_machine_proof": false,
"revoked_key_reuse_proof": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"evidence_json_path": "",
"evidence_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"gl200_composition_theorem_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_id": "",
"acceptance_template": "",
"required_tool_family_symbolic": "",
"required_tool_family_proof_assistant": "",
"obligation_path": "",
"obligation_sha256": "",
"obligation_matches": false,
"model_path": "",
"model_sha256": "",
"lean_path": "",
"lean_sha256": "",
"model_static_ready": false,
"lean_static_ready": false,
"required_rule_count": 0,
"required_rule_present_count": 0,
"required_event_count": 0,
"required_event_present_count": 0,
"required_lemma_count": 0,
"required_lemma_present_count": 0,
"lean_theorem_count": 0,
"lean_theorem_present_count": 0,
"placeholder_absent": false,
"boundary_comment_present": false,
"tamarin_available": false,
"tamarin_replay_attempted": false,
"tamarin_replay_ok": false,
"proverif_available": false,
"proverif_model_present": false,
"proverif_replay_attempted": false,
"proverif_replay_ok": false,
"symbolic_protocol_replay_ok": false,
"lean_available": false,
"lean_replay_attempted": false,
"lean_replay_ok": false,
"verified_by_required_toolchain": false,
"production_composition_theorem_proof": false,
"component_proof_closure_ready": false,
"global_security_composition_proof": false,
"e2e_security_property_proof": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"evidence_json_path": "",
"evidence_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"gl205_system_theorem_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_id": "",
"acceptance_template": "",
"source_queue_item_matches": false,
"system_theorem_path": "",
"system_theorem_sha256": "",
"assumption_register_path": "",
"assumption_register_sha256": "",
"architecture_tcb_path": "",
"architecture_tcb_sha256": "",
"dependency_graph_path": "",
"dependency_graph_sha256": "",
"assurance_contract_path": "",
"assurance_contract_sha256": "",
"model_path": "",
"model_sha256": "",
"lean_path": "",
"lean_sha256": "",
"artifact_present_count": 0,
"artifact_required_count": 0,
"assumption_code_present_count": 0,
"assumption_code_required_count": 0,
"epsilon_structure_present": false,
"system_theorem_statement_present": false,
"graph_gl205_ready": false,
"meta_replay_ok": false,
"dependency_graph_prior_replay_path": "",
"dependency_graph_prior_replay_sha256": "",
"dependency_graph_prior_replay_ok": false,
"model_static_ready": false,
"lean_static_ready": false,
"required_rule_count": 0,
"required_rule_present_count": 0,
"required_event_count": 0,
"required_event_present_count": 0,
"required_lemma_count": 0,
"required_lemma_present_count": 0,
"lean_theorem_count": 0,
"lean_theorem_present_count": 0,
"placeholder_absent": false,
"boundary_comment_present": false,
"tamarin_available": false,
"tamarin_replay_attempted": false,
"tamarin_replay_ok": false,
"proverif_available": false,
"proverif_model_present": false,
"proverif_replay_ok": false,
"symbolic_protocol_replay_ok": false,
"lean_available": false,
"lean_replay_attempted": false,
"lean_replay_ok": false,
"verified_by_required_toolchain": false,
"accepted_theorem_evidence_present": false,
"theorem_grade_s0_proof": false,
"numeric_epsilon_total_proof": false,
"production_component_closure_proof": false,
"mechanized_refinement_proof": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"evidence_json_path": "",
"evidence_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"gl206_epsilon_total_bound_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_id": "",
"acceptance_template": "",
"source_queue_item_matches": false,
"source_artifacts_present": false,
"system_theorem_path": "",
"system_theorem_sha256": "",
"dependency_graph_path": "",
"dependency_graph_sha256": "",
"assurance_contract_path": "",
"assurance_contract_sha256": "",
"bound_note_path": "",
"bound_note_sha256": "",
"lean_path": "",
"lean_sha256": "",
"epsilon_term_present_count": 0,
"epsilon_term_required_count": 0,
"ledger_source_mapped_count": 0,
"aggregation_formula_present": false,
"hidden_residual_term_absent": false,
"theorem_epsilon_structure_present": false,
"graph_node_gl206_ready": false,
"graph_edges_gl206_ready": false,
"contract_boundary_present": false,
"lean_static_ready": false,
"lean_theorem_count": 0,
"lean_theorem_present_count": 0,
"placeholder_absent": false,
"boundary_comment_present": false,
"lean_available": false,
"lean_replay_attempted": false,
"lean_replay_ok": false,
"numeric_local_bound_present_count": 0,
"numeric_total_available": false,
"concrete_epsilon_total_proof": false,
"production_component_numeric_bounds": false,
"machine_checked_numeric_bound": false,
"verified_by_required_toolchain": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"evidence_json_path": "",
"evidence_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"gl207_multi_session_theorem_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_id": "",
"acceptance_template": "",
"required_tool_family": "",
"source_queue_item_matches": false,
"source_artifacts_present": false,
"source_artifact_present_count": 0,
"source_artifact_required_count": 0,
"system_theorem_path": "",
"system_theorem_sha256": "",
"s0_statement_present": false,
"s1_statement_present": false,
"s1_conditioned_on_s0": false,
"system_theorem_s1_static_ready": false,
"multi_session_dimension_present_count": 0,
"multi_session_dimension_required_count": 0,
"dependency_model_path": "",
"dependency_model_sha256": "",
"dependency_model_gl207_ready": false,
"dependency_prerequisite_count": 0,
"dependency_consequence_count": 0,
"dependency_graph_path": "",
"dependency_graph_sha256": "",
"graph_node_gl207_ready": false,
"graph_edges_gl207_ready": false,
"coverage_matrix_path": "",
"coverage_matrix_sha256": "",
"coverage_matrix_gl207_ready": false,
"coverage_matrix_module_present_count": 0,
"coverage_matrix_proof_artifact_count": 0,
"first_audit_path": "",
"first_audit_sha256": "",
"first_audit_gl207_ready": false,
"closure_queue_path": "",
"closure_queue_sha256": "",
"closure_queue_gl207_ready": false,
"workbench_note_path": "",
"workbench_note_sha256": "",
"workbench_note_static_ready": false,
"lean_path": "",
"lean_sha256": "",
"lean_static_ready": false,
"lean_theorem_count": 0,
"lean_theorem_present_count": 0,
"placeholder_absent": false,
"boundary_comment_present": false,
"lean_available": false,
"lean_replay_attempted": false,
"lean_replay_ok": false,
"theorem_grade_s1_proof": false,
"probabilistic_multi_user_bound": false,
"production_fleet_concurrency_evidence": false,
"verified_by_required_toolchain": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"evidence_json_path": "",
"evidence_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"gl208_refinement_theorem_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_id": "",
"acceptance_template": "",
"required_tool_family": "",
"source_queue_item_matches": false,
"source_artifacts_present": false,
"source_artifact_present_count": 0,
"source_artifact_required_count": 0,
"trace_claim_present_count": 0,
"trace_claim_required_count": 0,
"refinement_source_path": "",
"refinement_source_sha256": "",
"refinement_source_static_ready": false,
"attestation_doc_path": "",
"attestation_doc_sha256": "",
"refinement_attestation_doc_static_ready": false,
"audit_path": "",
"audit_sha256": "",
"refinement_audit_static_ready": false,
"local_trace_audit_accepted": false,
"coverage_matrix_path": "",
"coverage_matrix_sha256": "",
"coverage_matrix_gl208_ready": false,
"coverage_matrix_function_present_count": 0,
"coverage_matrix_function_required_count": 0,
"dependency_model_path": "",
"dependency_model_sha256": "",
"dependency_model_gl208_ready": false,
"dependency_prerequisite_count": 0,
"dependency_consequence_count": 0,
"dependency_graph_path": "",
"dependency_graph_sha256": "",
"graph_node_gl208_ready": false,
"graph_edges_gl208_ready": false,
"assumption_h8_boundary_present": false,
"workbench_note_path": "",
"workbench_note_sha256": "",
"lean_path": "",
"lean_sha256": "",
"lean_static_ready": false,
"lean_theorem_count": 0,
"lean_theorem_present_count": 0,
"placeholder_absent": false,
"boundary_comment_present": false,
"lean_available": false,
"lean_replay_attempted": false,
"lean_replay_ok": false,
"mechanized_e2e_refinement_proof": false,
"production_binary_refinement_proof": false,
"binary_hash_equivalence_proof": false,
"verified_by_required_toolchain": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"evidence_json_path": "",
"evidence_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"gl214_api_invariants_typestate_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_id": "",
"acceptance_template": "",
"required_tool_family": "",
"source_queue_item_matches": false,
"source_artifacts_restored": false,
"artifact_present_count": 0,
"artifact_required_count": 0,
"tests_integration_artifact_present": false,
"contract_doc_path": "",
"contract_doc_sha256": "",
"contract_doc_static_ready": false,
"contract_refusal_clause_present_count": 0,
"contract_refusal_clause_required_count": 0,
"contract_scope_limit_present": false,
"smoke_report_path": "",
"smoke_report_sha256": "",
"api_refusal_smoke_ok": false,
"api_refusal_smoke_case_present_count": 0,
"api_refusal_smoke_pass_count": 0,
"api_refusal_smoke_required_count": 0,
"header_budget_path": "",
"header_budget_sha256": "",
"header_budget_static_ready": false,
"gpqve_exact_path": "",
"gpqve_exact_sha256": "",
"gpqve_exact_static_ready": false,
"integration_tests_path": "",
"integration_tests_sha256": "",
"integration_tests_static_ready": false,
"integration_replay_ok": false,
"integration_replay_test_count": 0,
"workbench_note_path": "",
"workbench_note_sha256": "",
"workbench_note_static_ready": false,
"lean_path": "",
"lean_sha256": "",
"lean_static_ready": false,
"lean_theorem_count": 0,
"lean_theorem_present_count": 0,
"placeholder_absent": false,
"boundary_comment_present": false,
"lean_available": false,
"lean_replay_attempted": false,
"lean_replay_ok": false,
"typestate_theorem_proof": false,
"whole_api_static_impossibility_proof": false,
"full_public_api_invariant_closure": false,
"verified_by_required_toolchain": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"evidence_json_path": "",
"evidence_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"gl215_state_closure_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_id": "",
"acceptance_template": "",
"required_tool_family": "",
"source_queue_item_matches": false,
"source_artifacts_present": false,
"artifact_present_count": 0,
"artifact_required_count": 0,
"state_model_path": "",
"state_model_sha256": "",
"state_model_static_ready": false,
"state_machine_inventory_count": 0,
"state_machine_inventory_required_count": 0,
"native_cpabe_path": "",
"native_cpabe_sha256": "",
"gpqve_exact_path": "",
"gpqve_exact_sha256": "",
"source_transition_markers_ready": false,
"source_transition_marker_present_count": 0,
"source_transition_marker_required_count": 0,
"dependency_model_gl215_ready": false,
"dependency_prerequisite_count": 0,
"dependency_consequence_count": 0,
"graph_node_gl215_ready": false,
"graph_edges_gl215_ready": false,
"coverage_matrix_gl215_ready": false,
"coverage_matrix_function_present_count": 0,
"coverage_matrix_module_present_count": 0,
"coverage_matrix_proof_artifact_count": 0,
"first_audit_gl215_ready": false,
"closure_queue_gl215_ready": false,
"gl197_key_lifecycle_ready": false,
"gl198_invalid_state_rejection_ready": false,
"gl199_atomic_update_ready": false,
"prerequisite_workbenches_ready": false,
"prerequisite_workbench_ready_count": 0,
"prerequisite_workbench_required_count": 0,
"targeted_rust_replay_ok": false,
"targeted_rust_replay_test_count": 0,
"workbench_note_path": "",
"workbench_note_sha256": "",
"workbench_note_static_ready": false,
"lean_path": "",
"lean_sha256": "",
"lean_static_ready": false,
"lean_theorem_count": 0,
"lean_theorem_present_count": 0,
"placeholder_absent": false,
"boundary_comment_present": false,
"lean_available": false,
"lean_replay_attempted": false,
"lean_replay_ok": false,
"state_closure_theorem_proof": false,
"whole_system_state_totality_proof": false,
"production_state_machine_safety_proof": false,
"verified_by_required_toolchain": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"evidence_json_path": "",
"evidence_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"gl218_software_hardware_compatibility_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_id": "",
"acceptance_template": "",
"required_tool_family": "",
"source_queue_item_matches": false,
"source_artifacts_present": false,
"artifact_present_count": 0,
"artifact_required_count": 0,
"system_theorem_path": "",
"system_theorem_sha256": "",
"bridge_statements_ready": false,
"bridge_statement_present_count": 0,
"bridge_statement_required_count": 0,
"assumption_register_path": "",
"assumption_register_sha256": "",
"hardware_assumptions_ready": false,
"hardware_class_ready": false,
"hardware_assumption_present_count": 0,
"hardware_assumption_required_count": 0,
"assumption_h9_ready": false,
"assumption_h11_ready": false,
"assumption_h12_ready": false,
"meta_contract_path": "",
"meta_contract_sha256": "",
"meta_contract_scope_ready": false,
"dependency_model_path": "",
"dependency_model_sha256": "",
"dependency_model_gl218_ready": false,
"prerequisite_count": 0,
"prerequisite_required_count": 0,
"prerequisite_partial_count": 0,
"prerequisite_missing_evidence_count": 0,
"unclosed_prerequisite_count": 0,
"prerequisite_gaps_exposed": false,
"gl163_partial": false,
"gl164_partial": false,
"gl165_missing_evidence": false,
"gl166_partial": false,
"coverage_matrix_path": "",
"coverage_matrix_sha256": "",
"coverage_matrix_gl218_ready": false,
"coverage_matrix_module_present_count": 0,
"coverage_matrix_module_required_count": 0,
"coverage_matrix_proof_artifact_count": 0,
"coverage_matrix_platform_scope": "",
"graph_path": "",
"graph_sha256": "",
"graph_node_gl218_ready": false,
"graph_edge_gl218_h9_ready": false,
"first_audit_gl218_ready": false,
"closure_queue_gl218_ready": false,
"fault_model_path": "",
"fault_model_sha256": "",
"meta_fault_model_ready": false,
"fault_class_count": 0,
"modeled_fault_class_count": 0,
"partially_modeled_fault_class_count": 0,
"excluded_fault_class_count": 0,
"universal_microarchitecture_exclusion_ready": false,
"platform_coverage_path": "",
"platform_coverage_sha256": "",
"platform_coverage_ready": false,
"declared_platform_count": 0,
"local_host_scope_only": false,
"side_channel_campaign_count": 0,
"side_channel_platform_coverage_replay_path": "",
"side_channel_platform_coverage_replay_sha256": "",
"side_channel_platform_coverage_replay_ok": false,
"meta_fault_model_replay_path": "",
"meta_fault_model_replay_sha256": "",
"meta_fault_model_replay_ok": false,
"workbench_note_path": "",
"workbench_note_sha256": "",
"workbench_note_static_ready": false,
"lean_path": "",
"lean_sha256": "",
"lean_static_ready": false,
"lean_theorem_count": 0,
"lean_theorem_present_count": 0,
"placeholder_absent": false,
"boundary_comment_present": false,
"lean_available": false,
"lean_replay_attempted": false,
"lean_replay_ok": false,
"software_hardware_compatibility_proof": false,
"formal_hardware_model_proof": false,
"universal_microarchitecture_claim_allowed": false,
"production_compatibility_theorem_proof": false,
"verified_by_required_toolchain": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"evidence_json_path": "",
"evidence_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"gl224_fail_safe_policy_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_id": "",
"acceptance_template": "",
"required_tool_family": "",
"source_queue_item_matches": false,
"source_artifacts_present": false,
"artifact_present_count": 0,
"artifact_required_count": 0,
"meta_contract_path": "",
"meta_contract_sha256": "",
"contract_fail_closed_clauses_ready": false,
"contract_fail_closed_clause_present_count": 0,
"contract_fail_closed_clause_required_count": 0,
"source_fail_closed_markers_ready": false,
"source_fail_closed_marker_present_count": 0,
"source_fail_closed_marker_required_count": 0,
"dependency_model_path": "",
"dependency_model_sha256": "",
"dependency_model_gl224_ready": false,
"dependency_edges_gl224_ready": false,
"prerequisite_count": 0,
"prerequisite_required_count": 0,
"unclosed_prerequisite_count": 0,
"prerequisite_gaps_exposed": false,
"gl128_formal_theorem_present": false,
"gl128_status": "",
"gl181_status": "",
"gl191_status": "",
"gl197_status": "",
"graph_path": "",
"graph_sha256": "",
"graph_node_gl224_ready": false,
"graph_edge_gl215_gl224_ready": false,
"graph_edge_gl224_gl215_ready": false,
"coverage_matrix_path": "",
"coverage_matrix_sha256": "",
"coverage_matrix_gl224_ready": false,
"coverage_matrix_function_present_count": 0,
"coverage_matrix_module_present_count": 0,
"coverage_matrix_proof_artifact_count": 0,
"coverage_matrix_platform_scope": "",
"first_audit_gl224_ready": false,
"closure_queue_gl224_ready": false,
"gl181_protocol_model_ready": false,
"gl191_csprng_ready": false,
"gl197_key_lifecycle_ready": false,
"prerequisite_workbenches_ready": false,
"prerequisite_workbench_ready_count": 0,
"prerequisite_workbench_required_count": 0,
"targeted_rust_replay_ok": false,
"targeted_rust_replay_test_count": 0,
"workbench_note_path": "",
"workbench_note_sha256": "",
"workbench_note_static_ready": false,
"lean_path": "",
"lean_sha256": "",
"lean_static_ready": false,
"lean_theorem_count": 0,
"lean_theorem_present_count": 0,
"placeholder_absent": false,
"boundary_comment_present": false,
"lean_available": false,
"lean_replay_attempted": false,
"lean_replay_ok": false,
"fail_safe_policy_theorem_proof": false,
"non_exploitability_proof": false,
"whole_system_failure_noninterference_proof": false,
"verified_by_required_toolchain": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"evidence_json_path": "",
"evidence_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"gl225_assurance_contract_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_id": "",
"acceptance_template": "",
"first_audit_path": "",
"first_audit_sha256": "",
"first_audit_gl225_ready": false,
"source_artifacts_present": false,
"artifact_present_count": 0,
"artifact_required_count": 0,
"meta_contract_path": "",
"meta_contract_sha256": "",
"contract_inventory_ready": false,
"required_section_present_count": 0,
"required_section_required_count": 0,
"verification_link_present_count": 0,
"verification_link_required_count": 0,
"operator_command_present_count": 0,
"operator_command_required_count": 0,
"assumption_register_path": "",
"assumption_register_sha256": "",
"assumption_code_present_count": 0,
"assumption_code_required_count": 0,
"system_theorem_path": "",
"system_theorem_sha256": "",
"system_theorem_boundary_ready": false,
"approval_checklist_path": "",
"approval_checklist_sha256": "",
"approval_checklist_ready": false,
"replay_script_path": "",
"replay_script_sha256": "",
"meta_replay_json_path": "",
"meta_replay_json_sha256": "",
"meta_replay_md_path": "",
"meta_replay_md_sha256": "",
"meta_replay_ok": false,
"meta_replay_requirement_count": 0,
"meta_replay_gl225_ok": false,
"meta_replay_gl225_check_present_count": 0,
"meta_replay_gl225_check_required_count": 0,
"dependency_model_path": "",
"dependency_model_sha256": "",
"dependency_model_gl225_ready": false,
"dependency_edges_ready": false,
"dependency_prerequisite_count": 0,
"gl205_status": "",
"gl206_status": "",
"gl210_status": "",
"prerequisite_verified_count": 0,
"unclosed_prerequisite_count": 0,
"graph_path": "",
"graph_sha256": "",
"graph_node_gl225_ready": false,
"graph_edge_gl225_s0_ready": false,
"coverage_matrix_path": "",
"coverage_matrix_sha256": "",
"coverage_matrix_gl225_ready": false,
"coverage_matrix_function_present_count": 0,
"coverage_matrix_module_present_count": 0,
"coverage_matrix_proof_artifact_count": 0,
"coverage_matrix_platform_scope": "",
"workbench_note_path": "",
"workbench_note_sha256": "",
"workbench_note_static_ready": false,
"lean_path": "",
"lean_sha256": "",
"lean_static_ready": false,
"lean_theorem_count": 0,
"lean_theorem_present_count": 0,
"placeholder_absent": false,
"boundary_comment_present": false,
"lean_available": false,
"lean_replay_attempted": false,
"lean_replay_ok": false,
"process_control_verified": false,
"theorem_grade_s0_proof": false,
"numeric_epsilon_total_proof": false,
"production_component_closure_proof": false,
"all_p6_requirements_closed": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"evidence_json_path": "",
"evidence_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"gl161_secret_branch_binsec_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_id": "",
"acceptance_template": "",
"required_tool_family": "",
"obligation_path": "",
"obligation_sha256": "",
"obligation_matches": false,
"binsec_contract_path": "",
"binsec_contract_sha256": "",
"lean_path": "",
"lean_sha256": "",
"binsec_contract_static_ready": false,
"lean_static_ready": false,
"required_clause_count": 0,
"required_clause_present_count": 0,
"lean_theorem_count": 0,
"lean_theorem_present_count": 0,
"placeholder_absent": false,
"boundary_comment_present": false,
"binsec_available": false,
"binsec_replay_attempted": false,
"binsec_replay_ok": false,
"lean_available": false,
"lean_replay_attempted": false,
"lean_replay_ok": false,
"verified_by_required_toolchain": false,
"production_secret_branch_proof": false,
"secret_dependent_branch_absence_proof": false,
"side_channel_closure_ready": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"evidence_json_path": "",
"evidence_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"gl162_secret_memory_access_binsec_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_id": "",
"acceptance_template": "",
"required_tool_family": "",
"obligation_path": "",
"obligation_sha256": "",
"obligation_matches": false,
"binsec_contract_path": "",
"binsec_contract_sha256": "",
"lean_path": "",
"lean_sha256": "",
"binsec_contract_static_ready": false,
"lean_static_ready": false,
"required_clause_count": 0,
"required_clause_present_count": 0,
"lean_theorem_count": 0,
"lean_theorem_present_count": 0,
"placeholder_absent": false,
"boundary_comment_present": false,
"binsec_available": false,
"binsec_replay_attempted": false,
"binsec_replay_ok": false,
"lean_available": false,
"lean_replay_attempted": false,
"lean_replay_ok": false,
"verified_by_required_toolchain": false,
"production_memory_non_interference_proof": false,
"secret_dependent_memory_access_absence_proof": false,
"side_channel_closure_ready": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"evidence_json_path": "",
"evidence_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"gl121_mlkem_fips203_conformance_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_id": "",
"acceptance_template": "",
"required_tool_family": "",
"closure_lane": "",
"workpack_path": "",
"workpack_sha256": "",
"workpack_matches": false,
"integrity_summary_path": "",
"integrity_summary_sha256": "",
"integrity_gate_ready": false,
"historical_artifacts_restored": false,
"missing_artifact_lane_empty": false,
"source_readme_path": "",
"source_readme_sha256": "",
"tests_readme_path": "",
"tests_readme_sha256": "",
"lean_path": "",
"lean_sha256": "",
"ml_kem_source_path": "",
"ml_kem_source_sha256": "",
"native_ml_kem_source_path": "",
"native_ml_kem_source_sha256": "",
"source_readme_static_ready": false,
"tests_readme_static_ready": false,
"restore_missing_artifacts_ready": false,
"lean_static_ready": false,
"lean_available": false,
"lean_replay_attempted": false,
"lean_replay_ok": false,
"placeholder_absent": false,
"boundary_comment_present": false,
"ml_kem_source_static_ready": false,
"native_profile_static_ready": false,
"cargo_ml_kem_dependency_present": false,
"backend_vendor_backed": false,
"backend_non_autonomous": false,
"autonomous_backend_admitted": false,
"native_full_encaps_decaps": false,
"foundation_source_map_ready": false,
"existing_replay_artifacts_ready": false,
"supported_parameter_set_count": 0,
"fips203_parameter_set_count": 0,
"strict_fips203_conformance_proof": false,
"mechanized_fips203_algorithm_proof": false,
"verified_by_required_toolchain": false,
"production_mlkem_fips203_conformance_proof": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"evidence_json_path": "",
"evidence_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"gl125_126_127_mlkem_algorithm_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_ids": "",
"acceptance_template": "",
"required_tool_family": "",
"closure_lane": "",
"workpack_path": "",
"workpack_sha256": "",
"workpack_matches": false,
"integrity_summary_path": "",
"integrity_summary_sha256": "",
"integrity_gate_ready": false,
"historical_artifacts_restored": false,
"missing_artifact_lane_empty": false,
"vendor_src_lib_path": "",
"vendor_src_lib_sha256": "",
"tests_readme_path": "",
"tests_readme_sha256": "",
"lean_path": "",
"lean_sha256": "",
"ml_kem_source_path": "",
"ml_kem_source_sha256": "",
"native_ml_kem_source_path": "",
"native_ml_kem_source_sha256": "",
"hacspec_tests_path": "",
"hacspec_tests_sha256": "",
"hacspec_spec_path": "",
"hacspec_spec_sha256": "",
"vendor_src_lib_static_ready": false,
"tests_readme_static_ready": false,
"restore_missing_artifacts_ready": false,
"hacspec_correspondence_static_ready": false,
"hacspec_spec_static_ready": false,
"hacspec_replay_available": false,
"hacspec_replay_ok": false,
"lean_static_ready": false,
"lean_available": false,
"lean_replay_attempted": false,
"lean_replay_ok": false,
"placeholder_absent": false,
"boundary_comment_present": false,
"wrapper_keygen_binding_static_ready": false,
"wrapper_encaps_binding_static_ready": false,
"wrapper_decaps_binding_static_ready": false,
"native_keygen_surface_present": false,
"native_encaps_surface_present": false,
"native_decaps_surface_present": false,
"native_full_encaps_decaps": false,
"backend_vendor_backed": false,
"backend_non_autonomous": false,
"autonomous_backend_admitted": false,
"keygen_formal_proof": false,
"encaps_formal_proof": false,
"decaps_formal_proof": false,
"production_mlkem_algorithm_proof": false,
"verified_by_required_toolchain": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"evidence_json_path": "",
"evidence_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"gl141_144_mldsa_fips204_algorithm_workbench": {
"version": "",
"summary": "",
"summary_sha256": "",
"workbench_ready": false,
"requirement_ids": "",
"acceptance_template": "",
"required_tool_family": "",
"closure_lane": "",
"scope_decision": "",
"workpack_path": "",
"workpack_sha256": "",
"workpack_matches": false,
"nist_fips204_page": "",
"nist_fips204_pdf": "",
"official_parameter_sets_represented": "",
"not_represented_parameter_sets": "",
"signature_surface_path": "",
"signature_surface_sha256": "",
"mldsa_module_path": "",
"mldsa_module_sha256": "",
"mldsa_algorithm_source_path": "",
"mldsa_algorithm_source_sha256": "",
"lean_path": "",
"lean_sha256": "",
"fips204_parameter_ledger_ready": false,
"signature_surface_static_ready": false,
"mldsa_internal_algorithm_surface_ready": false,
"seeded_sign_verify_vector_ready": false,
"rejection_corpus_ready": false,
"certificate_static_ready": false,
"api_surface_static_ready": false,
"homogeneity_profile_ready": false,
"glbm_profile_evidence_ready": false,
"lean_static_ready": false,
"lean_available": false,
"lean_replay_attempted": false,
"lean_replay_ok": false,
"cargo_mldsa_replay_available": false,
"cargo_mldsa_replay_attempted": false,
"cargo_mldsa_replay_ok": false,
"backend_in_tree": false,
"external_dependency": false,
"strict_fips204_conformance_proof": false,
"keygen_formal_proof": false,
"sign_formal_proof": false,
"verify_formal_proof": false,
"production_mldsa_algorithm_proof": false,
"verified_by_required_toolchain": false,
"counts_as_p6_closure_count": 0,
"p6_closure_claim_allowed": false,
"evidence_json_path": "",
"evidence_json_sha256": "",
"typed_evidence_path": "",
"typed_evidence_compiles": false,
"manifest_path": "",
"claim_boundary": ""
},
"critical_queue_head": [],
"priority_queue_head": [],
"public_queue_truncated": false,
"full_workpack_reference": "",
"claim_firewall": {
"p6_workpack_closure_claim_allowed": false,
"p6_closure_claim_allowed": false,
"first_local_audit_superseded": false,
"external_operator_evidence_count": 0,
"true_decentralization_proven": false,
"public_economic_finality": false,
"public_endpoint_admits_sovereign_claims": false,
"counts_as_sovereign_closure_count": 0,
"not_third_party_audit": true,
"not_legal_or_financial_guarantee": true
},
"next_required_internal_step": "Work the remaining queue by lane: primary evidence, scope activation, requirement rewrite, assumption acceptance, and re-audit of present artifacts; then rerun the P6 audit and sovereign readiness gates.",
"claim_boundary": "p6_local_audit_closure_workpack_only_no_gap_closure_claim"
}API publique : GET /api/public/p6/local-audit-workpack