Huit preuves formelles vertes devenues cinq preuves validables après l'audit des assertions SystemVerilog
J'ai vu un tableau de bord formel synthétique rapporter 8/8 PROVEN, puis j'ai vu son propre audit n'en certifier que 5/8 comme TRUSTWORTHY. Ce revirement est le point de départ de Proof Firewall, notre démonstration exécutable de gouvernance pour les assertions SystemVerilog (SVA) générées par l'IA, et il a changé le niveau d'exigence auquel je souhaite soumettre une preuve verte avant qu'elle n'atteigne une revue de validation finale (sign-off) de tape-out.
J'ai construit le tableau de bord avec des propriétés « créées par LLM » issues de bancs de test fixes sur un arbitre synthétique, un pipeline à deux étages et une traversée de domaines d'horloge (CDC), car les cas embarrassants méritent d'être visibles. Une assertion peut paraître parfaitement respectable dans un registre de propriétés. Un moteur formel peut renvoyer un résultat vert. Pourtant, l'implication peut n'avoir jamais eu à travailler, ou elle peut continuer à passer alors même que le comportement pertinent du design a été corrompu. J'avais l'habitude de traiter le mot PROVEN comme un point d'arrivée. Construire cette démonstration m'a forcé à le considérer comme le début d'un examen des preuves.
La démonstration Proof Firewall ne remplace pas un moteur formel, n'ingère pas de RTL réel et n'appelle pas de LLM en direct dans son parcours par défaut. Elle est délibérément plus compacte et plus facile à inspecter : un vérificateur de modèles à états explicites en pur Python évalue une représentation intermédiaire (IR) synthétique de système de transitions, puis une porte de gouvernance vérifie l'accessibilité des antécédents, l'élimination des mutations et le cône d'influence (COI). La sortie constitue soit un motif pour enregistrer un certificat de démonstration signé, soit une raison de retenir le résultat pour un examen humain.
J'ai commencé avec le mauvais type de vert
Je me souviens que la première version du tableau de bord était rassurante précisément parce qu'elle était si limpide. Huit propriétés, huit badges verts, et une vue du flux brut qui donnait l'impression que le travail était terminé. Mon premier réflexe a été de faire en sorte que la démonstration explique mieux ce résultat limpide. Je pensais que la tâche d'ingénierie relevait de la présentation : faire émerger les preuves, montrer les assertions, rendre le tableau de bord plus facile à croire. Le résultat vert était réel, mais il répondait à une question bien plus restreinte que celle qu'un réviseur doit poser.
Ensuite, j'ai soumis ces mêmes huit propriétés aux vérifications qu'une véritable discussion de validation finale exige. L'antécédent est-il jamais devenu vrai ? L'assertion protesterait-elle si une partie pertinente du design était modifiée ? Contraint-elle un COI significatif ? Ces questions sont moins flatteuses qu'un badge vert, car elles interrogent ce que la preuve a réellement mérité, et non simplement ce que le solveur a renvoyé.
J'ai dû abandonner la formulation initiale du projet. Un écran affichant 8/8 PROVEN était une vue exacte de la référence en flux brut, mais restait incomplet en tant que bilan de sign-off. Après l'audit du pare-feu, ce même tableau synthétique fixe compte cinq résultats TRUSTWORTHY, un résultat VACUOUS et deux résultats WEAK. Les trois restants ne sont pas requalifiés en succès. Ils sont retenus avec les éléments de preuve qui expliquent pourquoi. Une étiquette de preuve et une décision de validation sont deux artefacts distincts.
J'ai choisi le mot « gouvernance » avec soin ici. Les contrôles déterministes de la démonstration rendent la décision de validation auditable. Un auteur de SVA optionnel peut proposer une assertion, mais le vérificateur de modèles et la porte de règles déterminent le verdict. Les agents conseillent, le code décide. J'essayais de rendre la porte suffisamment lisible pour que le résultat négatif soit utile plutôt que simplement embarrassant. Un résultat retenu nécessite une justification qu'un ingénieur de vérification peut inspecter, reproduire et contester.
ARB3 a rendu le problème impossible à ignorer
J'ai découvert la défaillance la plus flagrante dans ARB3, la propriété de l'arbitre synthétique assert (g0 && g1) |-> (turn == 0). Dans le flux brut, elle est verte. Lorsque j'ai ouvert son chronogramme et les preuves d'accessibilité, l'antécédent g0 && g1 était inaccessible dans cet arbitre synthétique. L'implication n'avait été prouvée qu'au sens étroit où elle n'a jamais été contrainte de répondre de l'état qu'elle décrivait. L'antécédent ne se déclenche jamais.
Cette distinction est facile à énoncer et difficile à garder à l'esprit lorsqu'un tableau de bord de vérification est tout vert. Au départ, j'avais interprété l'implication comme une affirmation sur le comportement d'arbitrage. Le résultat d'accessibilité a transformé ma lecture. Il s'agissait d'une affirmation dont la condition de déclenchement ne se produisait jamais. Qualifier cela de VACUOUS est plus utile que de préserver une étiquette verte, car cela oriente le réviseur vers l'hypothèse ou le stimulus qui a vidé la preuve de sa substance.
Je n'ai cessé de revenir à ce panneau en travaillant sur les étiquettes de règles. VACUOUS peut sembler être un résultat sévère jusqu'à ce que l'on envisage l'alternative. Si un dossier de sign-off conserve une preuve sans consigner que son antécédent ne se déclenche jamais, la revue a reçu une conclusion dépourvue de la condition qui lui donne son sens. Le meilleur dossier est celui qui explicite la limitation et fournit à un humain un élément concret à examiner. Cet enregistrement d'accessibilité a sa place aux côtés du verdict.
J'ai également dû résister à la tentation de traiter la vacuité comme un simple avertissement cosmétique. Si la propriété est censée contraindre une condition d'arbitrage, un déclenchement inaccessible constitue une preuve capitale pour déterminer si la propriété a réellement sollicité le comportement prévu. Le tableau de bord ne devrait pas demander à un réviseur de déduire cela d'un résultat vert. Il doit conserver le constat d'accessibilité, exclure le résultat de la voie de certification et rendre évidente l'action de révision suivante.
Le contexte industriel a renforcé les enjeux à mes yeux. L'étude Wilson Research Group / Siemens EDA de 2024 citée dans la spécification de la démonstration rapporte un taux de réussite au premier silicium de 14 %. Il ne s'agit pas d'une mesure réalisée par Veriprajna, et ce tableau de bord synthétique ne prétend pas expliquer ce chiffre. Mais cela me rend bien moins disposé à considérer l'état flatteur d'un tableau de bord comme une preuve en soi.
La propriété du pipeline a survécu à la corruption qu'elle était censée détecter
J'ai rencontré la deuxième défaillance en testant PIPE3, une propriété synthétique de pipeline à deux étages : assert v2 |-> (s2 == s2). Je voulais un exemple concis d'assertion qui paraisse suffisamment raisonnable pour passer inaperçue lors d'une revue superficielle. Le conséquent est une tautologie. Il affirme que s2 est égal à lui-même. Le conséquent ne contraint rien.
L'avancée importante de la démonstration ne consiste pas seulement à repérer la tautologie dans le texte. La porte de gouvernance injecte des mutations ponctuelles pertinentes dans le design et vérifie si la propriété les élimine. Pour le cas mis en avant du pipeline faible, PIPE3 enregistre un résultat d'élimination des mutations de 0/6. La propriété survit aux variantes corrompues pertinentes. C'est pourquoi la règle lui attribue la mention WEAK plutôt que de laisser le simple résultat PROVEN servir de preuve pour la validation finale. Le résultat de mutation teste une sensibilité réellement utile.
J'ai tiré un enseignement dérangeant en essayant de rendre cet exemple moins évident. Un humain peut lire s2 == s2 et l'écarter rapidement. De nombreuses faiblesses ne s'annoncent pas aussi clairement. C'est pourquoi je ne voulais pas que la démonstration repose sur la capacité de l'opérateur à repérer une chaîne suspecte. L'artefact utile réside dans la procédure : l'accessibilité, un test pertinent d'élimination des mutations, le COI et une décision de règles qui en consigne le motif.
J'en suis venu à considérer la vérification par mutation comme une méthode rigoureuse pour refuser une interprétation trop arrangeante d'une preuve. Le but n'est pas de fabriquer un échec spectaculaire. Il s'agit de déterminer si la propriété remarquerait une modification locale pertinente dans le comportement qu'elle est censée contraindre. Quand ce n'est pas le cas, le résultat transmet au réviseur une information exploitable : cette assertion nécessite d'être renforcée ou de suivre un parcours d'examen distinct avant de pouvoir étayer le dossier de sign-off.
C'est aussi pourquoi le banc d'évaluation de la démonstration nécessite une description précise. Son exécution locale python -m backend.bench obtient un score de 18/18 sur un ensemble fixe d'assertions synthétiques étiquetées et identifie 6 preuves que la référence sans porte de contrôle de la démonstration aurait validées aveuglément. Ces chiffres constituent un test de reproductibilité sur les bancs d'essai étiquetés de cette démonstration. Ils ne représentent pas un taux de production, une affirmation générale sur les assertions générées par l'IA, ni une comparaison avec des outils formels commerciaux.
J'ai cessé de vouloir faire paraître la porte permissive
J'ai été confronté à un choix de conception après les premiers résultats d'audit : adoucir les verdicts retenus pour rendre le tableau de bord plus optimiste, ou laisser le tableau refuser de certifier ce qu'il ne pouvait pas défendre. J'ai choisi cette seconde option, car une véritable revue de sign-off doit être capable de distinguer une preuve complète d'une preuve bornée, un antécédent inaccessible d'une propriété significative, et un contrôle faible d'un contrôle qui réagit à un comportement corrompu pertinent. La retenue d'un résultat est une issue d'examen, pas une impasse.
Ce choix se reflète dans le vocabulaire des règles. TRUSTWORTHY permet d'obtenir le certificat de démonstration signé. BOUNDED-PROVEN, VACUOUS, WEAK, DEAD et VIOLATED conservent les différents motifs de refus de ce certificat ou d'escalade du résultat. Dans le banc d'essai CDC, par exemple, la propriété plus stricte assert (req && !ack) |-> ##1 req est VIOLATED et produit un chronogramme de contre-exemple synthétique concret. Elle illustre une classe de défaillance liée à une perte de transaction ou de CDC. Elle n'affirme rien quant à une puce client.
Je ne conçois pas cela comme un plaidoyer pour remplacer le moteur existant d'une équipe de vérification. La direction en production est agnostique vis-à-vis du moteur : placer une porte de contrôle autour d'un flux formel existant, puis rendre ses critères d'acceptation inspectables. Les adaptateurs pour moteurs réels et l'ingestion de RTL sont différés dans cette démonstration. Le périmètre démontré est intentionnellement restreint. Cette délimitation est essentielle, car elle maintient les affirmations à la juste mesure de ce qui s'exécute réellement.
Je veux désormais la pièce justificative aux côtés du verdict
Je repense sans cesse à l'artefact dont une réunion de validation finale (sign-off) a besoin lorsque l'auteur des assertions est assisté par l'IA. Il ne s'agit pas d'un score de confiance émis par l'auteur. C'est un rapport consignant quels contrôles ont été exécutés, quel a été le résultat d'accessibilité, quelles mutations ont été éliminées, ce que contenait le COI et pourquoi la règle a accordé ou retenu la certification. La revue a besoin de preuves qu'elle peut rouvrir.
C'est ce que la démonstration exporte dans signoff_certificate.json : les verdicts par propriété, l'accessibilité, les résultats de mutation, le COI, les enregistrements de contre-exemples le cas échéant, et un champ SHA-256. J'ai conçu ce certificat comme un dossier de démonstration, car un réviseur doit pouvoir reconstituer la décision sans accepter un badge vert sur parole. Un certificat doit conserver le cheminement menant à son verdict.
Et si vous préférez le voir en action plutôt que de me lire le décrire, voici l'ensemble qui s'exécute de bout en bout.
J'ai rendu la démonstration exécutable afin que le revirement de 8/8 à 5/8 puisse être inspecté plutôt que répété comme un slogan. La leçon que j'en tire est modeste mais pérenne : une preuve digne d'être enregistrée porte en elle les éléments attestant de ce qu'elle a contraint, de ce à quoi elle a survécu et des raisons pour lesquelles on peut s'y fier. Le vert reste utile. Il a simplement besoin d'un dossier qui permette au réviseur suivant de décider s'il mérite d'aller plus loin.
