Aller au contenu

PD-297 — REX

Résumé

Boucle d'enrichissement formel implémentée : 3 scripts (enrich-ontology, extract-formal-invariants, formal-non-regression). L'ontologie Prolog est désormais enrichie à chaque story DONE. Testé sur PD-296 (18 invariants extraits).

Métriques

  • G3 RESERVE 7.25 v1, G5 RESERVE 8.5 v1, G8 RESERVE 8.75 v1
  • 3 scripts créés, ontologie/{domain}/ structure créée
  • Crash Ringbearer initial détecté et repris manuellement

Learnings

  1. Le Ringbearer PD-297 a crashé entre le besoin et la spec (timeout claude -p sur un prompt de 63KB). Reprendre manuellement = 15 min vs relancer un Ringbearer = 30+ min. Le protocole de reprise est efficace.
  2. formal-verify.py reste un stub (retourne SKIP) — la vérification complète TLA+/Alloy model checking reste manuelle. C'est une dette technique connue et acceptée.
  3. L'extraction d'invariants depuis markdown est fragile (regex sur INV-XXX-NN). Les specs qui n'utilisent pas ce format (PD-295 minimaliste) ne produisent pas de prédicats. Amélioration future : extraction plus souple.

Prochaines étapes

  • Intégrer l'appel à enrich-ontology.py dans gov-compounder Phase 7
  • Implémenter formal-verify.py (TLA+ model checking automatique)
  • Étendre l'extraction à d'autres formats d'invariants (CA-, D-, ERR-)