High Voltage

Challenge

Formally verifying critical software is notoriously difficult and labor-intensive, often requiring years of expert effort for even a modest codebase. This human bottleneck—compounded by a fragmented toolchain—makes it nearly impossible to scale verification across critical infrastructure, which relies on millions of lines of legacy C code. Consequently, the software underpinning our most vital systems remains largely unverified and vulnerable. 

Solution

Recent breakthroughs in AI auto-formalization signal a paradigm shift: leveraging AI can fundamentally alter the cost-benefit calculus of software verification, compressing timelines from person-years to person-days. We just need to prove that it works at scale. 

HighVoltage is a joint initiative by Galois and Math, Inc., conceived and funded by RAND’s Center for AI, Security and Technology (CAST), to demonstrate that AI-assisted formal verification can tackle real-world critical infrastructure at commercial speed. To learn more about RAND CAST, including information about its funders, visit www.rand.org/cast.

The project will attempt to verify the ~1,200 lines of code in the deployed Linux kernel WireGuard handshake within a compressed timeline that would be infeasible with traditional, manual formal verification processes. 

This stress test offers a win-win outcome, resulting in either: 

1. A Verified Artifact: A machine-checked proof that the implementation satisfies its protocol specification and is memory safe, demonstrating that the AI-assisted approach works on real deployed code. 
2. A Concrete Research Roadmap: Detailed documentation of exactly where current tools, methods, or AI capabilities fall short, providing an actionable blueprint for future breakthroughs.

A verified WireGuard handshake proves the paradigm shift is real and provides a replicable template for the entire industry. A blocker analysis pinpoints exactly what the research community must solve to make infrastructure-scale verification viable. 

How It Works

Our dual-path strategy balances near-term execution with exploration of emerging methods: 

• Direct Certification (DC) aims to demonstrate the capabilities of LLMs when applied to state-of-the-art verification tools. In this path, Galois will verify the Linux kernel WireGuard handshake using the mature VST toolchain in Rocq, producing a machine-checked proof of protocol correctness and memory safety. The goal is to accelerate the field by showing the community that such results are now within reach on deployed infrastructure. 
• Alternative Certification (AC) aims to demonstrate the capabilities of LLMs using emerging verification tools while contributing to their development. In this path, Math, Inc. will pursue the same verification task using Lean. This work is inherently symbiotic: improvements in the Lean tooling enable faster progress, while the demands of this effort provide concrete feedback that drives the evolution and robustness of the underlying verification infrastructure. Success here will spark the formal verification community’s imagination beyond the limits of existing tools. 

By automating the verification of WireGuard, HighVoltage will demonstrate that practical, AI-driven systems verification is possible, establishing a methodology and a new baseline for the entire software industry to follow. 

Value Add

• Commercial-Speed Verification: By leveraging AI auto-formalization agents like Gauss, the project aims to compress the formal verification process from person-years of manual labor into just days or weeks.
• Securing Real-World Infrastructure: The project directly hardens the deployed Linux kernel WireGuard code, which actively secures major VPNs, industrial private 5G, Kubernetes clusters, and SCADA/OT systems.
• Accelerating the Ecosystem: Simultaneously elevates mature, production-grade frameworks (Rocq/VST) while rapidly advancing cutting-edge environments (Lean 4) for real-world code.
• Actionable Industry Roadmap: The effort will either deliver a fully verified artifact as a replicable template for the software industry, or identify precise technical gaps to create a concrete research agenda for the field.