PD-297 — Boucle d'enrichissement formel¶

1. Contexte¶

PD-296 a intégré la vérification formelle (Art. VIII CONSTITUTIONAL) en mode lecture seule : formal-check.sh invoque le coherence check Prolog inter-EB, mais les scopes contracts, code et full retournent SKIP car formal-verify.py n'existe pas. Les prédicats extraits par extract-eb-predicates.py sont éphémères — ils ne sont jamais persistés dans la base formelle de ProbatioVault-formal.

Résultat : la base formelle ne s'enrichit pas au fil des stories. Chaque story repart de la même base statique (ontologie + normes). Les invariants découverts (INV-XXX-01..N), les code-contracts, et les patterns vérifiés ne sont pas capitalisés.

2. Problème¶

3 trous identifiés après PD-296 (2026-04-13) :

1. Pas d'enrichissement de l'ontologie : quand une story ajoute des invariants (INV-XXX-01..N), ils ne sont jamais injectés dans la base Prolog de ProbatioVault-formal. La prochaine story du même domaine ne bénéficie pas des nouvelles règles.

2. Pas d'extraction systématique des prédicats : extract-eb-predicates.py extrait des prédicats temporaires, les compare, puis les jette. Pas de data/ontology.pl persistant accumulant les prédicats de toutes les stories.

3. formal-verify.py n'existe pas : les scopes contracts, code, full de formal-check.sh retournent SKIP. Seule la cohérence Prolog inter-EB fonctionne.

3. Objectif¶

Fermer la boucle de vérification formelle : chaque story DONE enrichit la base formelle, et les stories suivantes bénéficient de cette base étendue. Implémenter formal-verify.py pour que formal-check.sh retourne GO/FAIL (pas SKIP) pour tous les scopes.

4. Périmètre¶

4.1 Enrichissement ontologie (step 10 / story DONE)¶

• Extraire les prédicats de la spec + code-contracts de la story terminée
• Les persister dans ProbatioVault-formal/coherence/ontology/stories/PD-XXX.pl
• Recompiler la base Prolog globale (_ontology-facts.pl étendu)
• Intégrer dans /gov-retrospective (step 10)

4.2 Enrichissement modèles TLA+/Alloy/Z (step 10)¶

• Extraire les invariants TLA+/Alloy/Z depuis les code-contracts
• Les ajouter aux modèles formels du domaine dans ProbatioVault-formal/normes/{norme}/formal/
• Script scripts/extract-formal-invariants.py
• 4 formalismes : Prolog, TLA+, Alloy, Z

4.3 Implémentation formal-verify.py¶

• Pipeline complet chargeant les modèles formels du domaine
• Vérifie le code généré / les contracts contre les modèles
• Scopes : contracts, code, full
• Remplace le SKIP actuel de formal-check.sh par un vrai verdict GO/FAIL

4.4 Test de non-régression formelle¶

• Après enrichissement, relancer le coherence check sur la base étendue
• Vérifier qu'aucune régression n'est introduite (nouveaux prédicats ne contredisent pas les anciens)

4.5 Documentation¶

• Mise à jour procedures.md et workflow-rules.md
• Point d'intégration step 10 / gov-retrospective

5. Hors périmètre¶

• Modification des normes existantes dans ProbatioVault-formal (lecture seule)
• Enrichissement rétroactif des stories déjà DONE (capitalisation future uniquement)
• Modification de formal-check.sh (seul formal-verify.py est créé, le wrapper existant l'appelle déjà)

6. Dépendances¶

7. Critères de succès¶

8. Invariants¶

9. Arbitrages et décisions¶

10. Projets concernés¶