RayNu-V

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

Single-binary Type-1 hypervisor — on real PowerEdge R640: COM2 printed RAYNU-V-R640-BOOT-OK, then the operator LAN reached RAYNU-V-M7-UEFI-HTTP-OK.

View on GitHub Read the architecture

Milestones · August 2026

R640 iron: BOOT-OK through E4 SPA VMLAUNCH.

Real PowerEdge R640 (iDRAC9 SOL console com2) closed HDA E2 — RAYNU-V-R640-BOOT-OK (M0→SHELL→M4, 2026-08-15) — E3 MVP RAYNU-V-M7-UEFI-HTTP-OK (PRE-EBS SNP, 2026-08-16) — E5 stamps RAYNU-V-M7-ISO-BOOTED-FROM-DISK (Cruzer, LBA not a rootfs) — E3b + Phase F RAYNU-V-M7-HOST-NIC-HTTP-OK beside VMX (BCM5720 :38, 2026-08-20) — and P0-14 RAYNU-V-M7-E4-SPA-LAUNCH-OK (2026-08-21: private-EPT SHELL guest from SPA start + shadow re-entry). Mount Everest residual: TLS/console and a real distro installer. Not Everest.

macOS Terminal: iDRAC SOL session ending in RAYNU-V-R640-BOOT-OK
Operator Terminal.app · iDRAC SOL (console com2) — full archive 
boot: mgmt HTTP listening on 10.99.99.127:8443 (PRE-EBS SNP window)
RAYNU-V-AUDIT: AuthAllowed method_tag=1
RAYNU-V-M7-UEFI-HTTP-OK
…
RAYNU-V-R640-BOOT-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) and UEFI HTTP (RAYNU-V-M7-UEFI-HTTP-OK) closed 2026-08-15/16. E5 stamp persist closed on Cruzer (RAYNU-V-M7-ISO-BOOTED-FROM-DISK). Residual: TLS/console + distro installer (E3b + Phase F closed 2026-08-20; E4 SPA VMLAUNCH closed 2026-08-21, SHELL stub).

  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
  4. M7.3 ISO extract-boot deploy (lab host smoke) → RAYNU-V-M7-ISO-OK
  5. M7.4 Ops UI create-VM + media (lab host smoke) → RAYNU-V-M7-UI-OK
  6. M7.5 Real R640 iron closed (SHELL+M4, 2026-08-15) → RAYNU-V-R640-BOOT-OK
  7. M7.8 Native BCM5720 HTTP after BOOT-OK + Phase F coexist (2026-08-20) → RAYNU-V-M7-HOST-NIC-HTTP-OK
  8. E4 SPA private-EPT VMLAUNCH + shadow re-entry (2026-08-21, SHELL stub) → RAYNU-V-M7-E4-SPA-LAUNCH-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 iron closed BOOT-OK (E2), UEFI-HTTP-OK (E3), host-NIC HTTP (E3b), and E4 SPA VMLAUNCH (P0-14, SHELL stub) through 2026-08-21.
    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 plus real R640 iron: RAYNU-V-R640-BOOT-OK (E2), RAYNU-V-M7-UEFI-HTTP-OK (E3 MVP), RAYNU-V-M7-ISO-BOOTED-FROM-DISK (E5 stamps), and RAYNU-V-M7-HOST-NIC-HTTP-OK (E3b + Phase F, 2026-08-20), and RAYNU-V-M7-E4-SPA-LAUNCH-OK (P0-14, 2026-08-21, SHELL stub). Mount Everest residual: TLS/console + distro installer. See HDA. 

# Lab: Latitude / QEMU · R640 iron: E2 BOOT-OK + E3 UEFI-HTTP-OK + E5 stamps
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/m7-iso-smoke.sh        # M7.3 → RAYNU-V-M7-ISO-OK
./tools/m7-ui-smoke.sh         # M7.4 → RAYNU-V-M7-UI-OK
./tools/m7-r640-smoke.sh       # M7.5 scaffold → RAYNU-V-M7-R640-SCAFFOLD-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 iron closed RAYNU-V-R640-BOOT-OK and RAYNU-V-M7-UEFI-HTTP-OK (2026-08-15/16) and Cruzer stamp persist RAYNU-V-M7-ISO-BOOTED-FROM-DISK and durable HTTP RAYNU-V-M7-HOST-NIC-HTTP-OK (2026-08-20) and E4 SPA VMLAUNCH RAYNU-V-M7-E4-SPA-LAUNCH-OK (2026-08-21, SHELL stub); Mount Everest residual is TLS/console and a real distro installer. See the living verification paper.

Email namaskaar@raynuv.com Open the repository