RayNu-V

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

Single-binary Type-1 hypervisor. Mount Everest is closed. On the same PowerEdge, an Ubuntu ISO on the PERC spare installed and logged in.

View on GitHub Read the architecture

Everest closed, then Ubuntu on the spare: c3a70e62 · initrd.img-7.0.0-14-generic · vikkp@raynusrv2:~$

Milestones · October 2026

Ubuntu logged in from the PERC spare.

Guests stored ubuntu-26.04-live-server-amd64.iso on RAYNU-SPARE, the large RAID virtual disk of the lab H740P. Start on the 10 GiB tail installed it. EFI c3a70e62 then booted that disk: RayNu-F copied initrd.img-7.0.0-14-generic (34,338,680 bytes), Linux 7.0.0-14-generic came up with root ubuntu--vg-ubuntu--lv, and the serial console reached vikkp@raynusrv2:~$. vda is 10 GiB (vda1 vda2 vda3). Clear ISO then printed boot: M8.8 library ISO cleared — the signature sector only. UBUNTU0 and the Ubuntu disk stayed. Mount Everest, the Alpine install loop of 11 September, stays closed on f72b4276. Next is M8.9, in the same kind of stages as M8.8. M8.9.1 keeps a NIC record on the spare and does not attach one. This shell still has no network. The 2.9 TB virtual disk is not this 10 GiB tail. Auth is still open. Summit rollback remains v0.1.0-everest-closed.

macOS Terminal: iDRAC SOL session ending in RAYNU-V-R640-BOOT-OK
Operator Terminal.app · iDRAC SOL (console com2) — first iron close RAYNU-V-R640-BOOT-OK (2026-08-15). Summit COM2: ISO-INSTALL-OK → DISK-BOOT-OK → login. 
HOST-NIC coexist listening on 10.99.99.145:8443
RAYNU-V-M7-HOST-NIC-HTTP-OK
boot: E4 SPA start — RayNu-F product ISO
RAYNU-V-M7-ISO-INSTALL-OK
RAYNU-V-RAYNU-F-DISK-BOOT-OK
root=UUID=814a97a0-d3be-4a64-8611-b3dbd9859201
localhost login:
build: sha=c3a70e623aec
boot: RayNu-F initrd ext4 bytes=34338680 name=initrd.img-7.0.0-14-generic
Linux version 7.0.0-14-generic
virtio_blk virtio0: [vda] 20971520 512-byte logical blocks (10.0 GiB)
Welcome to Ubuntu 26.04 LTS!
vikkp@raynusrv2:~$
boot: M8.8 library ISO cleared (signature sector only; disks unchanged)
For infrastructure leaders Your PowerEdge fleet has years left. License economics, isolation assurance, and what a reversible design partnership looks like — the executive view. CIO View → For engineers Every claim has a marker. Dozens of closed gates, Verus proof transcripts, and serial logs from real iron — the evidence, end to end. The journey ↓

M1.0 through the spare

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.

Gates closed · M1.0 → Everest
55+
Verus proofs · M6.9 external audit
80 verified · 0 errors
Mount Everest · real PowerEdge R640
closed

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

Closed on iron 2026-09-11. Real R640 boot (RAYNU-V-R640-BOOT-OK), durable HTTP (RAYNU-V-M7-HOST-NIC-HTTP-OK), SPA Start of RayNu-F, Alpine ISO install (RAYNU-V-M7-ISO-INSTALL-OK), reboot to disk (RAYNU-V-RAYNU-F-DISK-BOOT-OK). The summit stays closed. M8, below, is the work after it.

  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
  9. E5 Guest-UEFI OVMF past SEC + CD/virtio-blk on private VMCS (nested VT-x, 2026-08-23) → RAYNU-V-M7-E5-OVMF-VIRTIO-OK
  10. E5 · 44 Guest firmware reads the CD — ATAPI READ(10), sectors=1, on iron (2026-08-27) → RAYNU-V-M7-E5-OVMF-ATAPI-OK
  11. E5 · 45 El Torito CD EFI on iron — catalog + boot image (2026-08-27) → RAYNU-V-M7-E5-OVMF-ELTORITO-OK
  12. E5 · 46 Nested RayNu-F alpine-extended sys-install complete (2026-09-05, Please reboot + F7). Nested ≠ iron. Iron close is the Everest row below → RAYNU-V-RAYNU-F-DISK-BOOT-OK
  13. Everest SPA Start of RayNu-F on coexist HTTP (f72b4276, 2026-09-11) — M7 closed on iron → RAYNU-V-M7-ISO-INSTALL-OK

M8 · after the summit

Same R640. TLS and a standing SPA came first. M8.8 then put an Ubuntu ISO on the PERC spare, installed it, and logged in. Next is M8.9. M8.9.1 is the spare NIC record. The guest still has no NIC.

  1. M8.1 HTTPS on the host NIC before the guest → RAYNU-V-M8-TLS-OK
  2. M8.7 PERC spare read, write, then a guest login from the 8 GiB window → RAYNU-V-M8-PERC-BOOT-OK
  3. Guests 10 GiB tail ee851fd5 booted (f44ba647). Slice 3 on 752586b9 withheld setup-disk.
  4. M8.8 Ubuntu 26.04 from the library ISO on the spare, then vikkp@raynusrv2:~$ and Clear ISO (c3a70e62). Guest NIC is next.

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), E4 SPA VMLAUNCH, El Torito CD EFI, and Mount Everest (ISO-INSTALL-OK + DISK-BOOT-OK, 2026-09-11). After that, Ubuntu 26.04 logged in from a 10 GiB tail of the PERC spare.
    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

The product · management UI

The console ships inside the binary.

The management SPA is embedded in the .efi as a compressed PE asset (.aswebui) and served from the host NIC — VM list, create-VM, ISO attach, and the audit tail. Shown here with the bundled demo state; on R640 iron it answers after BOOT-OK on the host-owned BCM5720 (E3b, 2026-08-20), even while guests run (Phase F).

RayNu-V management Web UI: two shell-ready VMs in the list, Create Virtual Machine form, and the audit log tail
Management SPA · demo-state bundle · served from the host-owned NIC after BOOT-OK (E3b closed 2026-08-20)

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 through Mount Everest: RAYNU-V-R640-BOOT-OK (E2), RAYNU-V-M7-HOST-NIC-HTTP-OK (E3b), RAYNU-V-M7-ISO-INSTALL-OK + RAYNU-V-RAYNU-F-DISK-BOOT-OK (E5 + Phase B, 2026-09-11). M8 TLS and USB persist are closed on COM2. Ubuntu 26.04 then logged in from a 10 GiB PERC tail. Next is M8.9. M8.9.1 is the spare NIC record. Auth is still open. See HDA and LOI. 

# 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

Field notes · friendship

Making buddies along the way.

Our best bud is Mr. COM2 Serial Port. He works at 115,200 bits per second, never lies, never sleeps, and tells us everything — every trap, every timer tick, every time the firmware throws a chair. He was there for first light on the R640, he was there for the red screen, and he prints the markers this site is named after. We transcribed one full conversation with him on real iron and annotated every beat.

Have a chat with COM2 The raw transcript

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) and Stage 44/45 OVMF-ATAPI-OK / OVMF-ELTORITO-OK (2026-08-27); and the full ISO install loop RAYNU-V-M7-ISO-INSTALL-OK / RAYNU-V-RAYNU-F-DISK-BOOT-OK (2026-09-11). Mount Everest is closed. Since then an Ubuntu ISO on the PERC spare reached vikkp@raynusrv2:~$. A virtual guest NIC is next. See the LOI tracker and the living verification paper.

Email namaskaar@raynuv.com Open the repository