Verificarea formală pentru toți — Dafny, Verus și viitorul

Context istoric

Verificarea formală a software-ului a fost, până recent, un efort extrem de costisitor:

| Proiect | Verificat | Efort | Raport proof/cod | |---|---|---|---| | seL4 (2009) | Kernel C | ~25 persoane·ani | 23:1 | | CompCert (2015) | Compilator C | ~20 persoane·ani | ~10:1 | | CakeML (2018) | Compilator ML | ~15 persoane·ani | ~15:1 | | IronFleet (2015) | Sistem distribuit | ~10 persoane·ani | ~30:1 |

Problema: nu poți aplica această metodologie la codul obișnuit — costă prea mult.

Tool-urile noi

Dafny (Microsoft)

Dafny e un limbaj de programare cu verificare formală incorporată. Spre deosebire de seL4, nu scrii demonstrația într-un theorem prover separat — scrii precondiții și postcondiții direct în același limbaj:

method BinarySearch(arr: array<int>, key: int) returns (index: int)
    requires forall i, j :: 0 <= i < j < arr.Length ==> arr[i] <= arr[j]
    ensures 0 <= index < arr.Length ==> arr[index] == key
    ensures index < 0 ==> forall i :: 0 <= i < arr.Length ==> arr[i] != key
{
    var low := 0;
    var high := arr.Length - 1;
    
    while low <= high
        invariant 0 <= low && high < arr.Length
        invariant forall i :: 0 <= i < arr.Length && !(low <= i <= high) 
                   ==> arr[i] != key
    {
        var mid := (low + high) / 2;
        if arr[mid] < key {
            low := mid + 1;
        } else if arr[mid] > key {
            high := mid - 1;
        } else {
            return mid;
        }
    }
    return -1;
}

Dafny verifică automat că:

• key există în array → returnezi indexul corect
• key nu există → returnezi -1
• Nu accesezi array-ul în afara limitelor
• Bucla se termină

Fără demonstrații separate, fără Isabelle/HOL. Doar specificații în același fișier.

Ce e remarcabil

• E folosit de AWS pentru S3, Lambda, și servicii critice
• Nu cere PhD în logică — e accesibil unui inginer cu experiență
• Rulează ca orice program (compilă la .NET, Java, Python, JS)
• Dafny e gratis și open source

Verus (AWS + Microsoft)

Verus e un tool de verificare formală pentru Rust. Scrii specificații ca note lângă codul Rust:

pub fn binary_search(arr: &[u32], key: u32) -> (result: isize)
    requires
        forall|i: int, j: int| 0 <= i < j < arr@.len() ==> arr@[i] <= arr@[j],
    ensures
        (0 <= result && result < arr@.len() ==> arr@[result as int] == key),
        (result < 0 ==> forall|i: int| 0 <= i < arr@.len() ==> arr@[i] != key),
{
    // Implementarea e Rust standard
}

Beneficiu: Rust + Verus — borrow checker-ul elimină bug-urile de memorie, Verus demonstrează corectitudinea funcțională. E ca și cum ai combina seL4 (kernel verificat) cu Rust (memorie sigură) — dar pentru cod obișnuit.

Aeneas (INRIA, Franța)

Aeneas e un tool care transformă automat cod Rust în demonstrații formale. Scrii Rust normal, Aeneas generează specificații în F (un theorem prover)* — și le verifică.

Dacă Dafny e "scrie specificații + cod", iar Verus e "adaugă note la Rust", Aeneas e "doar scrie Rust, demonstrația se generează singură" (pentru o clasă limitată de proprietăți).

Comparație

| Tool | Ce verifică | Limbaj | Efort | Folosit de | |---|---|---|---|---| | Dafny | Corectitudine funcțională | Limbaj propriu | Mediu | AWS S3, Lambda | | Verus | Corectitudine + memorie | Rust | Mediu-ridicat | AWS, cercetare | | Aeneas | Corectitudine | Rust → F* | Scăzut | Cercetare INRIA | | seL4/Isabelle | Totul | C → HOL | Extrem de ridicat | seL4 Foundation |

Când merită

| Scenariu | Merită verificare formală? | Tool | |---|---|---| | Funcție criptografică (AES, RSA) | ✅ Da | Dafny | | Protocol distribuit (Raft, Paxos) | ✅ Da | Dafny | | Algoritm de sortare | ✅ Da | Dafny / Verus | | Driver de rețea | ⚠️ Poate | Verus | | API REST | ❌ Nu | Testare clasică | | UI / frontend | ❌ Nu | Testare clasică |

Concluzie

Dacă seL4 a demonstrat că verificarea formală e posibilă, Dafny și Verus demonstrează că e practicabilă — nu mai e nevoie de 25 de persoane·ani și un PhD. Pentru componente critice (criptografie, protocoale, algoritmi), verificarea formală devine accesibilă unui inginer obișnuit. În 2026-2030, e de așteptat ca tool-urile să devină parte din pipeline-ul standard de CI/CD — la fel cum testele unitare sunt azi.