RayNu-V

Memory isolation isn’t tested. It’s proved.

A commercially targeted, single-binary Type-1 hypervisor designed for formal verification from day one — Dell PowerEdge first.

View on GitHub Read the architecture

Milestones · July 2026

M3.17: true L3.

First machine-checked exclusivity proof on the frozen Verus pin — 4K single-guest map/unmap, no admit — latched by RAYNU-V-M3-L3-VERIFY-OK. That is ADR-006 L3 for the ghost model; live EptMap stays L2 until refinement. 

RAYNU-V-M3-L3-VERIFY-OK
==> Verus L3-verify smoke PASSED (M3.17)
# cargo verus verify -p ept_model → 13 verified, 0 errors (no admit)

M1.0 → M3.17: how we got here

A closed gate proves one acceptance property under automation — COM1 markers on nested KVM for boot behavior, or host cargo test for verification artifacts — not that the product is finished.

M1 · Root mode

  1. M1.0 ExitBootServices — own the machine after firmware
  2. M1.1 Real VMXON / VMXOFF
  3. M1.2 VMLAUNCH → guest HLT → VMEXIT

M2 · Guest under EPT

  1. M2.0–M2.1 Identity EPT; guest store, loop, HLT
  2. M2.2–M2.3 Exclusive EPT ownership + Proven Core allocator
  3. M2.4–M2.6 IRQ + timer; Verus specs written + bounded Kani

M3 · Unmodified Linux

  1. M3.0–M3.7 I/O through bzImage — synthetic shell, then real kernel
  2. M3.8–M3.9 Real earlyprintk; MSR firewall + GTIMER2
  3. M3.10 Real /init → RAYNU-V-M3-SHELL-OK

Post-shell

  1. M3.11–M3.12 Guest APIC timer + faithful IRR/ISR inject
  2. M3.13–M3.14 Precise EPT; Verus L3 attempt (lemmas drafted)
  3. M3.15–M3.16 Frozen Verus pin + linkable ept_model
  4. M3.17 True L3 verify → RAYNU-V-M3-L3-VERIFY-OK

Four pillars. Every line serves one.

Proof work is the trust product a buyer can take to an auditor; iDRAC is how that story lands on iron you operate; the audit trail turns hypervisor events into compliance evidence — not a slide deck.

  1. [V]
    Formally Verified Core Isolation claims you can machine-check, not re-test every release.
    North star
  2. [Z]
    Zero-Config Single Binary One EFI artifact — smaller surface, clearer attestation target.
    Near-term
  3. [D]
    Dell iDRAC-Native Deploy and attest on PowerEdge you own, via Redfish — not a mystery appliance.
    Near-term
  4. [A]
    Audit-First / FinOps Sequenced events for SOX/ISO evidence and capacity truth — not after-the-fact forensics.
    Medium-term

The invariant we prove

For every valid EPT mapping from guest-physical to host-physical, that frame is exclusively owned by one guest — and belongs to neither the hypervisor nor any other guest.

Proven Core only. Scoped cargo verus --verify on the frozen pin is green for 4K single-guest exclusivity (RAYNU-V-M3-L3-VERIFY-OK) — live EptMap refinement remains ahead.

ADR-002 · ADR-004 · ADR-006 · ADR-008

One binary. One server family.

No host OS. No packages. No config sprawl. Optimized first for Dell PowerEdge R640 / R650 / R660 — hardware we can own and test on. We ship for the iron we verify on. 

cargo build --release --target x86_64-unknown-uefi --features uefi-bin
./tools/qemu-boot-test.sh
./tools/verus-verify-smoke.sh   # true L3 → RAYNU-V-M3-L3-VERIFY-OK

What’s next

Scoped true L3 is closed. Next: refine live EptMap against the ghost model, then keep hardening the real-Linux guest path.

Open the repository EPT isolation ADR