rust

9 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-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…
capability-based-securityrustcap-stdsandboxing

Vos dépendances peuvent lire n'importe quel fichier sur le disque. cap-std les force à demander la permission.

La bibliothèque standard de Rust accorde une autorité ambiante sur le système de fichiers à chaque dépendance. cap-std la remplace par des APIs basées sur les capabilities qui forcent le code à prouver qu'il a le droit d'accéder à un chemin avant de l'ouvrir.

N'importe quelle crate dans votre arbre de dépendances peut ouvrir , écrire dans votre répertoire , ou énumérer chaque fichier de votre projet. La bibliothèque…
type-level-correctnesserror-handlingtypescriptrust

Arrêtez de lancer des erreurs que votre vérificateur de types ne peut pas voir

Les exceptions lancées masquent les chemins d'échec à votre système de types. Voici pourquoi les retours d'erreur explicites rendent votre code plus honnête, et comment les adopter sans vous détester.

La signature de votre fonction dit qu'elle retourne un . C'est faux. Elle retourne un ou elle explose. Le système de types ne connaît simplement pas la seconde…
deep-divesmutation-testingrustcargo-mutantstest-quality

Le mutation testing en Rust fonctionne, mais vos temps de compilation vont le détester

cargo-mutants trouve les tests qui font semblant de vérifier votre code. Voici comment fonctionne le mutation testing pour Rust, ce qu'il détecte, et si le coût en temps de compilation en vaut la peine.

Vous avez 100 % de couverture de lignes. Chaque branche est exécutée. Chaque fonction est appelée. Puis quelqu'un change un en dans votre logique de…
deep-divesrustproperty-based-testingquickcheckproptest

Les tests basés sur les propriétés en Rust trouvent les bugs que vos tests unitaires ne détectent pas

Le test par exemple ne couvre que les entrées auxquelles vous avez pensé. Le test basé sur les propriétés génère des données aléatoires, vérifie les invariants et réduit les échecs à des contre-exemples minimaux.

Vous avez écrit une fonction . Vous l'avez testée avec et . Elle passe. Vous livrez. Un utilisateur passe un slice à un seul élément. Votre fonction l'ignore.…
deep-divesrustruntime-contractsperformance

Les Runtime Contracts en Rust peuvent être sans coût en release, mais le compilateur ne le fera pas à votre place

Rust élimine automatiquement les debug assertions, mais un vrai design-by-contract nécessite plus que debug_assert!. Voici comment construire des runtime contracts sans coût qui disparaissent de votre binaire release.

Rust peut appliquer des runtime contracts en développement et les effacer complètement des builds release. La mise en garde est que le langage ne traite pas…