Skip to main content
agentl verify raisonne sur l’AST avant toute exécution réelle. La commande refuse d’émettre un verdict si check trouve une erreur.
--depth borne la recherche de route utilisée par les théorèmes concernés. La recherche peut s’arrêter plus tôt lorsqu’elle atteint son point fixe.

​
Ce que cherche le vérificateur

Le rapport couvre notamment :
  • les appels qui aboutiraient sous un interdit ;
  • les branches écrites mais toujours bloquées ;
  • les états où le but n’a plus de route ni d’escalade ;
  • la surface d’actions à risque exposée au LLM ;
  • les sorties structurées qui pilotent une cible sensible ;
  • les effets déclarés qui ne peuvent pas être démentis par une observation ;
  • les seuils probabilistes inatteignables.

​
Lire les verdicts

Une branche sûre ne produit pas nécessairement une ligne de rapport. Le vérificateur cherche à rester silencieux sur les sites qu’il peut établir sans ambiguïté.

​
Exemple de problème structurel

Le plan est bien formé, mais il peut tenter l’action dans un état interdit. Selon le reste du programme, le rapport peut signaler une exposition et l’absence de repli.

​
Corriger sans affaiblir

1

Reproduisez le contre-exemple

Transformez l’état signalé en SCENARIO pour éviter la régression.
2

Corrigez la route

Ajoutez une garde prouvable, une capacité alternative ou une escalade explicite.
3

Relancez toute la chaîne

check, test puis verify. Une correction de sûreté peut rendre un plan inatteignable ou casser un scénario.
La preuve porte sur le programme .agent et son modèle déclaré. Elle ne certifie ni l’implémentation d’un outil externe, ni la sûreté générale du Python hôte.

​
Limites à garder visibles

  • le solveur n’est pas déclaré complet pour tous les programmes ;
  • un EFFECT mensonger reste un contrat mensonger ;
  • l’analyse de frontière Python est syntaxique ;
  • un journal signé n’obtient pas pour autant un horodatage tiers.

Contrôler aussi l’hôte

Complétez la preuve du programme par l’analyse de la frontière Python.