model-checking

6 posts

model-checkingautoverusrustverification

AutoVerus transforme 40 heures d'écriture de proof en 3 appels LLM. L'astuce consiste à savoir quand abandonner.

AutoVerus utilise un réseau d'agents LLM pour générer des proofs de correction Verus pour du code Rust, automatisant plus de 90% des proof obligations via une boucle générer-réparer-discharger pilotée par le feedback du solveur SMT.

La partie la plus difficile de la vérification formelle n'a jamais été le vérificateur. C'est l'écriture du proof. Donnez à un ingénieur Rust senior Verus, le…
model-checkingllmrustformal-proofs

Les LLMs peuvent générer du code Rust. Les preuves formelles sont un problème entièrement différent.

Les grands modèles de langage écrivent du Rust étonnamment bon, mais quand vous leur demandez une preuve formelle, ils hallucinent des invariants et inventent une syntaxe qu'aucun vérificateur n'accepte. Voici ce qu'ils font réellement bien, où ils échouent et comment les utiliser malgré tout.

Les LLMs peuvent écrire du Rust qui compile et même passe . Ce qu'ils ne peuvent pas faire de manière fiable, c'est écrire une preuve formelle que le code est…
model-checkingtemporal-logicformal-methodsverification

Vous pouvez vérifier du code par model checking sans apprendre la temporal logic

Les bounded model checkers comme Kani et les relational model finders comme Alloy permettent de vérifier des propriétés avec des assertions et des contraintes ordinaires. Vous renoncez aux preuves de liveness pour une courbe d'apprentissage mesurée en heures.

Vous n'avez pas besoin d'apprendre la logique temporelle linéaire pour utiliser un model checker. Des outils comme Kani, CBMC et Alloy vous permettent de…
model-checkingrustverificationformal-methods

Vous pouvez prouver votre code Rust correct sans écrire une seule preuve, mais l'espace d'états est la facture

Des outils de model checking comme Kani permettent de vérifier des propriétés Rust avec des assertions au lieu de preuves formelles. Le hic, c'est ce qui se passe quand vos boucles n'ont pas de petites bornes.

Vous pouvez prouver votre code Rust correct sans écrire une seule preuve. L'outil qui le fait s'appelle un model checker, et pour Rust le plus pratique en ce…
model-checkingdistributed-systemstlaplusprotocol-design

Vous ne pouvez pas unit tester un protocole distribué, mais vous pouvez le model checker

Les bugs distribués sont coûteux à corriger après déploiement. Le model checking vous permet de les trouver avant d'écrire une seule ligne de code d'implémentation. Voici comment faire avec TLA+.

Vous ne pouvez pas unit tester un protocole distribué. Un unit test exécute un processus sur une machine dans un ordre. Votre protocole exécute dix processus…