Methodologie de verification formelle — ProbatioVault¶

Table des matieres¶

1. Objet et portee
2. Fondement theorique
3. Les quatre formalismes
4. 3.1 TLA+ — Logique temporelle des actions
5. 3.2 Alloy — Analyse structurelle par solveur SAT
6. 3.3 Z Notation — Specification mathematique
7. 3.4 Prolog — Verification de conformite directe
8. Pipeline d'extraction
9. Pipeline de verification
10. Mecanisme d'ancrage
11. Piste d'audit
12. Tracabilite
13. Limites et perimetre
14. 9.5 Feuille de route d'amelioration
15. Annexe A — Demonstration complete ANCHOR-16
16. Annexe B — Arborescence des fichiers
17. Annexe C — Glossaire

1. Objet et portee¶

1.1 Objectif¶

Ce document decrit la methodologie de verification formelle utilisee par ProbatioVault pour verifier formellement que les implementations logicielles sont conformes aux specifications normatives. Il constitue la reference methodologique pour tout audit de conformite et est concu pour etre auto-porteur : un auditeur n'a pas besoin de lire d'autres documents pour comprendre la demarche.

La verification formelle ProbatioVault repose sur quatre systemes formels complementaires, appliques systematiquement a chaque norme. Chaque systeme apporte une garantie distincte, et leur combinaison constitue une defense en profondeur contre les defauts de conception et d'implementation.

1.2 Perimetre de verification¶

La methodologie s'applique a l'ensemble des normes ProbatioVault, internes et externes.

Protocoles internes ProbatioVault :

Standards externes de reference :

1.3 Garanties apportees¶

La verification formelle ProbatioVault apporte les assurances suivantes (toutes bornees par le scope d'exploration — cf. Section 9 pour les limites) :

1. Correction du design — Le modele TLA+ verifie par model checking exhaustif que les proprietes de surete (invariants) sont satisfaites dans tous les etats atteignables du systeme dans le scope configure.
2. Coherence structurelle — Le modele Alloy verifie par solveur SAT qu'aucune configuration structurelle ne viole les assertions dans le scope explore. L'absence de contre-exemple constitue une assurance formelle bornee.
3. Rigueur mathematique — La specification Z exprime les proprietes en theorie des ensembles et logique des predicats, avec pre/post-conditions explicites pour chaque operation. Les theoremes Z sont formules comme contrats mathematiques auditables (cf. Section 3.3.5).
4. Conformite de l'implementation — Les regles Prolog verifient directement que les artefacts du code source reel (entites, colonnes, services, methodes, gardes, triggers, infrastructure) satisfont chaque exigence normative.
5. Ancrage au code reel — Les modeles formels sont lies au code source par extraction automatique. Les constantes et structures extraites du code sont injectees dans les modeles. Si le code ne correspond pas au modele, la verification echoue immediatement.

1.4 Hors perimetre¶

Les elements suivants ne sont pas couverts par la verification formelle :

• Performance et scalabilite — Temps de reponse, debit, consommation memoire.
• Correction des primitives cryptographiques — La verification formelle suppose que les bibliotheques cryptographiques sous-jacentes (OpenSSL, AWS CloudHSM, node:crypto) sont correctes. Seule leur utilisation est verifiee.
• Securite reseau — Configuration TLS, pare-feu, regles de routage.
• Interface utilisateur — Comportement de l'application front-end.
• Dependances tierces — Correction des modules npm, drivers de base de donnees.
• Sur-implementation — La verification verifie que le code satisfait les exigences (RFC ⊆ SOURCE). Elle ne verifie pas que le code ne fait rien de plus (SOURCE ⊆ RFC).

2. Fondement theorique¶

2.1 Principe d'inclusion predicats_RFC ⊆ predicats_SOURCE¶

Le fondement mathematique de la verification ProbatioVault repose sur un principe unique :

Theoreme de conformite : Soit P_RFC l'ensemble des predicats formalisant les exigences d'une norme, et P_SOURCE l'ensemble des predicats extraits du code source. Le systeme est conforme si P_RFC ⊆ P_SOURCE — c'est-a-dire que chaque exigence normative est satisfaite par un artefact du code reel.

Precision : la relation est une condition suffisante de conformite, pas une equivalence. La verification etablit que toutes les exigences du RFC sont satisfaites dans le code (P_RFC ⊆ P_SOURCE), mais ne verifie pas que le code ne contient rien de plus que les exigences (P_SOURCE ⊆ P_RFC). Autrement dit : la conformite est verifiee, pas la minimalite.

Ce principe est applique independamment par chaque formalisme :

La direction de l'inclusion est cruciale :

• P_RFC ⊆ P_SOURCE (verifie) : toute exigence du RFC est implementee dans le code.
• P_SOURCE ⊆ P_RFC (non verifie) : le code pourrait contenir des fonctionnalites non specifiees.

2.2 Defense en profondeur¶

Quatre formalismes sont necessaires car chacun detecte des classes de defauts differentes.

Exemple concret : une exigence stipule que « un batch ne peut etre finalise que si le nombre de confirmations blockchain est suffisant ».

• TLA+ verifie que dans toute sequence d'etats possible, un batch FINALIZED a toujours confirmations >= FINALITY_DEPTH.
• Alloy verifie que dans toute configuration structurelle valide, un batch Finalized a un champ confirmations >= 1.
• Z verifie que la precondition formelle de l'operation FinalizeBatch exige confirmations >= finalityDepth.
• Prolog verifie que dans le code reel, la colonne confirmation_count existe ET que la methode finalizeBatch() contient une garde sur cette colonne.

2.3 Ancrage au code reel¶

La verification formelle traditionnelle opere sur des modeles abstraits, deconnectes du code reel. Un modele peut etre correct alors que l'implementation diverge. ProbatioVault elimine ce risque par un mecanisme d'ancrage automatique :

1. Extraction automatique — Le script extract-facts.py analyse le code source reel (TypeScript, SQL, Terraform) et genere des fichiers de faits dans les 4 formats formels.
2. Regeneration systematique — Les fichiers d'ancrage sont regeneres a chaque build CI. Ils portent la mention DO NOT EDIT — regenerated at each CI build.
3. Controle de compatibilite — Pour les types et enumerations, l'ancrage verifie RealStates ⊆ StatusValues (pas d'etat code hors modele). Pour garantir l'absence d'etats modele non implementes, le pipeline verifie aussi StatusValues ⊆ RealStates — les deux inclusions combinees imposent l'egalite RealStates = StatusValues. Pour les invariants, la liaison est unidirectionnelle : le modele exige, le code satisfait.

2.4 Deux niveaux de verification¶

La verification Prolog opere a deux niveaux, par ordre de rigueur croissante :

Niveau 1 — Structurel : l'artefact existe.

%% La colonne confirmation_count existe-t-elle dans l'entite anchor_batch ?
check_confirmation_count_col :-
    entity_column(anchor_batch, confirmation_count, _), !.

Niveau 2 — Semantique : l'artefact est utilise correctement.

%% La methode finalizeBatch() verifie-t-elle la valeur de confirmation_count ?
check_finalize_confirmations_guard :-
    service_method_guard(anchor_batch, finalizeBatch, confirmation_count), !.

Le predicat service_method_guard/3 est extrait du code source par analyse statique des methodes de service. Il represente une precondition metier : la methode finalizeBatch du service anchor_batch contient une garde sur le champ confirmation_count.

Ce double niveau detecte les violations silencieuses : une colonne peut exister dans le schema sans jamais etre verifiee dans la logique metier.

2.5 Diagramme de flux¶

     RFC-{NORM}.md                            Code source
     (source normative)                       (TypeScript, SQL, Terraform)
           │                                         │
           ▼                                         ▼
    ┌──────────────────┐                    ┌──────────────────┐
    │  Formalisation    │                    │  extract-facts.py │
    │  manuelle         │                    │  (automatique)    │
    └────────┬─────────┘                    └────────┬─────────┘
             │                                       │
             ▼                                       ▼
    ┌──────────────────┐                    ┌──────────────────┐
    │  predicats_RFC    │                    │  predicats_SOURCE │
    │                   │                    │                   │
    │  • {Norm}.tla     │                    │  • _AnchoredFacts │
    │  • {Norm}.als     │                    │    _{MODULE}.tla  │
    │  • {Norm}.zed     │                    │  • _AnchoredFacts │
    │  • {norm}_        │                    │    _{MODULE}.als  │
    │    compliance.pl  │                    │  • _generated-    │
    └────────┬─────────┘                    │    z-lint.yaml   │
             │                               │  • _generated-   │
             │                               │    facts.pl      │
             │                               └────────┬─────────┘
             │                                        │
             ▼                                        ▼
    ┌─────────────────────────────────────────────────────────┐
    │                   verify-norm.sh                         │
    │                                                          │
    │  1. TLC  : {Norm}.tla + _AnchoredFacts → 0 violation ?  │
    │  2. Prolog: compliance.pl + _generated-facts → 32/32 ?   │
    │  3. Alloy: {Norm}.als + _AnchoredFacts → UNSAT ?         │
    │  4. z-lint: {Norm}.zed + _generated-z-lint → lint OK ?   │
    │  5. Prolog: completeness.pl (informatif)                 │
    │  6. Score: compliance_scoring.pl (informatif)            │
    └────────────────────────┬────────────────────────────────┘
                             │
                             ▼
                    ┌──────────────────┐
                    │  AUDIT-REPORT.md  │
                    │  Verdict :        │
                    │  CONFORME /       │
                    │  PARTIELLEMENT /  │
                    │  NON CONFORME     │
                    └──────────────────┘

3. Les quatre formalismes¶

3.1 TLA+ — Logique temporelle des actions¶

3.1.1 Nature de la verification¶

TLA+ (Temporal Logic of Actions) est un langage de specification formelle concu par Leslie Lamport pour la modelisation de systemes concurrents et distribues. Le model checker TLC explore exhaustivement l'espace des etats atteignables du systeme et verifie que chaque invariant est satisfait dans chaque etat.

La verification TLA+ apporte une assurance formelle de surete (safety) : si TLC ne trouve aucune violation, alors l'invariant est verifie dans tous les etats atteignables du systeme dans le scope defini par les constantes. Cette assurance est bornee par les constantes du modele (cf. Section 3.1.6).

3.1.2 Comment les exigences RFC deviennent des predicats¶

Chaque exigence normative du RFC est traduite en un ou plusieurs elements du modele TLA+ :

Types et domaines — Les types enumeres du RFC deviennent des ensembles TLA+ :

StatusValues == {"PENDING", "BUILDING", "SUBMITTED",
                 "PENDING_FINALITY", "FINALIZED", "FAILED"}
SignerStatusValues == {"ACTIVE", "REVOKED"}

Actions — Chaque operation du protocole devient une action TLA+ avec des preconditions et postconditions explicites. Le modele PV Anchor definit 11 actions :

Invariants — Chaque propriete de surete du RFC devient un invariant TLA+, verifie dans chaque etat atteignable. Exemple (INV-12, ANCHOR-16) :

(* INV-12 : FinalityDepthEnforced — batch FINALIZED a confirmations >= FINALITY_DEPTH *)
FinalityDepthEnforced ==
    \A id \in batches :
        batch_status[id] = "FINALIZED"
        => batch_confirmations[id] >= FINALITY_DEPTH

Theoremes — Chaque invariant est associe a un theoreme de preservation :

THEOREM Spec => []FinalityDepthEnforced

Ce theoreme affirme que l'invariant FinalityDepthEnforced est satisfait dans tous les etats de toutes les executions conformes a la specification Spec.

Le modele PV Anchor comprend 13 invariants (INV-01 a INV-13) et 10 theoremes (THM-01 a THM-10).

3.1.3 Comment le code source devient des predicats¶

Le script extract-facts.py genere automatiquement un module TLA+ d'ancrage (_AnchoredFacts_{MODULE}.tla) qui etend le modele principal et ajoute des contraintes ASSUME derivees du code reel.

Mecanisme EXTENDS + ASSUME :

---- MODULE _AnchoredFacts_ANCHOR ----
EXTENDS PV_Anchor

\* Mapping code enum -> norm states (from norm.yaml state_mapping)
RealStates == {"PENDING", "BUILDING", "SUBMITTED",
               "PENDING_FINALITY", "FINALIZED", "FAILED"}

\* ASSUME: real states must match model states (double inclusion = egalite)
ASSUME AnchorAssume_States ==
    /\ RealStates \subseteq StatusValues
    /\ StatusValues \subseteq RealStates

Categories de faits ancres :

Chaque ASSUME est un axiome : si le fait extrait du code ne satisfait pas la contrainte du modele, TLC s'arrete immediatement avec une erreur d'assumption.

3.1.4 Comment l'inclusion est prouvee¶

Le model checker TLC opere en deux phases :

Phase 1 — Verification des ASSUMEs : TLC charge le module ancre (qui EXTENDS le modele principal) et evalue chaque ASSUME. Si un ASSUME echoue (par exemple, le code contient un etat PROCESSING absent du modele), TLC s'arrete immediatement avec le message :

Error: Assumption AnchorAssume_States is not satisfied by the initial predicate.

Phase 2 — Exploration exhaustive : TLC explore l'espace des etats en partant de l'etat initial (Init) et en appliquant toutes les actions possibles (Next) a chaque etat. Pour chaque etat atteint, TLC verifie que chaque invariant est satisfait. Si un invariant est viole, TLC produit un contre-exemple : une trace d'execution complete menant a l'etat violant, permettant de reproduire exactement le probleme.

Resultat : 0 violation = aucune violation trouvee dans l'espace d'etats explore. Ceci constitue une assurance formelle bornee (cf. Section 9.5.6 pour les limites du vocabulaire).

Direction de l'inclusion :

• Egalite imposee pour les types : le pipeline genere RealStates depuis le code et verifie RealStates ⊆ StatusValues (pas d'etat code hors modele) et StatusValues ⊆ RealStates (pas d'etat modele absent du code). Les deux ASSUME combines imposent RealStates = StatusValues, une compatibilite stricte.
• Unidirectionnelle pour les invariants : le modele exige des proprietes (ex: FinalityDepthEnforced). Si le code ne les satisfait pas, le model checking ne le detecte pas directement — c'est le role de Prolog.

3.1.5 Configuration¶

Le fichier de configuration TLC (PV_Anchor.cfg) definit les parametres du model checking :

SPECIFICATION Spec

CONSTANTS
    MAX_BATCHES = 1
    MAX_EVENTS = 2
    MAX_ITERATIONS = 6
    FINALITY_DEPTH = 1

CONSTRAINT StateConstraint

INVARIANTS
    TypeInvariant
    ValidTransitions
    FinalizedImmutable
    EventUniqueness
    NoEventsLost
    WindowOrdering
    AuditCompleteness
    MerkleRootPresent
    TxIdPresent
    SignerAddressAppendOnly
    AuditAppendOnly
    FinalityDepthEnforced
    SignerRevocationValid

Les constantes bornent l'espace d'etats pour rendre le model checking faisable en temps fini. La contrainte StateConstraint limite le nombre de batches et l'horloge logique.

3.1.6 Limites¶

• Model checking borne : les constantes MAX_BATCHES=1, MAX_EVENTS=2 limitent l'exploration. Les proprietes sont prouvees pour ces bornes, pas pour des valeurs arbitrairement grandes. En pratique, les defauts de conception se manifestent generalement dans de petites instances (hypothese du petit scope).
• Abstraction des valeurs : les hashes, adresses, et identifiants de transaction sont representes par des entiers abstraits (MerkleValues == 0..10). La verification ne porte pas sur les valeurs reelles.
• Pas de proprietes de vivacite : seules les proprietes de surete (invariants) sont verifiees. Les proprietes de vivacite (« un batch PENDING finit par etre FINALIZED ») ne sont pas modelisees.
• Explosion combinatoire : l'espace d'etats croit exponentiellement avec les constantes. Des bornes trop larges rendent le model checking impraticable.

3.2 Alloy — Analyse structurelle par solveur SAT¶

3.2.1 Nature de la verification¶

Alloy est un langage de modelisation relationnelle cree par Daniel Jackson (MIT). Il utilise un solveur SAT (Satisfiability) pour explorer exhaustivement toutes les configurations possibles d'un modele dans un scope borne, et determiner si une assertion est satisfaite ou si un contre-exemple existe.

La verification Alloy apporte une assurance structurelle bornee : si aucun contre-exemple n'est trouve dans le scope for N, alors l'assertion est satisfaite pour toutes les configurations contenant jusqu'a N atomes par type. Il ne s'agit pas d'une preuve au sens mathematique strict mais d'une verification exhaustive dans un scope fini (hypothese du petit scope, Jackson 2006).

3.2.2 Comment les exigences RFC deviennent des predicats¶

Signatures (sig) — Les structures de donnees du RFC deviennent des signatures Alloy :

sig AnchorBatch {
    status        : one BatchStatus,
    merkleTree    : one MerkleTree,
    events        : some BatchEvent,
    window        : one TemporalWindow,
    txHash        : lone HashValue,
    chainId       : lone Int,
    blockNumber   : lone Int,
    confirmations : lone Int,
    signerAddress : lone SignerAddress
}

Les multiplicites (one, lone, some) expriment directement les contraintes de cardinalite du RFC.

Faits (fact) — Les contraintes structurelles du RFC deviennent des faits Alloy, toujours vrais dans toute instance valide. Le modele PV Anchor comprend 12 faits :

-- ANCHOR-16 : Batch FINALIZED a confirmations >= 1 (FINALITY_DEPTH abstrait)
fact FinalityDepthEnforced {
    all b : AnchorBatch |
        b.status = Finalized implies
            (one b.confirmations and b.confirmations >= 1)
}

-- ANCHOR-17 : Batch SUBMITTED+ a un signer ACTIVE
fact SignerRevocationValid {
    all b : AnchorBatch |
        b.status in (Submitted + PendingFinality + Finalized)
        implies (one b.signerAddress and b.signerAddress.signerStatus = Active)
}

Assertions (assert) — Les proprietes a verifier deviennent des assertions, verifiees par commande check. Le modele PV Anchor comprend 12 assertions :

assert FinalityDepthCheck {
    all b : AnchorBatch |
        b.status = Finalized implies
            (one b.confirmations and b.confirmations >= 1)
}
check FinalityDepthCheck for 5

Commandes run — Des scenarios d'exploration permettent de verifier que le modele est satisfiable (pas trivialement vide) :

run ExampleFinalizedBatch {
    #AnchorBatch = 1
    some b : AnchorBatch | b.status = Finalized
} for 4 but 6 Int

3.2.3 Comment le code source devient des predicats¶

Le script extract-facts.py genere un module Alloy d'ancrage (_AnchoredFacts_{MODULE}.als) contenant des singletons one sig Real_* representant les artefacts reels du code :

module _AnchoredFacts_ANCHOR
open PV_Anchor

-- Real artifact singletons (zero scope cost)
one sig Real_document_secure_file_hash {}
one sig Real_audit_log_entry_hash {}
one sig Real_audit_log_hsm_signature {}
one sig Real_anchor_batch_tx_id {}
one sig Real_anchor_batch_merkle_root {}
one sig Real_anchor_batch_confirmation_count {}
one sig Real_anchor_batch_signer_status {}
one sig Real_WORM_bucket {}
one sig Real_HSM_FIPS {}
one sig Real_journal_trigger {}

Les singletons (one sig) ont un cout de scope nul : ils n'augmentent pas le nombre de configurations a explorer.

Precision sur les one sig : un singleton one sig Real_X {} existe toujours dans toute instance Alloy (exactement un atome). L'expression some Real_X est donc trivialement vraie. L'interet des singletons n'est pas dans la verification some — c'est le mecanisme de generation conditionnelle qui assure la garantie : le module _AnchoredFacts_*.als n'est genere par extract-facts.py que si l'artefact correspondant existe reellement dans le code source. Si la colonne confirmation_count est supprimee du code, le singleton Real_anchor_batch_confirmation_count disparait du module genere, et toute assertion ou fait qui le reference echoue a la compilation Alloy.

Les singletons sont groupes en faits thematiques :

fact AnchoredTSAAndAnchoring {
    some Real_anchor_batch_tx_id
    some Real_anchor_batch_merkle_root
    some Real_anchor_batch_confirmation_count
    some Real_anchor_batch_signer_status
}

Et une assertion combinee verifie la completude des artefacts :

assert AnchoredArtifactsConsistent {
    some Real_anchor_batch_tx_id and
    some Real_anchor_batch_merkle_root and
    some Real_anchor_batch_confirmation_count and
    some Real_anchor_batch_signer_status and
    some Real_WORM_bucket and
    some Real_HSM_FIPS and
    some Real_journal_trigger
    \* ... (tous les singletons)
}
check AnchoredArtifactsConsistent for 4

3.2.4 Comment l'inclusion est verifiee¶

L'analyseur Alloy effectue une verification en deux passes :

Passe 1 — Modele principal : pour chaque commande check AssertionName for N, le solveur SAT cherche un contre-exemple contenant jusqu'a N atomes par type. Si le solveur retourne No counterexample found (souvent note UNSAT), aucun contre-exemple n'existe dans ce scope — l'assertion est satisfaite pour ce scope.

Passe 2 — Artefacts ancres : le module _AnchoredFacts_*.als est genere conditionnellement. Si un artefact requis est absent du code, le singleton correspondant n'est pas genere, et la compilation ou le check echoue.

Resultat : absence de contre-exemple pour toutes les assertions dans le scope explore = assurance formelle bornee que le modele structural est coherent et que le code reel fournit tous les artefacts requis.

3.2.5 Limites¶

• Scope borne : les assertions sont verifiees pour un nombre fini d'atomes (for 5 = jusqu'a 5 instances par type). L'hypothese du petit scope (Jackson, 2006) stipule que la plupart des defauts se manifestent dans de petites instances.
• Pas de raisonnement temporel : Alloy analyse des instantanes (snapshots), pas des sequences d'etats. Les proprietes temporelles sont du ressort de TLA+.
• Abstraction de FINALITY_DEPTH : le modele utilise confirmations >= 1 comme abstraction. La valeur configurable reelle est verifiee par TLA+ et Prolog.

3.3 Z Notation — Specification mathematique¶

3.3.1 Nature de la verification¶

La notation Z est un langage de specification formelle base sur la theorie des ensembles ZFC et le calcul des predicats du premier ordre. Developpe a l'Universite d'Oxford, Z est un standard ISO (ISO/IEC 13568:2002). Il fournit la specification la plus rigoureuse mathematiquement, avec des schemas explicites pour les donnees, l'etat, et les operations.

3.3.2 Comment les exigences RFC deviennent des predicats¶

Types enumeres — Les enumerations du RFC deviennent des types libres Z :

BatchStatus ::= PENDING | BUILDING | SUBMITTED | PENDING_FINALITY | FINALIZED | FAILED
SignerStatus ::= ACTIVE | REVOKED

Schemas de donnees — Chaque structure du RFC devient un schema Z avec des contraintes internes :

┌─ AnchorBatch ────────────────────────────────────────
│  batchId        : BatchId
│  status         : BatchStatus
│  merkleRoot     : HashBytes
│  txId           : TxHashBytes
│  chainId        : ChainIdStr
│  blockNumber    : ℕ
│  confirmations  : ℕ
│  signerAddress  : SignerAddressStr
│  events         : ℙ₁ AnchorEvent
│  window         : TemporalWindow
├───────────────────────────────────────────────────────────
│  batchId ≠ ∅
│  #events ≥ 1
│  window.windowStart < window.windowEnd
└───────────────────────────────────────────────────────────

Schema d'etat — L'etat global du systeme est un schema contenant tous les invariants. Le schema ANCHOR_State du modele PV Anchor contient 17 invariants (INV-01 a INV-17). Exemples :

┌─ ANCHOR_State ───────────────────────────────────────
│  batches          : BatchId ⇸ AnchorBatch
│  finalizedEvents  : ℙ EventId
│  signerAddresses  : ℙ SignerAddressStr
│  signerStatuses   : SignerAddressStr ⇸ SignerStatus
│  finalityDepth    : ℕ₁
│  auditLog         : seq AuditEntry
├───────────────────────────────────────────────────────────
│  ── INV-12 : FinalityDepthEnforced
│  ∀ bid : dom batches •
│      batches(bid).status = FINALIZED ⇒
│          batches(bid).confirmations ≥ finalityDepth
│
│  ── INV-13 : SignerRevocationValid
│  ∀ bid : dom batches •
│      batches(bid).status ∈ {SUBMITTED, PENDING_FINALITY, FINALIZED} ⇒
│          batches(bid).signerAddress ∈ dom signerStatuses
└───────────────────────────────────────────────────────────

Operations — Chaque operation du protocole est specifiee par un schema Delta (Δ) avec pre-conditions explicites :

┌─ FinalizeBatch ──────────────────────────────────────
│  ΔANCHOR_State
│  batchId? : BatchId
├───────────────────────────────────────────────────────────
│  batchId? ∈ dom batches
│  batches(batchId?).status = PENDING_FINALITY
│  batches(batchId?).merkleRoot ≠ ∅
│  batches(batchId?).txId ≠ ∅
│  batches(batchId?).blockNumber ≥ 1
│  ── ANCHOR-16 : confirmations >= finalityDepth
│  batches(batchId?).confirmations ≥ finalityDepth
└───────────────────────────────────────────────────────────

Theoremes — Des theoremes de preservation garantissent que les operations maintiennent les invariants :

── THM-09 : FinalizeBatch preserve INV-12 (finality depth enforced)
── ∀ batchId? •
──     pre(FinalizeBatch) ⇒ confirmations ≥ finalityDepth

Le modele Z PV Anchor comprend 17 invariants, 9 theoremes, et 8 operations.

Invariants Z supplementaires — Z notation permet des invariants structurels supplementaires (INV-14 a INV-17) qui n'ont pas d'equivalent direct dans TLA+ ou Alloy :

Ces invariants supplementaires sont traces dans la matrice de tracabilite du RFC (Section 7.2).

3.3.3 Comment le code source devient des predicats¶

Le script extract-facts.py genere un fichier _generated-z-lint.yaml qui mappe les entites TypeORM aux schemas Z :

norm: pv-anchor
version: 1.1.0
entities:
  anchor_batch:
    z_schemas:
    - AnchorBatch
    - AnchorEvent
    - TemporalWindow
    - MerkleTree
    - InclusionProof
    - ProofArtifact
    required_columns:
    - merkle_root
    - tx_id
    - chain_id
    - block_number
    - status
    - signer_address
    - window_start
    - window_end
    - confirmation_count
    - signer_status
enums:
  batch_status:
    z_type: BatchStatus
    values: [PENDING, BUILDING, SUBMITTED, PENDING_FINALITY, FINALIZED, FAILED]
  signer_status:
    z_type: SignerStatus
    values: [ACTIVE, REVOKED]

La section anchored: du fichier genere contient les entites et colonnes reelles extraites du code, avec les schemas Z attendus :

anchored:
  entities:
  - name: anchor_batch
    expected_in_schemas: [Fingerprint]
    columns: [block_number, chain_id, merkle_root, signer_address, status,
              submitted_at, tree_id, tx_id, window_end, window_start]

3.3.4 Comment l'inclusion est prouvee¶

Le linter Z (z-notation-lint.py) effectue les verifications suivantes :

1. Colonnes requises : pour chaque entite, required_columns(RFC) ⊆ actual_columns(code). Si une colonne requise par la specification Z est absente du code, le lint echoue.
2. Mapping schemas : chaque entite est mappee aux schemas Z attendus. Le lint verifie que les schemas references existent dans la specification.
3. Enumerations : les valeurs d'enum extraites du code sont comparees aux types Z correspondants.

Le resultat est un score de lint (ex: 23/23 checks pass).

3.3.5 Role et limites¶

Role dans le pipeline : Z sert de contrat mathematique auditable. La mecanisation actuelle est un lint structurel ; la preuve des theoremes Z est revue par un auditeur humain. Z remplit trois fonctions complementaires aux autres formalismes :

1. Specification mathematique de reference — Les schemas Z constituent la definition la plus rigoureuse des structures de donnees, des invariants et des operations. Ils servent de source de verite formelle pour les auditeurs, exprimee en theorie des ensembles et logique des predicats.
2. Lint structurel automatise — Le linter Z verifie mecaniquement que les colonnes requises, les enumerations et les schemas du code correspondent a ceux de la specification.
3. Tracabilite exigences → artefacts — Les invariants INV-14 a INV-17 (specifiques a Z) enrichissent la matrice de tracabilite avec des proprietes que TLA+ et Alloy n'expriment pas (pessimistic locking, reorg handling).

Limites :

• Pas de prouveur automatique : contrairement a TLA+ (TLC) et Alloy (SAT), Z n'a pas de prouveur automatique dans ce pipeline. La verification mecanisee est structurelle (lint), pas semantique. Les theoremes Z (THM-01 a THM-09) sont formules mais non prouves mecaniquement — ils servent de contrats formels pour review humaine ou outillee ulterieurement (ex: Z/EVES, ProofPower-Z).
• Invariants supplementaires : les invariants INV-14 a INV-17 sont specifiques a Z et ne sont pas verifies mecaniquement. Ils sont neanmoins traces et documentes dans le rapport d'audit.

3.4 Prolog — Verification de conformite directe¶

3.4.1 Nature de la verification¶

SWI-Prolog est utilise comme moteur de verification factuelle directe : les exigences du RFC sont traduites en regles Prolog (check_*/0), et les artefacts du code source sont traduits en faits Prolog (entity/3, service_method/2, etc.). L'evaluation des regles contre les faits determine si chaque exigence est satisfaite.

Prolog apporte la verification la plus concrete : il ne raisonne pas sur des abstractions mais sur les artefacts reels du code — entites de base de donnees, methodes de service, triggers SQL, ressources Terraform.

Deux niveaux de regles sont definis :

• Compliance (*_compliance.pl) : checks bloquants. Tout echec constitue une non-conformite.
• Completeness (*_completeness.pl) : checks informatifs. Les echecs sont des recommandations, pas des non-conformites.

3.4.2 Comment les exigences RFC deviennent des predicats¶

Chaque exigence du RFC se traduit en un ou plusieurs predicats check_*/0. Un predicat utilise le mecanisme de cut (!) pour produire un verdict unique et lisible : la premiere clause qui reussit est definitive, et le backtracking est coupe. La base de faits peut contenir plusieurs correspondances (ex: variantes de nommage createBatch / create), la regle selectionne la premiere strategie valide et emet un seul [OK] ou [KO].

Check structurel (l'artefact existe) :

%% CHECK 28 : Colonne confirmation_count (ANCHOR-16)
check_confirmation_count_col :-
    entity_column(anchor_batch, confirmation_count, _), !,
    format("  [OK] final : colonne anchor_batch.confirmation_count (ANCHOR-16)~n"),
    record_ok.
check_confirmation_count_col :-
    entity_column(anchor_batch, confirmations, _), !,
    format("  [OK] final : colonne anchor_batch.confirmations (ANCHOR-16)~n"),
    record_ok.
check_confirmation_count_col :-
    format("  [KO] final : colonne confirmation_count/confirmations ABSENTE (ANCHOR-16)~n"),
    record_ko.

Check semantique (l'artefact est correctement utilise) :

%% CHECK 29 : Garde confirmations dans finalizeBatch (ANCHOR-16 — semantique)
check_finalize_confirmations_guard :-
    service_method_guard(anchor_batch, finalizeBatch, confirmation_count), !,
    format("  [OK] final : finalizeBatch() verifie confirmation_count (ANCHOR-16)~n"),
    record_ok.
check_finalize_confirmations_guard :-
    format("  [KO] final : finalizeBatch() SANS garde confirmation_count (ANCHOR-16)~n"),
    record_ko.

Tolerance aux variations de nommage : les checks acceptent des variantes courantes (ex: createBatch ou create, finalizeBatch ou finalize, anchor_batch ou anchor_batches). Cette tolerance evite les faux negatifs dus aux conventions de nommage.

Le modele PV Anchor comprend 32 checks de compliance (dont ANCHOR-16 finality depth et ANCHOR-17 signer revocation, ajoutes avec PD-276) et 4 checks de completeness.

3.4.3 Comment le code source devient des predicats¶

Le script extract-facts.py genere un fichier _generated-facts.pl contenant l'ensemble des faits extraits du code source. Les predicats generes sont :

Le predicat service_method_guard/3 est le plus critique pour la verification semantique. Il est extrait par analyse statique du code des methodes de service : si la methode finalizeBatch contient une condition sur confirmation_count (comparaison, assertion, ou validation), le fait service_method_guard(anchor_batch, finalizeBatch, confirmation_count) est genere.

3.4.4 Verification a deux niveaux¶

Le pattern de verification a deux niveaux est illustre par ANCHOR-16 (finality depth) :

Niveau 1 — Structurel : la colonne confirmation_count existe dans l'entite anchor_batch.

entity_column(anchor_batch, confirmation_count, 'integer').
→ check_confirmation_count_col : [OK]

Niveau 2 — Semantique : la methode finalizeBatch() contient une garde sur confirmation_count.

service_method_guard(anchor_batch, finalizeBatch, confirmation_count).
→ check_finalize_confirmations_guard : [OK]

Sans le niveau 2, un systeme pourrait declarer la colonne sans jamais la verifier. Le service_method_guard/3 ferme cette faille.

Le meme pattern s'applique a ANCHOR-17 (signer revocation) :

3.4.5 Comment l'inclusion est prouvee¶

Le predicat run_audit/0 orchestre l'execution sequentielle de tous les checks :

run_audit :-
    reset_counters,
    %% ... invocation de chaque check_*/0 ...
    count_results(OK, KO),
    Total is OK + KO,
    format("  Resultat : ~d/~d OK", [OK, Total]).

Pour chaque check :

1. SWI-Prolog tente de resoudre le predicat contre la base de faits chargee.
2. Si un fait correspondant est trouve → [OK], le compteur check_ok est incremente.
3. Si aucun fait ne correspond → [KO], le compteur check_ko est incremente.

Le verdict final est CONFORME si KO = 0, sinon les echecs sont listes.

Execution :

# Avec les faits generes automatiquement (production)
swipl -l _generated-facts.pl -l pv_anchor_compliance.pl -g "run_audit." -t "halt."

# Avec les faits statiques (test local)
swipl -l test_data.pl -l pv_anchor_compliance.pl -g "run_audit." -t "halt."

3.4.6 Fallback statique¶

Le fichier test_data.pl fournit un ensemble de faits statiques equivalents aux faits generes. Il permet :

• L'execution des checks en local sans le pipeline complet.
• La validation des regles de compliance independamment de l'etat du code.

Le script verify-norm.sh utilise _generated-facts.pl en priorite. Si ce fichier n'existe pas, il se rabat sur test_data.pl.

3.4.7 Limites¶

• Analyse statique : l'extraction parse les decorateurs et noms de methodes, pas le comportement a l'execution. Un decorateur @Column() incorrectement configure pourrait etre extrait sans erreur.
• Extraction AST ts-morph (depuis v1.3.0) : l'extracteur principal utilise le parsing AST TypeScript (extract-ts-facts.ts). Les anciens extracteurs regex sont conserves comme fallback automatique si ts-morph echoue (Node.js absent, timeout). Les extracteurs non-TypeScript (SQL, Terraform, tests, docs) restent en regex. Cf. Section 9.5.3 pour les metriques de migration.
• Granularite semantique des gardes : le predicat service_method_guard/3 detecte la presence d'une garde, mais pas la semantique. Le predicat enrichi service_method_guard_cmp/5 (operateur + constante comparee) est desormais implemente (cf. Section 9.5.1) et les checks Prolog tentent d'abord /5 puis fallback sur /3. L'extracteur extract-guards.ts (ts-morph) detecte les gardes directes et les gardes indirectes cross-composant via guard_mappings dans norm.yaml.
• Tolerance aux variantes : la tolerance de nommage (createBatch / create) peut produire des faux positifs si un service expose une methode create non liee au batch.

4. Pipeline d'extraction¶

4.1 Architecture de extract-facts.py¶

Le script extract-facts.py est le composant central du pipeline d'extraction. Il analyse le code source reel de ProbatioVault et genere les fichiers de faits dans les 4 formats formels. Le principe architectural est un AST, N sorties : un seul pass d'extraction alimente tous les formalismes.

4.1.1 Extracteur principal — ts-morph AST (depuis v1.3.0)¶

Le script extract-ts-facts.ts (~730 lignes) effectue un chargement unique du Project ts-morph (~3-5s) puis extrait 6 categories de faits en un seul pass AST :

La classe TsMorphExtractor dans extract-facts.py appelle extract-ts-facts.ts en subprocess. Si ts-morph echoue (Node.js absent, timeout), le fallback automatique vers les extracteurs regex se declenche (cf. Section 9.5.3).

4.1.2 Extracteurs complementaires (regex — sources non-TypeScript)¶

4.1.3 Generateurs de sortie¶

Les faits intermediaires unifies alimentent 4 generateurs de sortie, un par formalisme :

4.2 Sources de donnees¶

Le script accepte deux sources principales :

python3 extract-facts.py \
    --backend /path/to/ProbatioVault-backend/src \
    --infra /path/to/ProbatioVault-infra/terraform \
    --output-nf /path/to/normes/nf-z42-013/formal/_generated-facts.pl \
    --output-anchor /path/to/normes/pv-anchor/formal/_generated-facts.pl

• --backend : code source TypeScript (entites TypeORM, services NestJS, migrations, guards).
• --infra : code Terraform HCL (buckets S3, clusters CloudHSM, regles CRR).

4.3 Quatre sorties par norme¶

Pour chaque norme, le script genere :

Chaque fichier genere porte le commentaire :

DO NOT EDIT — regenerated at each CI build

4.4 Faits derives¶

Le DerivedFactsGenerator calcule des faits secondaires a partir des faits bruts. Exemple : si un bucket S3 a l'Object Lock en mode COMPLIANCE et une regle CRR active, le fait derive geo_copy_count(bucket, 2) est genere, indiquant que les donnees sont repliquees geographiquement.

4.5 Invariants du pipeline¶

Le pipeline d'extraction respecte trois invariants :

1. Determinisme : pour une meme base de code en entree, la sortie est toujours identique. Pas de dependance a l'horloge, a l'ordre de parcours du systeme de fichiers, ou a un etat externe.
2. Pas de curation manuelle : les fichiers generes ne sont jamais edites manuellement. Toute modification du code source est automatiquement refletee dans les faits generes au prochain build CI.
3. Regeneration systematique : le pipeline est execute a chaque build CI. Les fichiers generes sont des artefacts derives, pas des sources.

5. Pipeline de verification¶

5.1 Architecture de verify-norm.sh¶

Le script verify-norm.sh orchestre 6 etapes de verification sequentielles :

L'ordre est significatif : TLC (etape 1) verifie le design avant Prolog (etape 2) qui verifie l'implementation. Alloy (etape 3) et Z (etape 4) apportent des perspectives complementaires.

5.2 Manifest norm.yaml¶

Chaque norme possede un fichier norm.yaml qui declare ses fichiers formels :

name: "PV Blockchain Anchoring Protocol"
slug: pv-anchor
tla:
  spec: PV_Anchor.tla
  config: PV_Anchor.cfg
  anchored_facts: _AnchoredFacts_ANCHOR.tla
  state_set_name: StatusValues
  state_mapping:
    PENDING: PENDING
    BUILDING: BUILDING
    SUBMITTED: SUBMITTED
    PENDING_FINALITY: PENDING_FINALITY
    FINALIZED: FINALIZED
    FAILED: FAILED
prolog:
  rules: pv_anchor_compliance.pl
  completeness: pv_anchor_completeness.pl
  facts: _generated-facts.pl
  test_data: test_data.pl
alloy:
  model: PV_Anchor.als
z:
  spec: PV_Anchor.zed
  lint_config: _generated-z-lint.yaml
  lint_config_static: z-lint.yaml

Le champ state_mapping est critique : il mappe les valeurs d'enum du code aux etats du modele TLA+. Si le code utilise PENDING_FINALITY mais le modele attend WAITING_CONFIRMATION, le mapping detecte l'incoherence.

5.3 Integration CI/CD GitLab¶

Le pipeline CI/CD GitLab execute la verification formelle automatiquement :

extract-facts ──► verify:pv-anchor ──► compile-verdicts
                  verify:pv-envelope
                  verify:pv-audit
                  verify:pv-proof
                  verify:pv-pre
                  verify:nf-z42-013
                  verify:iso-14641
                  verify:rfc-3161
                  verify:rfc-5054

1. Job extract-facts : clone les repos backend et infra, execute extract-facts.py, genere les fichiers de faits pour toutes les normes.
2. Jobs verify:{slug} : un job par norme, execute verify-norm.sh. Les jobs s'executent en parallele. Chaque job produit un artefact JUnit XML pour le reporting GitLab.
3. Job compile-verdicts : agregation des baselines et overlays en verdicts Prolog compilees.

Les jobs sont declenches sur modification des fichiers docs/normes/*/formal/* ou scripts/formal/*.

5.4 Interpretation des resultats¶

Chaque formalisme a ses criteres d'echec :

5.5 Codes de sortie¶

Le script verify-norm.sh distingue les echecs de verification (violations formelles detectees) des erreurs d'outil (crash, timeout, fichier manquant) :

Les etapes non-bloquantes (completeness, compliance scoring) ne modifient pas le code de sortie. Les outils manquants (java, swipl) generent un [SKIP], pas un [ERROR] — seuls les crashs d'outils presents declenchent le code 2.

6. Mecanisme d'ancrage¶

Le mecanisme d'ancrage est le differenciateur fondamental de la verification formelle ProbatioVault par rapport aux approches traditionnelles. Il garantit que les modeles formels ne sont pas des abstractions deconnectees du code reel.

6.1 Principe¶

Dans la verification formelle traditionnelle, un modele est ecrit manuellement et peut diverger silencieusement du code au fil des evolutions. ProbatioVault elimine ce risque en generant automatiquement des fichiers d'ancrage qui lient les constantes et structures du modele aux artefacts reels du code.

Si le code evolue et qu'un artefact requis par le modele disparait ou change, la verification echoue immediatement.

6.2 Ancrage TLA+¶

Le module _AnchoredFacts_{MODULE}.tla utilise le mecanisme EXTENDS de TLA+ pour heriter du modele principal et ajouter des contraintes ASSUME :

---- MODULE _AnchoredFacts_ANCHOR ----
EXTENDS PV_Anchor

RealStates == {"PENDING", "BUILDING", "SUBMITTED",
               "PENDING_FINALITY", "FINALIZED", "FAILED"}

ASSUME AnchorAssume_States ==
    /\ RealStates \subseteq StatusValues
    /\ StatusValues \subseteq RealStates  \* egalite stricte

RealSignerStatuses == {"ACTIVE", "REVOKED"}

ASSUME AnchorAssume_SignerStatuses ==
    /\ RealSignerStatuses \subseteq SignerStatusValues
    /\ SignerStatusValues \subseteq RealSignerStatuses

RealHasHSM == TRUE
RealHasWORM == TRUE
RealHasCRR == TRUE
RealHasJournalTrigger == TRUE
RealHasTruncateRevoked == TRUE

ASSUME AnchorAssume_Infrastructure ==
    /\ RealHasHSM /\ RealHasWORM /\ RealHasCRR
    /\ RealHasJournalTrigger /\ RealHasTruncateRevoked

RealHasConfirmationCount == TRUE

ASSUME AnchorAssume_FinalitySupport ==
    RealHasConfirmationCount

====

Controle de compatibilite stricte pour les types : le pipeline genere RealStates directement depuis les enums du code. L'ASSUME RealStates ⊆ StatusValues echoue si le code declare un etat que le modele ne connait pas (ex: ARCHIVED). Un second ASSUME StatusValues ⊆ RealStates echoue si un etat du modele n'est pas implemente dans le code. Les deux inclusions combinees imposent l'egalite RealStates = StatusValues.

6.3 Ancrage Alloy¶

Le module _AnchoredFacts_{MODULE}.als utilise des singletons one sig :

module _AnchoredFacts_ANCHOR
open PV_Anchor

one sig Real_anchor_batch_tx_id {}
one sig Real_anchor_batch_merkle_root {}
one sig Real_anchor_batch_confirmation_count {}
one sig Real_anchor_batch_signer_status {}
one sig Real_WORM_bucket {}
one sig Real_HSM_FIPS {}
one sig Real_journal_trigger {}

fact AnchoredTSAAndAnchoring {
    some Real_anchor_batch_tx_id
    some Real_anchor_batch_merkle_root
    some Real_anchor_batch_confirmation_count
    some Real_anchor_batch_signer_status
}

assert AnchoredArtifactsConsistent {
    some Real_anchor_batch_tx_id and
    some Real_anchor_batch_merkle_root and
    some Real_anchor_batch_confirmation_count and
    some Real_anchor_batch_signer_status and
    some Real_WORM_bucket and
    some Real_HSM_FIPS and
    some Real_journal_trigger
}
check AnchoredArtifactsConsistent for 4

Les one sig ont un cout de scope nul : ils representent un atome unique qui existe toujours, sans augmenter le nombre de configurations a explorer.

6.4 Ancrage Z¶

Le fichier _generated-z-lint.yaml contient une section anchored: qui mappe les entites reelles aux schemas Z attendus :

anchored:
  entities:
  - name: anchor_batch
    expected_in_schemas: [Fingerprint]
    columns:
    - block_number
    - chain_id
    - merkle_root
    - signer_address
    - status
    - tx_id
    - window_end
    - window_start

Le linter Z verifie que les required_columns du modele sont un sous-ensemble des columns reelles.

6.5 Ancrage Prolog¶

Le fichier _generated-facts.pl est l'ancrage le plus direct : chaque fait represente un artefact reel du code. L'absence d'un fait entraine directement l'echec du check correspondant.

Exemple : si l'entite anchor_batch est supprimee du code, le fait entity(anchor_batch, _, _) disparait du fichier genere, et le CHECK 1 echoue immediatement.

6.6 Cycle de vie¶

Code modifie ──► git push ──► CI/CD Pipeline
                                    │
                              extract-facts.py
                                    │
                          extract-ts-facts.ts
                          (ts-morph AST — 1 seul pass, ~3-5s)
                                    │
                        Faits intermediaires unifies
                        (entity/3, service_method/2,
                         guard_cmp/5, cron_job/3, ...)
                                    │
                    ┌───────┬───────┼───────┬───────┐
                    ▼       ▼       ▼       ▼       ▼
                  .pl     .tla    .als   .yaml   (futur)
                Prolog   TLA+   Alloy  Z-lint  .thy/.spthy
                (=100%)  (~20%) (~20%) (struct) Isabelle/
                                                Tamarin
                    │       │       │       │
                    └───────┴───┬───┴───────┘
                                ▼
                          verify-norm.sh
                                │
                                ▼
                        AUDIT-REPORT.md
                        (verdict mis a jour)

Profondeur d'exploitation de l'AST par formalisme :

Ce cycle garantit que toute modification du code est immediatement refletee dans les modeles formels et verifiee.

7. Piste d'audit¶

7.1 Generation de AUDIT-REPORT.md¶

Le rapport d'audit est genere automatiquement par le script generate-audit-report.py v2. Il consolide les resultats des 4 systemes formels en un document unique, trace et datable.

7.2 Structure du rapport¶

Chaque AUDIT-REPORT.md suit une structure normalisee :

7.3 Verdicts¶

Trois verdicts sont possibles :

7.4 Score de conformite dynamique¶

Le score de conformite est calcule par le module compliance_scoring.pl :

Score = (conforme × 100 + partiel × 50) / applicable

Le score evolue dans le temps grace au systeme de baselines et overlays :

• Baseline (baseline.yaml) : verdicts initiaux issus d'un audit multi-agents (ex: PD-244).
• Overlays (overlays/) : verdicts mis a jour suite a des stories completees (Gate 8 GO/RESERVE).
• Compilation : compile-verdicts.py fusionne baselines + overlays en _compiled-verdicts.pl, un fichier Prolog chargeable directement.

8. Tracabilite¶

8.1 Matrice de tracabilite¶

Le fichier _traceability-matrix.yaml fournit une matrice de couverture globale. Chaque article normatif est mappe a :

• Article : reference normative (ex: art_5_6_fingerprint)
• Description : texte de l'exigence
• Prolog Rule : predicat de verification (ex: check_5_6_fingerprint)
• Status : COVERED, PARTIEL, GAP, HORS_PERIMETRE
• Artifacts : fichiers source et cles d'implementation

Exemple :

pv_anchor:
  anchor_16_finality:
    article: '3.16'
    description: 'Politique de finalite configurable (FINALITY_DEPTH)'
    prolog_rule: 'check_confirmation_count_col, check_finalize_confirmations_guard'
    status: COVERED
    artifacts:
      - path: 'src/modules/tsa/entities/anchor-batch.entity.ts'
        key: 'column:anchor_batch:confirmation_count'
      - path: 'src/modules/tsa/services/anchor-batch.service.ts'
        key: 'method:anchor_batch:finalizeBatch:guard:confirmation_count'

8.2 Tracabilite croisee¶

Chaque exigence RFC est tracee a travers les 4 formalismes. La matrice de tracabilite du RFC (Section 7.2 du RFC) formalise ce mapping :

8.3 Manifest norm.yaml¶

Le fichier norm.yaml constitue le point d'entree technique de la tracabilite. Il lie :

• Les fichiers de modeles formels (TLA+, Alloy, Z) aux specifications RFC.
• Les fichiers d'ancrage aux faits generes.
• Les fichiers Prolog aux regles de compliance.
• Le mapping d'etats entre le code et les modeles.

9. Limites et perimetre¶

9.1 Limites inherentes aux methodes formelles¶

9.2 Elements non verifies¶

• Performance et scalabilite du systeme.
• Correction des primitives cryptographiques (OpenSSL, CloudHSM, node:crypto).
• Securite reseau (TLS, pare-feu, routage).
• Interface utilisateur et experience utilisateur.
• Correction des dependances tierces (npm, drivers PostgreSQL).
• Sur-implementation (SOURCE ⊆ RFC).

9.3 Risques residuels¶

1. Gap d'abstraction : les modeles operent sur des valeurs abstraites (entiers pour les hashes, ensembles finis pour les identifiants). Un defaut specifique a une valeur reelle (ex: collision de hash) ne serait pas detecte.
2. Espace d'etats non totalement explore : les constantes bornent l'exploration. Un defaut qui ne se manifeste qu'avec 3+ batches simultanees ne serait pas detecte avec MAX_BATCHES=1.
3. Faux positifs de tolerance : la tolerance aux variantes de nommage (createBatch / create) pourrait accepter une methode sans rapport avec le batch.
4. Modele sequentiel : TLA+ modelise la concurrence par entrelacement non-deterministe, pas par parallelisme reel. Les conditions de course specifiques au threading ne sont pas couvertes.

9.4 Mesures d'attenuation¶

1. Defense en profondeur : les 4 formalismes couvrent mutuellement leurs angles morts. Un defaut qui echappe a TLA+ sera probablement detecte par Prolog ou Alloy.
2. Extraction automatique : l'absence de curation manuelle elimine les risques de drift modele/code.
3. Integration CI/CD : la verification est executee a chaque commit, detectant les regressions immediatement.
4. Verification a deux niveaux : le pattern service_method_guard/3 ajoute une couche semantique au-dela de la simple presence structurelle.
5. Audits periodiques : les rapports AUDIT-REPORT.md sont regeneres et revises regulierement.

9.5 Feuille de route d'amelioration¶

Les limites identifiees ci-dessus font l'objet d'un plan d'amelioration progressif. Chaque amelioration est classee par priorite et impact.

9.5.1 Enrichissement semantique des gardes Prolog — FAIT¶

Statut : implemente (v1.2.0, 2026-02-28).

Realisation :

• Nouveau predicat service_method_guard_cmp/5 (Service, Method, Field, Operator, ComparedValue).
• Extracteur extract-guards.ts (ts-morph) scanne *.service.ts, *.processor.ts, *.tracker.ts et detecte 4 patterns : comparaisons directes, status transitions, throw-on-missing, append-only checks.
• Gardes indirectes cross-composant declarees dans norm.yaml (guard_mappings) et verifiees contre l'AST.
• Checks Prolog 29 et 32 unifies avec fallback /5 → /3 (retrocompatible).
• Integration dans extract-facts.py via TsMorphGuardExtractor.

Resultats : 14 faits extraits automatiquement (6 /3 + 8 /5), dont 2 via guard_mappings (ANCHOR-16, ANCHOR-17). 32/32 checks OK.

9.5.2 Tests negatifs en CI — FAIT¶

Statut : implemente (v1.2.0, 2026-02-28).

Realisation :

• 6 scenarios negatifs dans test_negative_data/ (pv-anchor), chacun retirant un fait critique.
• Script verify-negative-tests.sh : pour chaque neg_*.pl, execute l'audit Prolog et verifie que le [KO] attendu apparait.
• Header machine-parseable %% EXPECTED_KO: dans chaque fichier negatif.
• Job CI test:negative-verification:pv-anchor dans .gitlab-ci.yml.

Scenarios couverts :

Resultats : 6/6 PASS — chaque non-conformite est correctement detectee.

9.5.3 Extraction AST TypeScript (Priorite : moyenne) — FAIT¶

Statut : implemente (v1.3.0). Le script extract-ts-facts.ts consolide l'extraction de TOUS les faits TypeScript via ts-morph AST. Les anciens extracteurs regex (EntityExtractor, ServiceExtractor, GuardExtractor, SchedulerExtractor) sont conserves comme fallback automatique dans extract-facts.py.

Script : scripts/formal/extract-ts-facts.ts (~730 lignes)

Architecture realisee : chargement unique du Project ts-morph (~3-5s), puis extraction en un seul pass AST de 6 categories de faits (9 predicats Prolog distincts).

Resultats de la migration (mesures reelles, backend ProbatioVault) :

Integration dans extract-facts.py : la classe TsMorphExtractor appelle extract-ts-facts.ts en subprocess. Si ts-morph echoue (Node.js absent, timeout), le fallback automatique vers les extracteurs regex se declenche. Les deux extracteurs doivent produire des sorties equivalentes — le taux de recouvrement mesure (96%, 1523 faits communs) sert de test de non-regression. Les anciens extracteurs regex sont conserves dans le code source pour permettre la comparaison a tout moment.

Metriques courantes (mesures reelles, 2026-03-01) :

Evolution : +551 faits depuis la migration v1.3.0 (1724 → 2275, +32%), principalement due a l'ajout d'entites (audit_event, clock_attestation, etc.), de gardes semantiques (service_method_guard_cmp/5) et d'index supplementaires.

Extracteurs restes en regex (non-TypeScript ou textuel) : - MigrationExtractor : patterns SQL dans les fichiers de migration - TerraformExtractor : patterns HCL dans les fichiers .tf - TestExtractor : pattern INV-\d+-\d+ dans les fichiers .spec.ts - DocumentExtractor : patterns de noms de fichiers dans docs/

9.5.4 Propriete de vivacite bornee TLA+ (Priorite : moyenne)¶

Probleme : le modele TLA+ verifie uniquement des proprietes de surete (safety). Aucune propriete de vivacite (liveness) n'est verifiee — par exemple, « un batch SUBMITTED finit par etre FINALIZED ou FAILED ».

Evolution cible : ajouter au moins une propriete de vivacite bornee (weak fairness) au modele TLA+ :

\* Liveness : chaque batch SUBMITTED atteint eventuellement FINALIZED ou FAILED
EventualFinality == \A id \in batches :
    batch_status[id] = "SUBMITTED" ~> batch_status[id] \in {"FINALIZED", "FAILED"}

Prerequis : activation de la weak fairness dans la specification (WF_vars(Next)) et augmentation de MAX_ITERATIONS pour permettre l'exploration des traces de vivacite.

Impact : verifie l'absence de deadlocks dans le protocole d'ancrage (dans le scope explore).

9.5.5 Constantes normatives unifiees (Priorite : basse)¶

Probleme : la constante FINALITY_DEPTH apparait dans 4 fichiers (.tla, .als, .zed, .pl) avec des valeurs potentiellement differentes. Toute modification manuelle risque une incoherence.

Evolution cible : definir les constantes normatives dans norm.yaml et les injecter automatiquement dans les 4 modeles via extract-facts.py :

# norm.yaml
constants:
  FINALITY_DEPTH: 6
  FINALITY_TIMEOUT: 300

Le pipeline genererait alors les fichiers d'ancrage avec les constantes normatives comme source de verite unique.

9.5.6 Vocabulaire de bornage explicite (Priorite : basse)¶

Probleme : les rapports d'audit utilisent des termes comme « preuve » ou « garanti » pour des resultats qui sont strictement bornes (scope fini).

Evolution cible : standardiser le vocabulaire dans les rapports generes :

Cette normalisation sera integree dans le template de generate-audit-report.py.

10. Annexe A — Demonstration complete ANCHOR-16¶

Cette annexe demontre le parcours complet d'une seule exigence normative — ANCHOR-16 : Politique de finalite configurable — a travers les 4 formalismes, depuis le RFC jusqu'a la verification du code source.

10.1 Exigence normative (RFC)¶

ANCHOR-16 : Chaque chaine cible definit un seuil de finalite (FINALITY_DEPTH) representant le nombre minimum de confirmations blockchain requises. FinalizeBatch exige que le nombre de confirmations du bloc contenant la transaction soit superieur ou egal a FINALITY_DEPTH.

Source : RFC PV-ANCHOR-001, Section 3.16.

10.2 TLA+ — Modelisation temporelle¶

Constante :

CONSTANTS
    FINALITY_DEPTH      \* Nombre minimum de confirmations pour finality

Variable :

VARIABLES
    batch_confirmations    \* [batchId -> nombre de confirmations]

Precondition de FinalizeBatch :

FinalizeBatch(id) ==
    /\ id \in batches
    /\ batch_status[id] = "PENDING_FINALITY"
    /\ batch_confirmations[id] >= FINALITY_DEPTH
    /\ batch_status' = [batch_status EXCEPT ![id] = "FINALIZED"]
    /\ ...

Invariant INV-12 :

FinalityDepthEnforced ==
    \A id \in batches :
        batch_status[id] = "FINALIZED"
        => batch_confirmations[id] >= FINALITY_DEPTH

Theoreme :

THEOREM Spec => []FinalityDepthEnforced

TLC verifie que cet invariant est satisfait dans tous les etats atteignables. Avec FINALITY_DEPTH = 1 et ConfirmValues == 0..10, TLC explore toutes les combinaisons possibles et ne trouve aucune violation.

10.3 TLA+ — Ancrage code¶

\* _AnchoredFacts_ANCHOR.tla
RealHasConfirmationCount == TRUE  \* entity_column(anchor_batch, confirmation_count, *)

ASSUME AnchorAssume_FinalitySupport ==
    RealHasConfirmationCount

Ce fait est genere car extract-facts.py a detecte la colonne confirmation_count dans l'entite TypeORM anchor_batch. Si la colonne est supprimee du code, RealHasConfirmationCount passerait a FALSE et l'ASSUME echouerait.

10.4 Alloy — Analyse structurelle¶

Fait :

fact FinalityDepthEnforced {
    all b : AnchorBatch |
        b.status = Finalized implies
            (one b.confirmations and b.confirmations >= 1)
}

Assertion :

assert FinalityDepthCheck {
    all b : AnchorBatch |
        b.status = Finalized implies
            (one b.confirmations and b.confirmations >= 1)
}
check FinalityDepthCheck for 5

Le solveur SAT cherche un AnchorBatch avec status = Finalized et confirmations < 1 dans toutes les configurations possibles contenant jusqu'a 5 atomes par type. Aucun contre-exemple n'est trouve dans ce scope — l'assertion est satisfaite.

10.5 Alloy — Ancrage code¶

\* _AnchoredFacts_ANCHOR.als
one sig Real_anchor_batch_confirmation_count {}
\* entity_column(anchor_batch, confirmation_count, *)

Ce singleton est present dans fact AnchoredTSAAndAnchoring et assert AnchoredArtifactsConsistent, garantissant que la colonne existe dans le code reel.

10.6 Z — Specification mathematique¶

Invariant INV-12 dans ANCHOR_State :

│  ── INV-12 : FinalityDepthEnforced
│  ∀ bid : dom batches •
│      batches(bid).status = FINALIZED ⇒
│          batches(bid).confirmations ≥ finalityDepth

Precondition de FinalizeBatch :

┌─ FinalizeBatch ──────────────────────────────────────
│  ΔANCHOR_State
│  batchId? : BatchId
├───────────────────────────────────────────────────────────
│  batches(batchId?).status = PENDING_FINALITY
│  ── ANCHOR-16 : confirmations >= finalityDepth
│  batches(batchId?).confirmations ≥ finalityDepth
└───────────────────────────────────────────────────────────

Theoreme THM-09 :

── THM-09 : FinalizeBatch preserve INV-12 (finality depth enforced)
── ∀ batchId? •
──     pre(FinalizeBatch) ⇒ confirmations ≥ finalityDepth

10.7 Z — Ancrage code¶

# _generated-z-lint.yaml
entities:
  anchor_batch:
    required_columns:
    - confirmation_count

Le linter Z verifie que confirmation_count est presente dans les colonnes reelles extraites du code.

10.8 Prolog — Verification structurelle¶

%% CHECK 28 : Colonne confirmation_count (ANCHOR-16)
check_confirmation_count_col :-
    entity_column(anchor_batch, confirmation_count, _), !,
    format("  [OK] final : colonne anchor_batch.confirmation_count (ANCHOR-16)~n"),
    record_ok.

Fait genere :

entity_column(anchor_batch, confirmation_count, 'integer').

Resolution : le fait entity_column(anchor_batch, confirmation_count, 'integer') unifie avec la regle → [OK].

10.9 Prolog — Verification semantique¶

%% CHECK 29 : Garde confirmations dans finalizeBatch (ANCHOR-16 — semantique)
check_finalize_confirmations_guard :-
    service_method_guard(anchor_batch, finalizeBatch, confirmation_count), !,
    format("  [OK] final : finalizeBatch() verifie confirmation_count (ANCHOR-16)~n"),
    record_ok.

Fait genere :

service_method_guard(anchor_batch, finalizeBatch, confirmation_count).

Ce fait est genere par extract-facts.py car l'analyse statique de la methode finalizeBatch() dans AnchorBatchService a detecte une verification sur confirmation_count (condition if, assertion, ou validation).

10.10 Synthese¶

Conclusion : l'exigence ANCHOR-16 est formellement verifiee par les 4 systemes, tant au niveau du design (TLA+, Alloy, Z) qu'au niveau de l'implementation (Prolog structurel + semantique), avec un ancrage automatique au code source reel.

11. Annexe B — Arborescence des fichiers¶

Structure type d'une norme (exemple : pv-anchor) :

normes/pv-anchor/
│
├── RFC-PV-ANCHOR.md                           # Source normative (verite)
│
└── formal/
    │
    ├── norm.yaml                              # Manifest (mapping fichiers ↔ formalismes)
    │
    │── PV_Anchor.tla                          # Modele TLA+ (13 invariants, 11 actions)
    │── PV_Anchor.cfg                          # Config TLC (constantes, invariants)
    │── _AnchoredFacts_ANCHOR.tla              # Code → TLA+ (ASSUME genere)
    │
    │── PV_Anchor.als                          # Modele Alloy (12 facts, 12 assertions)
    │── _AnchoredFacts_ANCHOR.als              # Code → Alloy (one-sig genere)
    │
    │── PV_Anchor.zed                          # Specification Z (17 invariants, 9 theoremes)
    │── z-lint.yaml                            # Config Z lint statique (source de verite)
    │── _generated-z-lint.yaml                 # Code → Z (colonnes/enums generes)
    │
    │── pv_anchor_compliance.pl                # RFC → Prolog (32 checks bloquants)
    │── pv_anchor_completeness.pl              # Recommandations (4 checks informatifs)
    │── test_data.pl                           # Fallback statique (tests locaux)
    │── _generated-facts.pl                    # Code → Prolog (faits generes)
    │
    │── AUDIT-REPORT.md                        # Rapport d'audit genere
    │
    └── compliance/
        ├── _compiled-verdicts.pl              # Verdicts compiles (baselines + overlays)
        ├── baseline.yaml                      # Verdicts initiaux
        └── overlays/                          # Verdicts mis a jour par story

Convention de nommage :

12. Annexe C — Glossaire¶