SPARK VirtIO Drivers

A high-assurance, formally verified driver stack for the VirtIO 1.4 specification. Proving safety in the wild world of I/O.

Full support for both Split (Legacy/Modern) and Packed (Modern) virtqueues. Ready for PCI and MMIO transports.

Uses SPARK "Ghost State" to model complex hardware lifecycles and ownership, proving invariants that standard types cannot capture.

Design Philosophy

Unlike typical drivers that panic on hardware misbehavior, this library is designed to be robust.

Malicious Device Model: We assume the device might return invalid indices. The driver defensively validates all inputs.
Zero-Overhead Abstractions: Contracts are erased at compile time, leaving code comparable to optimized C.
Partition Invariant: Mathematically proven prevention of Double-Free and Use-After-Free bugs in buffer management.

Comprehensive support for the standard device types defined in the spec.

Network

Block

GPU

Console

Entropy

Balloon

Input

Socket