PD-296 — Vérification formelle systématique et bloquante du workflow /gov¶

1. Objectif¶

La User Story PD-296 DOIT imposer une vérification formelle systématique aux points critiques du workflow /gov, avec un effet bloquant non contournable en cas d’échec, afin de garantir que les artefacts produits restent conformes aux invariants formels (Prolog, Alloy, TLA+, Z) sur toutes les stories et tous les projets ProbatioVault.

2. Périmètre / Hors périmètre¶

Inclus¶

• Intégration obligatoire des contrôles formels aux checkpoints suivants :
• STEP1_SPEC_COHERENCE (après step 1),
• STEP4_CONTRACTS_FORMAL (après step 4),
• GATE5_PLAN_FORMAL (pré-Gate 5),
• STEP6_CODE_FORMAL (après step 6c),
• GATE8_FINAL_FORMAL (pré-Gate 8).
• Effet bloquant sur la transition de step/gate en cas d’échec.
• Règle constitutionnelle Article VIII (obligatoire, non skippable).
• Application sans filtre de domaine ou de type de story.
• Contrats de format des données de vérification formelle.
• Contrats de concurrence et idempotence pour exécutions simultanées /gov.

Exclu¶

• Création d’un nouveau modèle formel.
• Refonte de ProbatioVault-formal.
• Optimisation de performance des moteurs formels.
• Changement du job CI GitLab tla-verify.
• Toute règle non testable : hors périmètre.

3. Définitions¶

4. Invariants (non négociables)¶

5. Flux nominaux¶

5.1 Modèle de données contractuel (source unique des formats)¶

Référencement unique : toutes les sections suivantes réutilisent ces IDs (D-296-*) sans redéfinir les formats.

5.2 Bornes numériques contractuelles¶

5.3 SLA temporels (transitions)¶

Aucune autre transition temporelle identifiée.

5.4 Machine d’états des checkpoints (transitions retour explicites)¶

États officiels : PENDING, RUNNING, PASSED, FAILED_BLOCKING.

État PENDING¶

État RUNNING¶

État PASSED (terminal)¶

État FAILED_BLOCKING¶

Comportement au retour/downgrade FAILED_BLOCKING -> PENDING : - Les détails d’échec (D-296-15) sont conservés. - Les verrouillages aval restent actifs jusqu’à passage PASSED. - Le rate-limit et l’idempotence sont réappliqués immédiatement. - Aucune suppression de données historiques.

Checklist machine à états : - [x] Chaque état liste ses transitions sortantes autorisées/interdites. - [x] État terminal explicite : PASSED -> * : INTERDITE. - [x] Modèle couvert par invariants dédiés (INV-296-12, INV-296-13).

5.5 Flux nominaux par checkpoint¶

1. Flux F-296-01 — Step 1 (spec)
2. Déclencheur : SPEC_SAVED (D-296-04) sur PD-XX-specification.md (D-296-10).
3. Checkpoint : STEP1_SPEC_COHERENCE (D-296-03), scope coherence_spec (D-296-05).
4. Résultat :
5. GO => step 2 autorisé.

6. FAIL => step 2 bloqué, contradictions affichées (D-296-15).

7. Flux F-296-02 — Step 4 (plan + contracts)

8. Déclencheur : PLAN_AND_CONTRACTS_SAVED.
9. Checkpoint : STEP4_CONTRACTS_FORMAL, scope formal_contracts.
10. Résultat :
11. GO => éligible pré-Gate 5.

12. FAIL => Gate 5 bloquée.

13. Flux F-296-03 — Pré-Gate 5 (/gov-check-plan Phase 4)

14. Déclencheur : CHECK_PLAN_PHASE4_START.
15. Checkpoint : GATE5_PLAN_FORMAL, scope formal_plan.
16. Résultat :
17. GO => soumission Gate 5 autorisée.

18. FAIL => verdict Gate 5 interdit.

19. Flux F-296-04 — Step 6 (code)

20. Déclencheur : STEP6C_DONE.
21. Checkpoint : STEP6_CODE_FORMAL, scope formal_code.
22. Résultat :
23. GO => step 7 autorisé.

24. FAIL => step 7 bloqué, boucle correction step 6.

25. Flux F-296-05 — Pré-Gate 8 (/gov-accept)

26. Déclencheur : GOV_ACCEPT_PHASE2_DONE.
27. Checkpoint : GATE8_FINAL_FORMAL, scope formal_full.
28. Résultat :
29. GO => soumission Gate 8 autorisée.
30. FAIL => Gate 8 bloquée, clôture interdite.

5.6 Mécanismes de protection distribuée (obligatoire)¶

Checklist protection distribuée : - [x] Lock : scope + TTL + comportement lock non acquis définis. - [x] Idempotence : clé + durée de déduplication définies. - [x] Réconciliation : intervalle + seuil orphelin + rattrapage définis. - [x] Rate-limit : granularité story + quota + rejet définis. - [x] Clearing : nombre de cycles conformes + comptage définis.

5.7 Contraintes inter-modules¶

5.8 Clauses obligatoires “non applicables”¶

• Stratégie de migration DDL : non applicable (aucune modification de colonne SQL).
• Atomicité multi-composant DB + queue/append-only : non applicable (pas de flux DB+queue dans PD-296).
• Invariant envelope encryption crypto : non applicable (domaine tooling/governance, pas crypto/crypto-proof).

5bis. Diagrammes (si applicable)¶

Diagramme d’état (>= 3 états)¶

stateDiagram-v2
    [*] --> PENDING

    PENDING --> RUNNING: trigger_event valide
    PENDING --> PASSED: INTERDITE
    PENDING --> FAILED_BLOCKING: INTERDITE

    RUNNING --> PASSED: verdict=GO
    RUNNING --> FAILED_BLOCKING: verdict=FAIL|timeout|tool_unavailable
    RUNNING --> PENDING: INTERDITE

    FAILED_BLOCKING --> PENDING: correction artefact + relance
    FAILED_BLOCKING --> RUNNING: INTERDITE (retrigger requis)
    FAILED_BLOCKING --> PASSED: INTERDITE (preuve manquante)

    PASSED --> PENDING: INTERDITE (etat terminal)
    PASSED --> RUNNING: INTERDITE (etat terminal)
    PASSED --> FAILED_BLOCKING: INTERDITE (etat terminal)
    PASSED --> [*]

Diagramme de séquence (flow multi-services)¶

sequenceDiagram
    participant GS as /gov-step
    participant CO as /coherence
    participant FV as /formal-verify
    participant GCP as /gov-check-plan
    participant GA as /gov-accept
    participant GG as /gov-gate
    participant FSM as FSM/Jira

    GS->>GS: save(PD-XX-specification.md)
    GS->>CO: check(predicates(spec_markdown))
    CO-->>GS: formal_check_result_json{checkpoint=STEP1_SPEC_COHERENCE, verdict}
    alt verdict=FAIL
        GS->>FSM: block step1->step2
    else verdict=GO
        GS->>FSM: allow step1->step2
    end

    GS->>GS: save(PD-XX-plan.md + code-contracts.yaml)
    GS->>FV: verify(invariants(spec) + contracts_yaml + plan_constraints_graph)
    FV-->>GS: formal_check_result_json{checkpoint=STEP4_CONTRACTS_FORMAL, verdict}
    alt verdict=FAIL
        GS->>FSM: block Gate 5
    else verdict=GO
        GCP->>FV: verify(plan_constraints_graph)
        FV-->>GCP: formal_check_result_json{checkpoint=GATE5_PLAN_FORMAL, verdict}
        GCP->>FSM: allow_or_block Gate 5
    end

    GS->>FV: verify(extract_facts(code_ast) + model_checks)
    FV-->>GS: formal_check_result_json{checkpoint=STEP6_CODE_FORMAL, verdict}
    GS->>FSM: allow_or_block step6->step7

    GA->>FV: verify_full(extract_facts(code_ast) + TLA+ + Prolog + Alloy + Z)
    FV-->>GA: formal_check_result_json{checkpoint=GATE8_FINAL_FORMAL, verdict}
    alt verdict=FAIL
        GA->>FSM: block Gate 8
    else verdict=GO
        GA->>GG: submit Gate 8
        GG->>FSM: continue verdict process
    end

6. Cas d’erreur¶

7. Critères d’acceptation (testables)¶

8. Scénarios de test (Given / When / Then)¶

1. Given une spec sauvegardée, When checkpoint STEP1_SPEC_COHERENCE retourne GO, Then step 2 est autorisé.
2. Given une spec sauvegardée, When checkpoint STEP1_SPEC_COHERENCE retourne FAIL, Then step 2 est bloqué et la liste des contradictions est visible.
3. Given plan + code-contracts sauvegardés, When STEP4_CONTRACTS_FORMAL retourne FAIL, Then Gate 5 est bloquée.
4. Given /gov-check-plan en phase 4, When GATE5_PLAN_FORMAL retourne FAIL, Then aucun verdict Gate 5 n’est soumis.
5. Given step 6c terminé, When STEP6_CODE_FORMAL retourne FAIL, Then step 7 est interdit jusqu’à correction et relance.
6. Given /gov-accept phase 2 terminée, When GATE8_FINAL_FORMAL retourne FAIL, Then Gate 8 est bloquée.
7. Given moteur formel indisponible, When un checkpoint est déclenché, Then résultat FAIL avec TOOL_UNAVAILABLE et blocage immédiat.
8. Given deux déclenchements concurrents sur même story_id + checkpoint_id, When le second démarre, Then il est rejeté (CONCURRENT_RUN).
9. Given une relance avec même idempotency_key et même payload, When elle est rejouée, Then le résultat est identique sans double exécution.
10. Given une story avec échec formel non résolu, When transition Jira vers Done est tentée, Then la transition est refusée.
11. Given une story projet app ou site, When workflow /gov atteint les checkpoints, Then les mêmes contrôles formels s’exécutent (pas d’exception projet).
12. Given timeout dépassé sur un checkpoint, When la fenêtre SLA expire, Then état RUNNING -> FAILED_BLOCKING et progression aval interdite.

9. Hypothèses explicites¶

10. Points à clarifier¶

10.1 Contraintes techniques (stack projet cible)¶

• Projet cible de la story : ProbatioVault-ia-governance.
• Stack réelle du projet cible :
• Scripts Shell (bash/zsh) pour orchestration workflow,
• Python 3 pour scripts d’indexation/traitement gouvernance,
• Artefacts Markdown, YAML, JSON,
• Composant Node.js (mcp-signal) pour intégration MCP Signal.
• Dépendance externe de vérification formelle (repo ProbatioVault-formal) :
• Python, SWI-Prolog, TLA+, Alloy, Z.
• Contrainte explicite : aucune substitution de stack (pas de Swift/SwiftUI, pas de Spring Boot) n’est autorisée pour ce projet.

10.2 Questions ouvertes¶

Références¶

• Epic : non fournie dans l’entrée (donnée manquante).
• JIRA : PD-296.
• Repos concernés : ProbatioVault-ia-governance, ProbatioVault-formal, et stories cibles backend/app/site/infra/doc/formal.
• Documents associés :
• docs/epics/tooling/PD-296-formal-verification-integration/PD-296-besoin.md
• governance/CONSTITUTIONAL.md
• CLAUDE.md
• .claude/commands/gov.md
• .claude/commands/gov-step.md
• .claude/commands/gov-gate.md
• .claude/commands/gov-check-plan.md
• .claude/commands/gov-accept.md
• .claude/commands/coherence.md
• .claude/commands/formal-verify.md