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 — built toward Dell PowerEdge; gates today run on Latitude + QEMU nested KVM.

View on GitHub Read the architecture

Milestones · July 2026

M0 → M7.2 closed on Latitude.

Software gates close on Dell Latitude + QEMU nested KVM — not yet on PowerEdge R640. Ship kit + network HTTP + datastore closed on Latitude — RAYNU-V-M7-STORE-OK (register/list/delete + ESP-shaped host catalog; UEFI persist still stubbed). Next: ISO deploy — see docs/m7_plan.md. 

RAYNU-V-M7-STORE-OK
==> M7.2 datastore smoke PASSED
host_catalog_persist_roundtrip ... ok

M1.0 → M6: how we got here

A closed gate proves one acceptance property under automation — COM1 markers on nested KVM for boot behavior, or host proof artifacts (cargo test / Verus / Kani smokes) — not that the product is finished, and not that PowerEdge R640 is validated.

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–M3.18 True L3 verify + ghost↔exec refine
  5. M3.19–M3.20 NOIRQ policy + tight EPT [0,512MiB)
  6. M3.21–M3.22 Hard-fail Kani + PE .askern/.asinit embed

M4 · Multi-VM platform

  1. M4.0 Dual VMCS + distinct EPT → RAYNU-V-M4-2VM-OK
  2. M4.1 Credit scheduler G0↔G1 → RAYNU-V-M4-SCHED-OK
  3. M4.2 G0 + G1–G3 (≥4) → RAYNU-V-M4-NVM-OK
  4. M4.3 Virtio-mmio blk probe → RAYNU-V-M4-BLK-OK
  5. M4.4 Virtio-net dual-port vSwitch → RAYNU-V-M4-NET-OK
  6. M4.5 Dual-vCPU BSP+AP shared EPT → RAYNU-V-M4-SMP-OK
  7. M4.6 N-guest ghost exclusivity → RAYNU-V-M4-NGUEST-SPEC-OK
  8. M4.7 N-guest L3 verify (ADR-006) → RAYNU-V-M4-NGUEST-VERIFY-OK
  9. M4.8 Large-page (2M/1G) ghost spec → RAYNU-V-M4-LPAGE-OK
  10. M4.9 N-guest ghost↔exec refine → RAYNU-V-M4-REFINE-OK

M5 · Operationally viable

  1. M5.0 VM lifecycle create/start/stop/destroy → RAYNU-V-M5-LIFE-OK
  2. M5.1 CLI + REST control plane → RAYNU-V-M5-API-OK
  3. M5.2 Embedded Web UI SPA (PE .aswebui) → RAYNU-V-M5-WEBUI-OK
  4. M5.3 Audit ring + hash chain (tamper-evident) → RAYNU-V-M5-AUDIT-OK
  5. M5.4 SOX / ISO-style reports from ring snapshot → RAYNU-V-M5-REPORT-OK
  6. M5.5 One-command OVF/VMDK inventory import (≥10) → RAYNU-V-M5-MIGRATE-OK
  7. M5.6 Dell Tier‑1 mock Redfish + SMBIOS/ACPI topology → RAYNU-V-M5-IDRAC-OK
  8. M5.7 Large-page (2M/1G) L3 verify — no admit → RAYNU-V-M5-LPAGE-VERIFY-OK
  9. M5.8 NUMA ghost spec (SRAT/SLIT) → RAYNU-V-M5-NUMA-OK
  10. M5.9 Allocator↔EPT refine + identity abs → RAYNU-V-M5-ALLOC-REFINE-OK

M6 · Ops + soak + audit (Latitude/QEMU)

Closed on Latitude/QEMU; not a claim of R640 field validation.

  1. M6.0 EPT-violation exclusivity → RAYNU-V-M6-EPTVIO-OK
  2. M6.1 HW PTE bit-decode → RAYNU-V-M6-HWPTE-OK
  3. M6.2 NUMA affinity L3 → RAYNU-V-M6-NUMA-L3-OK
  4. M6.3 Migrate page transfer → RAYNU-V-M6-MIGRATE-XFER-OK
  5. M6.4 REST auth → RAYNU-V-M6-AUTH-OK
  6. M6.5 PDF audit reports → RAYNU-V-M6-PDF-OK
  7. M6.6 HA failover + harden → RAYNU-V-M6-HA-OK
  8. M6.7 Fault injection → RAYNU-V-M6-FAULT-OK
  9. M6.8 72-hr soak → RAYNU-V-M6-SOAK-OK
  10. M6.9 External audit + spec review → RAYNU-V-M6-EXT-OK

M7 · Mount Everest

Software path on Latitude/QEMU; real R640 boot (RAYNU-V-R640-BOOT-OK) is the hard gate for M7 closed.

  1. M7.0 EFI release kit (SHA256 + USB/iDRAC) → RAYNU-V-M7-SHIP-OK
  2. M7.1 Network HTTP mgmt (SPA + Bearer REST) → RAYNU-V-M7-HTTP-OK
  3. M7.2 Datastore / image library → RAYNU-V-M7-STORE-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 is meant to land 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 Target: deploy and attest on PowerEdge you own, via Redfish — not a mystery appliance. R640 first-light is still ahead.
    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 and concrete refine (RAYNU-V-M3-L3-VERIFY-OK / RAYNU-V-M3-L3-REFINE-OK).

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

One binary. One server family.

No host OS. No packages. No config sprawl. Optimized for Dell PowerEdge R640 / R650 / R660. Today’s closed gates are on Latitude + QEMU nested KVM. We ship the EFI kit for PowerEdge; first-light on real R640 is M7.5 — see HDA. 

# Lab: Latitude / QEMU nested KVM · R640 = future hard gate
cargo build --release --target x86_64-unknown-uefi --features uefi-bin
./tools/check-pe-assets.sh      # .askern / .asinit / .aswebui
./tools/qemu-boot-test.sh       # M0 → M4.5
./tools/m5-idrac-smoke.sh       # M5.6 → RAYNU-V-M5-IDRAC-OK
./tools/verus-lpage-verify-smoke.sh # M5.7 → RAYNU-V-M5-LPAGE-VERIFY-OK
./tools/verus-numa-smoke.sh     # M5.8 → RAYNU-V-M5-NUMA-OK
./tools/verus-alloc-refine-smoke.sh # M5.9 → RAYNU-V-M5-ALLOC-REFINE-OK
./tools/verus-eptvio-smoke.sh   # M6.0 → RAYNU-V-M6-EPTVIO-OK
./tools/verus-hwpte-smoke.sh    # M6.1 → RAYNU-V-M6-HWPTE-OK
./tools/verus-numa-l3-smoke.sh  # M6.2 → RAYNU-V-M6-NUMA-L3-OK
./tools/verus-migrate-xfer-smoke.sh # M6.3 → RAYNU-V-M6-MIGRATE-XFER-OK
./tools/m6-auth-smoke.sh       # M6.4 → RAYNU-V-M6-AUTH-OK
./tools/m6-pdf-smoke.sh        # M6.5 → RAYNU-V-M6-PDF-OK
./tools/m6-ha-smoke.sh         # M6.6 → RAYNU-V-M6-HA-OK
./tools/m6-fault-smoke.sh      # M6.7 → RAYNU-V-M6-FAULT-OK
./tools/m6-soak-smoke.sh       # M6.8 → RAYNU-V-M6-SOAK-OK
./tools/m6-ext-smoke.sh        # M6.9 → RAYNU-V-M6-EXT-OK
./tools/package-release.sh     # versioned EFI + SHA256 tarball
./tools/m7-ship-smoke.sh       # M7.0 → RAYNU-V-M7-SHIP-OK
./tools/m7-http-smoke.sh       # M7.1 → RAYNU-V-M7-HTTP-OK
./tools/m7-store-smoke.sh      # M7.2 → RAYNU-V-M7-STORE-OK
./tools/kani-smoke.sh           # hard-fail Kani → RAYNU-V-M3-KANI-OK

Talk to us.

Investors and MSPs evaluating formally verified isolation on Dell PowerEdge — early interest, pilots, or partnership conversations — are welcome to reach out at namaskaar@raynuv.com. M0→M6 is closed on Latitude + QEMU nested KVM — the lab production bar under docs/m6_plan.md (EPT proof track + ops + soak + external audit). PowerEdge R640 validation is still ahead (Mount Everest / HDA).

Email namaskaar@raynuv.com Open the repository