· ai-devtools
Full-stack verification is the new trend
There have been several recent announcements about formal verification of software and hardware, both using AI and for AI systems: The common factor in these announcements is the goal of achieving full-stack formalization, either across the software stack or across a combination of software and hardware.
In the past, verification was performed only on a small core of the software or on a simplified model of the actual software. For reference, AWS’s access-control language, Cedar, had a Rust implementation running in production and a reference implementation—first in Dafny and later in Lean—that was verified for correctness. One approach would be to develop Cedar entirely in Lean, compile to C, and deploy the generated C code in production.
