Synthese des audits de verification formelle — ProbatioVault¶

1. Vue d'ensemble¶

Legende : - CONFORME = aucun echec bloquant sur les 4 formalismes. - PARTIEL = TLA+ non concluant (erreur outil) mais Prolog/Alloy/Z-lint conformes. - NON CONFORME = au moins 1 formalisme bloquant en echec (ASSUME false).

2. Resultats par couche formelle¶

2.1 TLA+ — Model checking (TLC)¶

7/9 PASS, 1 FAIL (ASSUME false), 1 ERROR (outil tue — espace d'etats trop grand malgre bornes reduites).

Total etats explores (hors NF Z42-013) : 86 637 854

Cause du FAIL ISO 14641 : Violation ASSUME a la ligne 22 (AnchorAssume_States). Le modele declare l'etat RESTITUTED que le code n'implemente pas encore.

Cause de l'ERROR NF Z42-013 : Le modele a un espace d'etats combinatoire (journal × attestations × copies × integrite × horloge) qui depasse les capacites locales meme avec les bornes reduites (MAX_DOCS=1, MAX_JOURNAL_ENTRIES=2, MAX_INTEGRITY_AGE=2, MAX_ITERATIONS=2). Le processus TLC a ete tue apres >10 min et 1.5 milliard d'etats explores. Les 3 autres formalismes (Prolog, Alloy, Z-lint) sont tous PASS pour cette norme.

2.2 Alloy — Verification structurelle (SAT)¶

9/9 PASS. Aucun contre-exemple sur aucune norme. Les modules d'ancrage (_AnchoredFacts_*.als) passent egalement.

2.3 Z Notation — Lint structurel¶

9/9 PASS complet (PD-281 : discrimination state machine vs classification eliminant les faux positifs).

2.4 Prolog — Conformite (faits reels du code)¶

9/9 conformes au niveau compliance (tous les checks bloquants passent).

2.5 Prolog — Completude (ecarts normatifs, non bloquant)¶

3. Analyse des ecarts¶

3.1 Ecart TLA+ ISO 14641 (1 norme)¶

La violation ASSUME est un etat defini dans le modele TLA+ mais pas encore implemente dans le code (RESTITUTED). Le mecanisme d'ancrage fonctionne correctement — il detecte exactement ce qu'il doit detecter.

Story de remediation : PD-279 (RESTITUTED)

3.2 Limitation TLA+ NF Z42-013¶

Le modele NF Z42-013 est intrinsiquement combinatoire : le produit cartesien des variables d'etat (journal, attestations, copies geographiques, derniere verification d'integrite, horloge) produit un espace d'etats qui depasse la capacite de verification locale. Les bornes ont ete reduites de MAX_JOURNAL_ENTRIES=4, MAX_INTEGRITY_AGE=4, MAX_ITERATIONS=3 a MAX_JOURNAL_ENTRIES=2, MAX_INTEGRITY_AGE=2, MAX_ITERATIONS=2, mais l'espace reste trop grand.

Mitigation : Les 3 autres formalismes (Prolog 18/18, Alloy PASS, Z-lint 42/42) fournissent une couverture suffisante pour cette norme. Une refactorisation du modele TLA+ (decomposition en sous-modules, symmetrie reduction) est envisageable pour un run futur.

3.3 Ecarts Z-lint¶

Aucun ecart Z-lint. PD-281 a elimine les faux positifs par discrimination state machine (status) vs classification (event_type, envelope_type, document_category, validation_status).

3.4 Ecarts Completude (non bloquants)¶

Les ecarts de completude NF/ISO sont des documents de gouvernance manquants (PAE, RACI, retention policy, etc.) qui ne sont pas du code mais de la documentation organisationnelle. Traces dans les stories PD-249 a PD-261.

4. Metriques globales¶

5. Historique¶

6. Conclusion¶

6.1 Etat de conformite¶

6.2 Ameliorations depuis dernier audit (01/03 matin)¶

• PV Proof TLA+ : FAIL (ASSUME) → PASS (77M etats explores, PD-280 implemente)
• Prolog compliance : 202/202 → 213/213 (nouveaux checks ajoutes)
• Faits extraits : 2275 → 2384 (+109 faits, extraction enrichie)
• PV Completude : ecarts PV Anchor/Audit/Proof → PASS (tous les 5 protocoles PV complets)

Rapport genere le 2026-03-01. Rapports detailles par norme : docs/normes/<slug>/formal/AUDIT-REPORT.md.