PD-296 — Intégration systématique de la vérification formelle dans le workflow /gov¶

1. Contexte¶

Le workflow /gov orchestre la production de code pour l'ensemble de l'écosystème ProbatioVault (backend, app, infra, site, formal). L'infrastructure de vérification formelle existe dans ProbatioVault-formal : 4 modèles (TLA+, Prolog, Alloy, Z), 9 normes, 8 modules de cohérence. Deux skills l'exploitent : /coherence (vérification inter-EB via Prolog) et /formal-verify (pipeline complet multi-modèles).

Aujourd'hui /coherence est appelé une seule fois (step 0, Phase 3.5, après validation du besoin). /formal-verify n'est jamais appelé par /gov. Le résultat : le workflow produit du code sans jamais valider formellement qu'il respecte les propriétés prouvées. C'est un trou dans la chaîne de garantie.

Les preuves formelles sont principalement motivées par le code ProbatioVault : invariants crypto, protocoles blockchain, conformité légale, sécurité authentification. Mais l'intégration concerne toutes les stories de tous les projets — une story qui ajoute un bouton CSS peut casser un invariant de sécurité si elle touche un composant partagé.

Source : audit documentation PD-295 (2026-04-12).

2. Besoin¶

En tant que PO/architecte ProbatioVault, je veux que la vérification formelle soit invoquée systématiquement à chaque étape pertinente du workflow /gov et que son échec bloque la gate concernée, afin de garantir que le code produit respecte les propriétés formellement prouvées et que cette garantie soit constitutionnelle (non skippable).

3. Points d'intégration¶

3.1 Après step 1 (spécification) — `/coherence check`¶

Vérifier que la nouvelle spécification ne contredit pas les invariants des stories existantes dans le même domaine. Déjà fait au step 0 sur le besoin, à reproduire sur la spec qui est plus détaillée et peut introduire de nouvelles contradictions.

Déclencheur : automatique après sauvegarde de PD-XX-specification.md. Comportement si échec : BLOQUE le passage à l'étape 2. Liste des contradictions affichée. Correction de la spec obligatoire avant de continuer.

3.2 Après step 4 (plan + code-contracts) — `/formal-verify contracts`¶

Prouver que les code-contracts formalisent correctement les invariants de la spécification. Vérifier la cohérence interne du plan (pas de dépendances circulaires, pas de contraintes insatisfiables).

Déclencheur : automatique après sauvegarde de PD-XX-plan.md + code-contracts.yaml. Modèles invoqués : Prolog (cohérence contracts vs invariants spec), Alloy (modèle de données si applicable). Comportement si échec : BLOQUE le passage à Gate 5. Corrections du plan/contracts obligatoires.

3.3 Pré-Gate 5 — cohérence interne plan¶

Intégrer dans /gov-check-plan une Phase 4 "Vérification formelle" qui invoque /formal-verify --scope plan avant de soumettre à Gate 5.

Comportement si échec : BLOQUE Gate 5 (même effet que les Phases 0-3 existantes du check-plan).

3.4 Après step 6 (code) — `/formal-verify code`¶

Valider le code généré contre les specs formelles. TLA+ pour les protocoles, Alloy pour les modèles de données, Z pour les préconditions/postconditions.

Déclencheur : automatique après Phase 6c (synthèse), avant le passage à step 7. Comportement si échec : BLOQUE le passage à step 7 (acceptabilité). Corrections du code obligatoires (boucle correction step 6 → re-vérification formelle).

3.5 Pré-Gate 8 — preuve formelle complète¶

Vérification formelle finale que l'implémentation préserve tous les invariants de la spec. C'est le dernier filet de sécurité avant la clôture.

Déclencheur : automatique dans /gov-accept après Phase 2 (reviews LLM), avant soumission à Gate 8. Modèles invoqués : pipeline complet /formal-verify (TLA+ + Prolog + Alloy + Z). Comportement si échec : BLOQUE Gate 8. Non négociable.

3.6 Article VIII CONSTITUTIONAL — vérification formelle obligatoire¶

Ajouter un 8e article au document constitutionnel :

Article VIII — Vérification formelle
La vérification formelle est une condition nécessaire au passage de chaque gate (3, 5, 8).
Son échec est BLOQUANT et non contournable.
Aucune story ne peut être clôturée (transition Jira → Done) si une vérification formelle
a échoué sans être corrigée.
Le pipeline /formal-verify est invoqué systématiquement pour TOUTES les stories de TOUS
les projets ProbatioVault, sans exception.

4. Contraintes¶

Stack existante : ProbatioVault-formal est déjà opérationnel (TLA+, Prolog, Alloy, Z). Pas de nouvel outil à intégrer.
Performance : /formal-verify prend 30s à 3min selon la complexité. Acceptable dans un workflow qui dure des heures.
Dégradation : si ProbatioVault-formal est indisponible (erreur Python, dépendance cassée), le comportement est fail-closed : la gate est bloquée, pas contournée.
Toutes les stories, tous les projets : pas de filtre par domaine ou par type. Si une story CSS casse un invariant partagé, la vérification formelle le détectera.

5. Livrables¶

Skills modifiés¶

.claude/commands/gov.md : ajout appels /coherence après step 1, /formal-verify après step 4 et step 6
.claude/commands/gov-gate.md : ajout phase vérification formelle pré-verdict pour G3, G5, G8
.claude/commands/gov-accept.md : ajout phase vérification formelle après reviews LLM
.claude/commands/gov-check-plan.md : ajout Phase 4 "Vérification formelle"
.claude/commands/gov-step.md : appels cohérence/formal après steps 1, 4, 6

Documents modifiés¶

governance/CONSTITUTIONAL.md : ajout Article VIII
.claude/rules/procedures.md : ajout procédures vérification formelle par étape
.claude/rules/workflow-rules.md : ajout règle "vérification formelle bloquante"
CLAUDE.md : mention Article VIII dans la table constitutionnelle

Scripts (si nécessaire)¶

scripts/formal-check.sh : wrapper qui invoque /formal-verify ou /coherence selon le contexte (step, projet, type de vérification) et retourne un JSON résumé {"verdict":"GO|FAIL","details":...}. Simplifie l'intégration dans les skills.

6. Critères de succès¶

CS-1 : /coherence est invoqué après step 0 ET step 1 (pas seulement step 0)
CS-2 : /formal-verify est invoqué après step 4, step 6, et pré-Gate 8
CS-3 : un échec de vérification formelle bloque la gate (test : simuler un échec et vérifier que la gate ne passe pas)
CS-4 : Article VIII est ajouté à CONSTITUTIONAL.md et référencé dans CLAUDE.md
CS-5 : une story sur n'importe quel projet (backend, app, site) déclenche la vérification formelle

7. Hors-scope¶

Pas de nouveau modèle formel (TLA+/Prolog/Alloy/Z sont suffisants)
Pas de refonte de ProbatioVault-formal
Pas d'optimisation de performance des vérifications
Pas de vérification formelle en CI GitLab (déjà en place via tla-verify job)

8. Arbitrages¶

Toutes les stories, sans exception (arbitrage PO 2026-04-13)
Échec = bloquant (arbitrage PO 2026-04-13) — pas informatif, pas warning, BLOQUE la gate