u/Impossible-Wrap5968

Hey r/rust,

I've been working on a weird experiment that sits at an unusual intersection: rust-vmm, formal verification (Kani), and LLM agents. I wanted to share it here because the Rust-specific architecture and the low-level KVM plumbing ended up being the most interesting parts of the project.

The TL;DR of how it works You type: ai-vmm run "create a VM with 2 vCPUs and 2 GiB RAM named db" An LLM generates a structured plan. You review it, and on y, the Rust control plane provisions and boots a real Linux kernel natively via kvm-ioctls and vm-memory. There is no Firecracker or QEMU under the hood—it's speaking directly to KVM.

The architecture & Rust highlights:

• Trust boundaries as types: The model produces a Spec struct which is treated as completely untrusted input. Every single field goes through a strict validate_spec before it ever touches a KVM ioctl. The LLM is allowed to parse intent, but it is structurally prevented from setting out-of-bound resources.
• Formal verification with Kani: Resource limits (vCPU count, memory size bounds, TAP name injection prevention) aren't just unit-tested, they are mathematically proven by Kani. cargo kani runs in CI alongside cargo test. This was my first serious use of Kani's bounded model checking, and the proofs run in seconds. I highly recommend it for any crate where invalid input is a security boundary.
• Manual KVM plumbing: Doing this from scratch meant writing an Intel MP table directly into guest memory by hand to bring up multiple vCPUs, and hand-writing a virtio-blk MMIO device for the rootfs. The vmm/ module is probably the part of the codebase most people here would enjoy reading.
• axum control plane: ai-vmm serve exposes a small REST API (with constant-time bearer auth comparison) and spawns each VM as its own supervised worker process.

A few things I learned: vm-memory's GuestAddress / GuestMemoryMmap abstraction is an absolute joy once you accept that the guest is just an mmap that your code owns. Also, kvm-ioctls is actually much thinner than I expected. The hard part of building a hypervisor isn't KVM itself; it's everything around it (IRQ routing, the MP table, the console).

Limitations (Obviously) This is an experiment, so it has strict limits:

• Actual provisioning requires native Linux/KVM or WSL2 (though the codebase compiles cleanly on Windows/macOS).
• One VM at a time in the foreground.
• TAP networking plumbing exists and is verified, but in-guest NIC attachment isn't fully wired up yet.

Repo:https://github.com/SO2304/ai-vmm

I'd love to hear your thoughts, especially if anyone here has messed with Kani formal verification or manual MP table construction before!