Verus is een open-source automatische programma-verificator voor de programmeertaal Rust. Waar Rust met zijn typesysteem al veel bugs voorkomt, gaat Verus een stap verder door code mechanisch te controleren aan de hand van formele wiskundige specificaties. Dit stelt ontwikkelaars in staat om te bewijzen dat code correct is voor alle mogelijke inputs, wat verder gaat dan wat met traditioneel testen mogelijk is.
Belangrijke aspecten van Verus:
- Integratie: Specificaties (zoals precondities en postcondities) worden direct in de Rust-broncode geschreven met een Rust-achtige syntax, wat snelle feedbackloops mogelijk maakt.
- Automatisering: Dankzij het gebruik van solvers krijgen ontwikkelaars in minder dan een seconde feedback, wat ook de inzet van AI-agenten bij het genereren van bewijzen vergemakkelijkt.
- Veiligheid en Concurrency: Verus kan de veiligheid van
unsafe Rust-code wiskundig bewijzen en garandeert de correctheid van concurrente code via mechanismen zoals lock-invarianten.
De tool wordt op grote schaal ingezet door Amazon voor kritieke infrastructuur, zoals de Nitro Isolation Engine, en wordt gebruikt in diverse open-source projecten zoals de Atmosphere microkernel, de Anvil Kubernetes-controllers en de Verdict-cryptografische bibliotheek.
Ontwikkelen van bewijsbaar correcte Rust-code met Verus
Door Bryan Parno 31 augustus 2026
Belangrijkste punten
- Verus is een open-source automatische programma-verificator voor Rust die code mechanisch controleert aan de hand van formele wiskundige specificaties voor alle mogelijke inputs. Dit gaat verder dan traditioneel testen om zeldzame 'corner cases' te vangen.
- Ontwikkelaars annoteren Rust-broncode direct met precondities en postcondities met behulp van een Rust-achtige syntax. Dit maakt snelle feedbackloops mogelijk (onder de ene seconde) en stelt AI-agenten in staat om te helpen bij het genereren van bewijzen.
- Verus maakt wiskundige verificatie mogelijk van Rust's
unsafe code-blokken en concurrente code met aangepaste locking-schema's. Hiermee worden machine-gecontroleerde veiligheidsgaranties hersteld voor prestatie-kritische implementaties, zoals de Nitro Isolation Engine van AWS.
- Amazon gebruikt Verus om de correctheid van cruciale primitieven in kritieke infrastructuur te bewijzen. De tool is ook overgenomen door open-source projecten, waaronder bibliotheken voor certificaatvalidatie, parsers voor dataformaten en gedistribueerde systemen zoals Kubernetes-controllers.
---
Veel open-source en industriële softwareprojecten, waaronder diverse projecten bij Amazon, maken gebruik van de programmeertaal Rust. Rust biedt prestaties en flexibiliteit die vergelijkbaar zijn met die van de C-taal, terwijl het slimme typesysteem automatisch een verscheidenheid aan bugs en beveiligingskwetsbaarheden voorkomt. Het resultaat is snelle code die gemiddeld correcter en veiliger is.
Echter, "correcter en veiliger" is niet hetzelfde als "daadwerkelijk correct en veilig". In C is het bijvoorbeeld een gevaarlijke fout om buiten de grenzen van een array te treden (indexing into an array past the boundary of the memory allotted to it), wat onvoorziene gevolgen kan hebben. In Rust zal het programma in zo'n geval stoppen, wat zeker veiliger is, maar een correct programma zou een out-of-bounds toegang in de eerste plaats nooit uitvoeren. Evenzo kan Rust niet garanderen dat je programma de resultaten berekent die je verwachtt, of dat het geen geheimen lekt waar het toegang toe heeft. Daar komt Verus in beeld.
Het buiten de grenzen van een array treden is een gevaarlijke fout die onvoorziene gevolgen kan hebben. Een correct programma zou dit niet toestaan.
Wat is Verus?
Verus is een open-source, automatische programma-verificator voor Rust. Een "programma-verificator" neemt een formele wiskundige specificatie van hoe je code zich zou moeten gedragen en controleert mechanisch of je code aan die specificatie voldoet voor alle mogelijke inputs.
Stel dat je code een geoptimaliseerd binair zoekalgoritme implementeert om een bepaalde waarde in een gesorteerde array te vinden. De specificatie zou kunnen stellen dat wanneer de code succesvol een index retourneert, het bijbehorende element in de array overeenkomt met de gezochte waarde. De verificator controleert of deze specificatie geldt voor alle mogelijke input-arrays en doelwaarden.
In tegenstelling tot traditionele testtechnieken, die slechts een paar specifieke arrays proberen en daardoor zeldzame gevallen kunnen missen (bijvoorbeeld: wat als de doelwaarde het laatste element in de array is, of helemaal niet aanwezig is?), houdt programma-verificatie in dat er een wiskundig bewijs wordt geconstrueerd dat de code overeenkomt met de specificatie.
In een automatische programma-verificator zoals Verus handelt de tool veel van de saaie, laagwaardige stappen van de bewijsvoering automatisch af, terwijl de menselijke ontwikkelaar high-level begeleiding biedt (bijvoorbeeld door een inductief bewijs op te zetten of een loop-invariant te leveren). Tegenwoordig kunnen zelfs deze high-level stappen vaak worden geautomatiseerd door AI.
Amazon is een oprichtend lid van de Rust Foundation en gebruikt Rust uitgebreid voor projecten zoals Firecracker (dat AWS Lambda en AWS Fargate aandrijft), onze serverless gedistribueerde SQL-database en de Nitro Isolation Engine (die virtuele-machine-isolatie afdwingt voor de Nitro-hypervisor). Gecombineerd met meer dan een decennium werk aan automated reasoning, was het een logische stap om Verus te adopteren. We hebben Verus gebruikt om de correctheid te bewijzen van cruciale primitieven in de Nitro Isolation Engine en diverse andere kritieke infrastructuur binnen Amazon.
Rust-code verifiëren met Verus
Met Verus kan een Rust-ontwikkelaar specificaties (en bewijzen) voor bestaande Rust-code direct in de bronbestanden toevoegen. In het voorbeeld van de zoekfunctie ziet een Verus-specificatie (geschreven als een Rust-annotatie) er als volgt uit:
- Preconditie (aangegeven door het trefwoord
requires): stelt de voorwaarden vast die waar moeten zijn voordat de functie wordt uitgevoerd. In het geval van een binaire zoekopdracht is de preconditie dat de array gesorteerd moet zijn.
- Postconditie (aangegeven door het trefwoord
ensures): stelt de voorwaarden vast die waar moeten zijn nadat de functie is uitgevoerd. Hier staat dat als de functie Some(index) retourneert, de index binnen de grenzen van de array moet vallen en de waarde op die index overeen moet komen met de gezochte waarde.
Belangrijk is dat de specificatie ook stelt dat als de functie None retourneert, de doelwaarde niet in de array aanwezig is. Zonder deze tweede clausule zou de specificatie ook voldaan kunnen worden door een implementatie die altijd None retourneert. Normale Rust-compilers negeren deze Verus-annotaties, waardoor geannoteerde code kan worden gebruikt door zowel geverifieerde als niet-geverifieerde projecten, inclusief die die gebruikmaken van de build-tool Cargo.
Ontwerpprincipes en automatisering
Een kernpunt van Verus is dat ontwikkelaars specificaties en bewijzen schrijven in hun broncode met behulp van een Rust-achtige syntax. Wanneer een bewijs mislukt, krijgt de ontwikkelaar foutmeldingen in Rust-stijl op bronniveau. Dit houdt de bewijzen synchroon met de eigenlijke code en voorkomt dat ontwikkelaars een volledig nieuwe taal of tool moeten leren.
Verus richt zich daarnaast op snelle, krachtige automatisering door verschillende solvers te gebruiken om de bewijslast te verwerken. In de praktijk krijgen ontwikkelaars feedback op hun code en bewijzen in minder dan een seconde, wat een interactieve ontwikkelcyclus mogelijk maakt (inclusief "rode kringeltjes" in IDE's zoals VS Code).
Op projectniveau kan Verus complexe projecten met duizenden regels code en bewijs verifiëren in de tijd die eerdere verificatoren nodig hadden voor een enkele functie. Deze snelheid helpt niet alleen mensen, maar ook AI-agenten bij het ontwikkelen van Verus-bewijzen, omdat ze sneller kunnen itereren.
Veiligheid en concurrency
Hoewel het typesysteem van Rust sterke veiligheidsgaranties biedt, kan het ontwikkelaars soms belemmeren in het schrijven van high-performance code. Daarom staat Rust toe dat ontwikkelaars expliciet gelabelde unsafe code schrijven. In dit geval controleert de compiler de veiligheid niet meer mechanisch; het is aan de ontwikkelaar om het correct te doen. Met Verus kunnen ontwikkelaars echter de veiligheid van deze unsafe Rust-code wiskundig bewijzen, waardoor machine-gecontroleerde veiligheidsgaranties worden hersteld.
Tevens bouwt Verus voort op de "fearless concurrency" van Rust. Verus stelt ontwikkelaars in staat om te bewijzen dat concurrente code niet alleen veilig is, maar ook correct.
Voorbeeld hiervan zijn locks, die een processor-thread exclusieve toegang geven tot data. Verus staat toe dat ontwikkelaars een invariant eigenschap aan een lock toevoegen. Dit betekent dat iedereen die de lock verkrijgt, een waarde krijgt die aan de invariant voldoet (bijv. de waarde is altijd even), en bij het vrijgeven van de lock moet worden bewezen dat de waarde nog steeds aan die eigenschap voldoet. Dit is essentieel voor programma's zoals de Nitro Isolation Engine, die vertrouwt op complexe, aangepaste locking-schema's voor hoge prestaties.
De garanties van Verus rusten uiteraard op de correctheid van Verus zelf, de top-level specificaties, de aannames over de runtime (zoals de Rust standard library) en de compiler toolchain.
Verus in het open-source ecosysteem
Naast het gebruik bij Amazon wordt Verus ingezet in diverse open-source projecten:
- Vest: Genereert automatisch Rust-code om data in een binair formaat te parsen en te serialiseren, inclusief Verus-bewijzen voor correctheid en beveiliging.
- Verdict: Een bewijsbaar correcte en veilige bibliotheek voor de validatie van certificaten voor de x.509 public-key cryptografie standaard.
- CapybaraKV: Verifieert de correctheid en crash-veiligheid van persistent-memory logs, die data in een correcte staat behouden, zelfs bij een onverwachte systeemcrash of stroomuitval.
- Atmosphere: Een microkernel (minimaal besturingssysteem) ontwikkeld in Rust en geverifieerd voor correctheid met Verus.
- Anvil: Bewijst de correctheid en "liveness" van controllers voor Kubernetes. Anvil toont aan dat de controllers het systeem onder redelijke aannames uiteindelijk in een stabiele staat zullen brengen.
- CortenMM: Een geheugenbeheersysteem met een transactionele interface en schaalbare locking-protocollen, waarvan de concurrente code is geverifieerd met Verus.
Verus zelf is een gratis, open-source project, ontwikkeld door een gedistribueerde samenwerking tussen academische en industriële onderzoekers.
***
Over de auteur Bryan Parno is een Amazon Scholar en de Kavčić-Moura Professor of Electrical and Computer Engineering and Computer Science aan Carnegie Mellon University, waar hij het Secure Foundations Lab leidt. Zijn onderzoek richt zich op fundamentele verbeteringen in het ontwerpen en bouwen van veilige systemen, met een nadruk op formeel geverifieerde software.
Ontwikkelen van bewijsbaar correcte Rust-code met Verus
Door Bryan Parno 31 augustus 2026
Belangrijkste punten
- Verus is een open-source automatische programma-verificator voor Rust die code mechanisch controleert aan de hand van formele wiskundige specificaties voor alle mogelijke inputs. Dit gaat verder dan traditioneel testen om zeldzame 'corner cases' te vangen.
- Ontwikkelaars annoteren Rust-broncode direct met precondities en postcondities met behulp van een Rust-achtige syntax. Dit maakt snelle feedbackloops mogelijk (onder de ene seconde) en stelt AI-agenten in staat om te helpen bij het genereren van bewijzen.
- Verus maakt wiskundige verificatie mogelijk van Rust's
unsafe code-blokken en concurrente code met aangepaste locking-schema's. Hiermee worden machine-gecontroleerde veiligheidsgaranties hersteld voor prestatie-kritische implementaties, zoals de Nitro Isolation Engine van AWS.
- Amazon gebruikt Verus om de correctheid van cruciale primitieven in kritieke infrastructuur te bewijzen. De tool is ook overgenomen door open-source projecten, waaronder bibliotheken voor certificaatvalidatie, parsers voor dataformaten en gedistribueerde systemen zoals Kubernetes-controllers.
---
Veel open-source en industriële softwareprojecten, waaronder diverse projecten bij Amazon, maken gebruik van de programmeertaal Rust. Rust biedt prestaties en flexibiliteit die vergelijkbaar zijn met die van de C-taal, terwijl het slimme typesysteem automatisch een verscheidenheid aan bugs en beveiligingskwetsbaarheden voorkomt. Het resultaat is snelle code die gemiddeld correcter en veiliger is.
Echter, "correcter en veiliger" is niet hetzelfde als "daadwerkelijk correct en veilig". In C is het bijvoorbeeld een gevaarlijke fout om buiten de grenzen van een array te treden (indexing into an array past the boundary of the memory allotted to it), wat onvoorziene gevolgen kan hebben. In Rust zal het programma in zo'n geval stoppen, wat zeker veiliger is, maar een correct programma zou een out-of-bounds toegang in de eerste plaats nooit uitvoeren. Evenzo kan Rust niet garanderen dat je programma de resultaten berekent die je verwachtt, of dat het geen geheimen lekt waar het toegang toe heeft. Daar komt Verus in beeld.
Het buiten de grenzen van een array treden is een gevaarlijke fout die onvoorziene gevolgen kan hebben. Een correct programma zou dit niet toestaan.
Wat is Verus?
Verus is een open-source, automatische programma-verificator voor Rust. Een "programma-verificator" neemt een formele wiskundige specificatie van hoe je code zich zou moeten gedragen en controleert mechanisch of je code aan die specificatie voldoet voor alle mogelijke inputs.
Stel dat je code een geoptimaliseerd binair zoekalgoritme implementeert om een bepaalde waarde in een gesorteerde array te vinden. De specificatie zou kunnen stellen dat wanneer de code succesvol een index retourneert, het bijbehorende element in de array overeenkomt met de gezochte waarde. De verificator controleert of deze specificatie geldt voor alle mogelijke input-arrays en doelwaarden.
In tegenstelling tot traditionele testtechnieken, die slechts een paar specifieke arrays proberen en daardoor zeldzame gevallen kunnen missen (bijvoorbeeld: wat als de doelwaarde het laatste element in de array is, of helemaal niet aanwezig is?), houdt programma-verificatie in dat er een wiskundig bewijs wordt geconstrueerd dat de code overeenkomt met de specificatie.
In een automatische programma-verificator zoals Verus handelt de tool veel van de saaie, laagwaardige stappen van de bewijsvoering automatisch af, terwijl de menselijke ontwikkelaar high-level begeleiding biedt (bijvoorbeeld door een inductief bewijs op te zetten of een loop-invariant te leveren). Tegenwoordig kunnen zelfs deze high-level stappen vaak worden geautomatiseerd door AI.
Amazon is een oprichtend lid van de Rust Foundation en gebruikt Rust uitgebreid voor projecten zoals Firecracker (dat AWS Lambda en AWS Fargate aandrijft), onze serverless gedistribueerde SQL-database en de Nitro Isolation Engine (die virtuele-machine-isolatie afdwingt voor de Nitro-hypervisor). Gecombineerd met meer dan een decennium werk aan automated reasoning, was het een logische stap om Verus te adopteren. We hebben Verus gebruikt om de correctheid te bewijzen van cruciale primitieven in de Nitro Isolation Engine en diverse andere kritieke infrastructuur binnen Amazon.
Rust-code verifiëren met Verus
Met Verus kan een Rust-ontwikkelaar specificaties (en bewijzen) voor bestaande Rust-code direct in de bronbestanden toevoegen. In het voorbeeld van de zoekfunctie ziet een Verus-specificatie (geschreven als een Rust-annotatie) er als volgt uit:
- Preconditie (aangegeven door het trefwoord
requires): stelt de voorwaarden vast die waar moeten zijn voordat de functie wordt uitgevoerd. In het geval van een binaire zoekopdracht is de preconditie dat de array gesorteerd moet zijn.
- Postconditie (aangegeven door het trefwoord
ensures): stelt de voorwaarden vast die waar moeten zijn nadat de functie is uitgevoerd. Hier staat dat als de functie Some(index) retourneert, de index binnen de grenzen van de array moet vallen en de waarde op die index overeen moet komen met de gezochte waarde.
Belangrijk is dat de specificatie ook stelt dat als de functie None retourneert, de doelwaarde niet in de array aanwezig is. Zonder deze tweede clausule zou de specificatie ook voldaan kunnen worden door een implementatie die altijd None retourneert. Normale Rust-compilers negeren deze Verus-annotaties, waardoor geannoteerde code kan worden gebruikt door zowel geverifieerde als niet-geverifieerde projecten, inclusief die die gebruikmaken van de build-tool Cargo.
Ontwerpprincipes en automatisering
Een kernpunt van Verus is dat ontwikkelaars specificaties en bewijzen schrijven in hun broncode met behulp van een Rust-achtige syntax. Wanneer een bewijs mislukt, krijgt de ontwikkelaar foutmeldingen in Rust-stijl op bronniveau. Dit houdt de bewijzen synchroon met de eigenlijke code en voorkomt dat ontwikkelaars een volledig nieuwe taal of tool moeten leren.
Verus richt zich daarnaast op snelle, krachtige automatisering door verschillende solvers te gebruiken om de bewijslast te verwerken. In de praktijk krijgen ontwikkelaars feedback op hun code en bewijzen in minder dan een seconde, wat een interactieve ontwikkelcyclus mogelijk maakt (inclusief "rode kringeltjes" in IDE's zoals VS Code).
Op projectniveau kan Verus complexe projecten met duizenden regels code en bewijs verifiëren in de tijd die eerdere verificatoren nodig hadden voor een enkele functie. Deze snelheid helpt niet alleen mensen, maar ook AI-agenten bij het ontwikkelen van Verus-bewijzen, omdat ze sneller kunnen itereren.
Veiligheid en concurrency
Hoewel het typesysteem van Rust sterke veiligheidsgaranties biedt, kan het ontwikkelaars soms belemmeren in het schrijven van high-performance code. Daarom staat Rust toe dat ontwikkelaars expliciet gelabelde unsafe code schrijven. In dit geval controleert de compiler de veiligheid niet meer mechanisch; het is aan de ontwikkelaar om het correct te doen. Met Verus kunnen ontwikkelaars echter de veiligheid van deze unsafe Rust-code wiskundig bewijzen, waardoor machine-gecontroleerde veiligheidsgaranties worden hersteld.
Tevens bouwt Verus voort op de "fearless concurrency" van Rust. Verus stelt ontwikkelaars in staat om te bewijzen dat concurrente code niet alleen veilig is, maar ook correct.
Voorbeeld hiervan zijn locks, die een processor-thread exclusieve toegang geven tot data. Verus staat toe dat ontwikkelaars een invariant eigenschap aan een lock toevoegen. Dit betekent dat iedereen die de lock verkrijgt, een waarde krijgt die aan de invariant voldoet (bijv. de waarde is altijd even), en bij het vrijgeven van de lock moet worden bewezen dat de waarde nog steeds aan die eigenschap voldoet. Dit is essentieel voor programma's zoals de Nitro Isolation Engine, die vertrouwt op complexe, aangepaste locking-schema's voor hoge prestaties.
De garanties van Verus rusten uiteraard op de correctheid van Verus zelf, de top-level specificaties, de aannames over de runtime (zoals de Rust standard library) en de compiler toolchain.
Verus in het open-source ecosysteem
Naast het gebruik bij Amazon wordt Verus ingezet in diverse open-source projecten:
- Vest: Genereert automatisch Rust-code om data in een binair formaat te parsen en te serialiseren, inclusief Verus-bewijzen voor correctheid en beveiliging.
- Verdict: Een bewijsbaar correcte en veilige bibliotheek voor de validatie van certificaten voor de x.509 public-key cryptografie standaard.
- CapybaraKV: Verifieert de correctheid en crash-veiligheid van persistent-memory logs, die data in een correcte staat behouden, zelfs bij een onverwachte systeemcrash of stroomuitval.
- Atmosphere: Een microkernel (minimaal besturingssysteem) ontwikkeld in Rust en geverifieerd voor correctheid met Verus.
- Anvil: Bewijst de correctheid en "liveness" van controllers voor Kubernetes. Anvil toont aan dat de controllers het systeem onder redelijke aannames uiteindelijk in een stabiele staat zullen brengen.
- CortenMM: Een geheugenbeheersysteem met een transactionele interface en schaalbare locking-protocollen, waarvan de concurrente code is geverifieerd met Verus.
Verus zelf is een gratis, open-source project, ontwikkeld door een gedistribueerde samenwerking tussen academische en industriële onderzoekers.
***
Over de auteur Bryan Parno is een Amazon Scholar en de Kavčić-Moura Professor of Electrical and Computer Engineering and Computer Science aan Carnegie Mellon University, waar hij het Secure Foundations Lab leidt. Zijn onderzoek richt zich op fundamentele verbeteringen in het ontwerpen en bouwen van veilige systemen, met een nadruk op formeel geverifieerde software.
Groetjes,