From prototype to peer review: answering @Rhode Brunel Moungondo on Odin OS

Four days ago on my initial post ("I Built an Operating System Because I Don't Trust AI Agents"), Rhode Brunel Moungondo left a comment that stopped me cold.

I had mentioned that my long-term goal is to get this work peer-reviewed and into arXiv.org someday. Rhode didn't sugarcoat it; he gave me the exact audit questions a reviewer would ask:

"For the peer review you are seeking, a claim-to-evidence map would help a reader choose a bounded starting point: the exact property, assumptions and trusted components, then the artifact or test supporting it and what remains outside scope.
Which single claim would you most like an independent reviewer to try to falsify first? In particular, where do you draw the boundary between enforcing an authorized memory access and establishing that the resulting business action is appropriate? Those seem like distinct review questions."

He was dead right. We had an interesting prototype, but we didn't have a falsifiable assurance case. You can't peer-review a vibe.

...so we spent the last four days rebuilding the publication package from scratch.
Here are the direct answers to his two questions, along with the receipts.
---
1. Which single claim should an independent reviewer try to falsify first?
Claim ODIN-C001 (Boundary Fault Isolation) via Protocol PROTO-01.
In early drafts, we wrote that out-of-bounds writes "fault and leave memory unmodified." That was sloppy; it conflated two completely different hardware properties:

• Unauthorized-byte preservation: Under RISC-V PMP in QEMU virt (rv64gc), an unprivileged task cannot flip bits outside its active spatial grant $[G_{\text{base}}, G_{\text{base}} + G_{\text{len}})$. Any out-of-bounds store triggers Cause 7 (mcause = 7, Store Access Fault), and the target bytes remain unmodified. We reproduced this across edge bounds (one byte below, one byte above, unmapped perimeter).
• Transactional store atomicity: Physical silicon is messier. RISC-V Unprivileged ISA §2.6 permits misaligned multi-byte stores to execute non-atomically. A 32-bit store straddling an authorized boundary could commit its lower bytes before the upper bytes trap, unless hardware implements transactional rollback. We separated that out as ODIN-C008 - an open physical-silicon proof obligation, not an invariant we claim today.

If you want to break Odin OS, start with PROTO-01. Try to make an unprivileged store to 0x8002003F or 0x80020060 commit or bypass Cause 7. Break C001 first.

---
2. Where is the boundary between memory access and business appropriateness?
We draw a hard architectural line here.
The microkernel is strictly a Policy Enforcement Point (PEP). It checks cryptographic capability deeds and configures hardware PMP registers. It makes sure an unprivileged task physically cannot touch memory it wasn't leased.

Whether that write makes sense for your business is not the kernel's problem.
We codified that distinction as an Assurance Boundary Axiom (ODIN-C012): hardware spatial authorization does not equal semantic business correctness. If an agent has a valid lease to write to an account balance register and it writes zero, PMP did its job; the agent just made a terrible business decision. That boundary belongs upstream in the Policy Decision Point (PDP) and application schema.

The microkernel guarantees containment; not wisdom.
---
The receipts
Over the last 96 hours we built and published:

1. Public GitHub repo: github.com/nwalker85/odinos (Apache-2.0, CI passing, branch protection on main).
2. Claim-to-Evidence Registry: 14 discrete claims categorized by status - REPRODUCED, MODEL-CHECKED, QUALIFIED, and ASSURANCE BOUNDARY. Exact assumptions and TCB listed for every claim:

github.com/nwalker85/odinos/blob/main/peer-review/CLAIMS_AND_EVIDENCE.md

1. 12 Falsification Protocols: Turn-key reproduction steps and failure criteria for each claim:

github.com/nwalker85/odinos/blob/main/peer-review/FALSIFICATION_PROTOCOLS.md

1. Zenodo Version 2 Archive: Minted under Concept DOI 10.5281/zenodo.23928301 (V2 DOI: 10.5281/zenodo.24044570).

You can clone the repo and run the verification pipeline in one shot:

git clone github.com/nwalker85/odinos.git
cd odinos
python3 tools/verify_release.py

...four days of Z3 solver queries and QEMU trap logs. I don't recommend the sleep schedule.
Ryan Allis pointed out on the last thread that enterprise buyers won't trust agents without proof that hard limits hold when the model hallucinates. Rhode gave us the roadmap to prove it.

If you work on OS kernels, capability systems, or AI safety boundaries: the code is open. Come break it.