Validation — fleet multi-agent, formalisation TLA+, gates falsifiables
Validation : la machine qui produit le code
L'observable principal n'est pas le binaire
Comme posé en § 01 : l'observable que Radience évalue n'est pas le binaire OptiX 9 fonctionnel — c'est le signal de fiabilité opérationnelle de l'orchestration agentique. Cette section décrit la machine qui a produit le code, et pourquoi sa dynamique est elle-même un livrable auditable.
Le port a été produit par une fleet, pas un agent — et la fleet a appris d'elle-même
Le portage n'est pas le travail d'un agent unique. C'est le travail d'une fleet composée — plusieurs sous-fleets atomiques, chacune avec ses rôles, ses gates, et sa dynamique collaborative.
Pour la dernière itération — le passage « on doit vraiment utiliser les GPUs du Mac » — la fleet a été conçue par une délibération à 10 personas (carnot bornes-théoriques, galileo mesure, forgemaster réutilisation/FFI, torvalds taste, knuth correctness, von-neumann formalisation, turing oracle, feynman premise-audit, janis anti-groupthink, adversary red-team). Chaque persona a grep-vérifié indépendamment la prémisse opérateur (« le backend MLX existe ») et est rentré avec la même conclusion : zéro appel sys:: dans le code, mlx = [] feature vide, descripteur sysctl-fabriqué — la prémisse est une panne silencieuse shippée. La fleet a promu son propre angle mort en finding load-bearing.
Le critère de la délibération : si le panel ne peut pas nommer le test concret qui ferait échouer la dynamique collaborative, la délibération échoue. Ce critère a été passé : la fleet a livré une décomposition en 5 unit of works-filles (gate-0 spike, anti-fabrication substrate, oracle indépendant, fleet.toml.v5, GpuFleet.tla), chacune avec un briefing falsifiable et un blocked-by typé.
Formalisation TLA+ — GpuFleet.tla (et le piège de CppFleet.tla:22-30)
La dynamique collaborative de la fleet est formalisée en TLA+ et vérifiée par model-checking. La spec courante GpuFleet.tla étend MlxFleet.tla (squelette pure-parallèle), pas CppFleet.tla (séquence-gardée) — par décision von-neumann §1 : une séquence manufacture l'ancre déjà-porté ; l'authoring parallèle rend le peeking structurellement indisponible.
Six invariants centraux, chacun adressant un mode d'échec concret :
| Invariant | Garantie | Mode d'échec qu'il bloque |
|---|---|---|
I_GpuReadSetDisjoint (symétrique, re-dérivé) | A ⊀ B et B ⊀ A, mutation-witnessed | Contamination read-set entre monomères — l'un copierait l'autre sous couvert d'indépendance. L'asymétrie naïve (CppFleet:22-30) PASSerait vide par héritage ; la re-dérivation force l'inspection effective. |
I_GpuExecutionWitnessed | Pas de signature sans ExecutionWitness::Gpu{source, timestamps} ; mintable seulement depuis un compteur driver | Silent-CPU fallback + descripteur menteur. Rend l'affirmation GPU sans preuve impossible au niveau du type — pas seulement au niveau de la revue. |
I_NoSignWithoutTripleOracle | \(\geq\) 3 témoins indépendants requis, dont f_tot.jpg (veto) | Signature sur un seul leg, ou sur deux legs co-dépendants. |
I_CascadeBounded | Boucles de rejet bornées par nlooplim=1000, cascade \(\leq\) 101 | Non-terminaison ou explosion en queue — la cascade Monte-Carlo a 4 boucles de rejet non gardées dans l'original ; le port les borne toutes. |
I_NoMidLoopEvalDeadlock | Au plus un mlx_array_eval par graphe, pas en milieu de boucle | Détruit la performance MLX (matteo D6) et peut bloquer en attente du host — un mode d'échec spécifique à MLX, désormais formel. |
L_EveryMonomerTerminates (vivacité) | Chaque monomère atteint signed ∨ rolled_back | Stall silencieux. |
Résultat TLC : safety avec symétrie (Permutations(Anomalies)) \(\to\) 7 429 792 états explorés, zéro violation ; liveness sans symétrie \(\to\) 117 504 états, zéro violation ; mutation gate 8/8 WITNESSED (chaque invariant prouve qu'il détecterait sa propre violation synthétique — pas d'invariant qui ne mesure rien). SANY clean. Détails : formal/GpuFleet.tla + formal/TLC-RESULTS.md § GpuFleet.
L'oracle 4-témoins rooted-independent — la fin de la tautologie
Avant cette itération, la cross-validation reposait sur trois legs tous écrits par la même équipe contre le même kernel — une seule hypothèse répétée trois fois. La délibération a posé le théorème anti-tautologie (turing) : l'accord d'un ensemble d'oracles n'est une preuve que si aucun ancêtre partagé ne porte une erreur latente identique \(\to\) rooted independence.
Le nouvel oracle a quatre témoins, dont une racine externe :
| Témoin | Substrat | Source d'authorship | Rôle |
|---|---|---|---|
| W1 — Metal-A | Apple GPU | port indépendant (ce livrable) | leg de production GPU |
| W2 — Reference CPU | Apple CPU | port indépendant (le physics.rs historique) | leg numérique CPU |
| W3 — Fixture CUDA | host | les .cu originaux d'Agustin — jamais le port | clé de voûte anti-tautologie — la seule racine vraiment externe |
W4 — f_tot.jpg | image livrée | rendu original d'Agustin | veto-only — peut invalider, jamais certifier |
W3 est dérivé par compilation directe des kernels CUDA source ; il n'a jamais touché un seul port. Si Metal-A passe le golden W3 dans \(\varepsilon\), l'agreement est une preuve réelle, pas un écho. Si Metal-A passe les \(W1\leftrightarrow{}W2\) mais échoue W3, l'oracle a démasqué une erreur compensée — exactement ce qui s'est produit avec la divergence du modèle d'écran de W2 (voir § 05, F2).
La règle p_KS = 1,0 → FAIL est cousue dans G_oracle_execution_disjoint : un accord parfait entre deux legs signale une exécution partagée (collusion), pas une correction. Un vrai accord physique laisse une signature de bruit Monte-Carlo indépendante par leg.
fleet.toml.v5 — la config exécutable
La fleet n'est pas qu'une narration ; elle est inscrite en config TOML lisible par la chaîne cs :
- Topologie : pure-parallèle A ⟂ B (
forbid_guarded_sequence = true), jointe seulement à l'oracle. - 18 gates dans le registre, chacun avec son script
scripts/portage-gates/G_*.sh, son owner, et son lien vers la unit of work qui l'a posé. - Backends roster :
optix_rust,cpu_reference,metal,mlx_gpu?;active_backendà sémantique recovery-floor (le rollback est un swap de backend, pas une démotion de grade). - Apparatus C++ supprimé (
[deleted_from_v4]audit record auditable) — les gates ASan/UBSan/ABI/owning-pointers et les phases CAS1/CAS2 n'avaient pas d'analogue MSL+Rust ; les garder en silence eût été du cargo.
Cinq rôles anti-groupthink (janis) sont inscrits comme agents de la fleet, pas comme aspirations :
backend-advocate-B— dissidence assignée, dissent note obligatoire même vide ; charge de plaider FOR Monomère B et AGAINST le compute-bound. Owner du re-entry test.clean-pass-sentinel— autorité halt-promotion sur les passes trop propres : exact-zero first-pass delta, all-9-KS-pass avecgpu_namenon vérifié, barre de speedup non mesurée.- Trois adversariaux continus firing every-launch / every-measurement / every-image :
gpu-execution-adversary(tente une silent-CPU),perf-adversary(tente de gonfler le speedup),physics-forgery-adversary(tente une fabrication d'image plausible).
Plus un embargo sealed-commit entre les équipes A et B (artéfacts de benchmark hashés et révélés simultanément — pas de second-mover anchoring).
Le ratchet de grade et les gates load-bearing
Le code monte un ratchet monotone de grades : draft, built, l0, l1, image, red-teamed, signed. Un grade ne descend jamais sans raison enregistrée (G_no_silent_veto). Chaque promotion exige une évidence machine-parsable — pas de promotion sans artefact.
Parmi les 18 gates, sept sont load-bearing pour Monomère A (extraits) :
G_gpu_actually_ran— preuve d'exécution GPU hardware-attestée \((\geq\) 2 témoins forts + contrôle négatifRADIENCE_FORCE_CPU=1qui erre).G_speedup_floor\((\geq\) \(20\times\) vs baseline CPU scellée, ceiling 66 — au-dessus = falsification ; fenêtre [14,20) recalibration roofline).G_anomalies_preserved_runtime— comportemental, pas textuel ;-ffast-mathinterdit sur les TU de physique.G_physics_unit_golden_w3— per-function vs fixture CUDA W3, \(\varepsilon\) dérivés (docs/derived-epsilon-table.toml).G_ks_bonferroni— KS Bonferroni 9 fenêtres sur la grille.datf64 (jamais le JPEG).G_tail_ks— KS ciblé queue, attrape les rares branches (pair-production, fin de cascade) où le KS vanilla sous-puissance.G_oracle_execution_disjoint— anti-collusion,p = 1,0 → FAIL.
Une honnêteté inscrite dans le design — l'étape suivante
Un point appris en cours de route, inscrit ici parce qu'il qualifie la fiabilité de la machine : la première version du design nommait le piège (« un PNG vert sans que le run ait réellement tourné ») mais ne le bloquait pas structurellement. G_gpu_actually_ran + le typage ExecutionWitness ont été ajoutés précisément pour fermer ce trou — exécutif et compositionnel : non seulement le run produit une preuve, mais le type Rust rend l'absence de preuve impossible à compiler.
La leçon, et c'est elle le signal de fiabilité : nommer un risque dans une synthèse \(\neq\) le câbler dans un gate \(\neq\) l'inscrire dans le type-système. La fleet a appris de son propre angle mort, et la correction est maintenant structurelle au niveau du compilateur — pas seulement au niveau du gate. C'est ce type de boucle de correction — pas l'absence d'erreur — qui qualifie une orchestration agentique comme partenaire fiable.