Skip to content

MEP-41 Research Substrate: Memory Safety Advances 2023–May 2026

MEP-41 Research Substrate: Memory Safety Advances 2023–May 2026

memory-safety overview

A literature/systems review across 12 threads, with concrete adaptation notes for the vm3 handle/arena/generation model. Each topic includes canonical name + venue/year, core mechanism, production status, and a Mochi adaptation hook.

This file is the broad overview produced by the parallel research sweep. Per-system deep-dive files live alongside it in:

  • hardware/ — CHERI, Morello, CHERIoT, MTE, MIE, PAC/BTI, CET, MarkUs, Scudo, LAM.
  • ownership/ — Rust+Polonius, Vale, Hylo, Mojo, Austral, Pony, Verona, Swift, OxCaml, Linear Haskell, Scala 3, Inko.
  • runtime/ — Perceus, Roc, Lobster, ZGC, MMTk LXR, JSC Riptide, V8 Oilpan, V8 Sandbox, MSWasm, Wasm segmented memory, WasmGC, V8 cage, W^X / JIT hardening, Spectre/JIT, Scudo-in-ART.
  • verification/ — RustBelt/Iris, Verus, Creusot, Kani, Aeneas, CompCert, CakeML, Stacked/Tree Borrows, separation logic for managed heaps, capability-machine logics.
  • industry/ — MSRC 70%, Google/Android Rust, CISA Secure-by-Design (Jan 2026 deadline), NSA, ONCD, DoD, EU CRA, Chrome CVE data, curl, UAF landscape.

§1. Hardware Capability Machines (CHERI / Morello / CHERIoT / Codasip)

Arm Morello (2022 prototype, still research as of 2025). Morello is Arm’s 7nm Neoverse-N1-derived prototype board implementing CHERI 128-bit capabilities (address + bounds + permissions + 1 tag bit out-of-band). Arm has publicly stated there is no roadmap to include Morello in any commercial Arm product; the boards are distributed via the CHERI Alliance and the UK Digital Security by Design programme. Active research continues: PLDI 2025 published “Morello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware Architecture” (a full-scale sequential model of the Morello ISA showing robust encapsulation even in the presence of arbitrary untrusted code). URLs: https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/cheri-morello.html , https://pldi25.sigplan.org/details/pldi-2025-papers/80/Morello-Cerise , https://ctsrd-cheri.github.io/morello-early-performance-results/introduction/index.html

CHERIoT (Microsoft Research, now multi-company). Embedded RISC-V variant providing object-granularity spatial safety, deterministic use-after-free, and lightweight compartments at <256KiB SRAM. CHERIoT 1.0 specification was released November 3, 2025; the SOSP'25 paper “CHERIoT RTOS: An OS for Fine-Grained Memory-Safe Compartments on Low-Cost Embedded Devices” describes a co-designed OS where compartmentalization and memory safety are first-class. Sonata boards ship from Mouser. URLs: https://cheriot.org/sail/specification/release/2025/11/03/cheriot-1.0.html , https://github.com/microsoft/cheriot-rtos , https://www.microsoft.com/en-us/research/publication/cheriot-rtos-an-os-for-fine-grained-memory-safe-compartments-on-low-cost-embedded-devices/

Codasip CHERI-RISC-V — first commercial silicon path. April 2025: Codasip Prime + X730 64-bit RISC-V CHERI application CPU shipped on FPGA. November 19, 2025: Codasip licensed its 700-family CHERI-enabled CPU to EnSilica for a quantum-resilient COTS microcontroller, the first announced mass-distribution CHERI-RISC-V part. URLs: https://codasip.com/press-release/2025/04/29/codasip-prime-launch/ , https://codasip.com/press-release/2025/11/19/codasip-ensilica-for-cheri-enabled-cpu/

What CHERI enforces that vm3 can mimic: unforgeable references (no integer→pointer cast), spatial bounds, permissions (read/write/execute/load-capability) carried with the reference, and revocation via tags that survive memory reuse.

Mochi adaptation: vm3’s 8-byte handle is already a CHERI-style fat pointer in spirit. Allocate spare bits in the handle for permission flags (read/write, frozen, sealed-for-FFI), and treat handle integrity as an invariant the bytecode verifier enforces. The verifier should refuse any instruction that synthesizes a Cell from raw bytes. Sealing (CHERIoT-style “sealed capabilities” usable only by a designated compartment) maps directly to FFI: when handing a handle to a Go library, swap its tag for a sealed variant that only the matching unseal opcode can re-open.

§2. Arm Memory Tagging Extension (MTE) and Apple MIE

Arm MTE basics (Armv8.5). Each 16-byte memory granule carries a 4-bit hardware tag; pointers carry a 4-bit “key” in their top byte; loads/stores fault on mismatch. SYNC mode is precise; ASYNC and asymmetric modes trade precision for throughput. Tag-collision probability is 1/16 per access. URL: https://developer.android.com/ndk/guides/arm-mte

Pixel 8/9 deployment (2023–2025). Pixel 8 is the first phone with user-toggleable MTE in Developer Options; Android 13+ supports the feature. Real exploits against MTE-enabled kernels have been demonstrated (CVE-2023-6241 on Mali GPUs, CVE-2025-0072 fixed in r54p0 May 2025, both relied on driver-side bypasses outside the MTE perimeter). URLs: https://source.android.com/docs/security/test/memory-safety/arm-mte , https://github.blog/security/vulnerability-research/bypassing-mte-with-cve-2025-0072/

Apple Memory Integrity Enforcement (MIE), iPhone 17 / A19, Sept 9 2025. The single largest deployment milestone. MIE = Enhanced MTE (EMTE, ratified with Arm in 2022) + secure typed allocators (kalloc_type from iOS 15, xzone malloc from iOS 17) + Tag Confidentiality Enforcement (an explicit defense against Spectre-style tag leakage). Runs in synchronous mode kernel-wide and across 70+ userland processes, always-on, not user-toggleable. Apple credits it with breaking essentially every recent mercenary-spyware exploit chain. URL: https://security.apple.com/blog/memory-integrity-enforcement/

Mochi adaptation: MIE’s three pillars correspond beautifully to vm3. The 12-bit generation in vm3’s handle is already a software-MTE “key”; the slot’s stored generation is the “tag.” Tag Confidentiality Enforcement is the lesson worth stealing: never let user code observe a raw generation number (or compute differences between them), because generation churn becomes a side channel that lets an attacker race a stale handle. Treat generation values as opaque, attacker-unobservable secrets, only the runtime can compare them. Pair this with a typed allocator (one arena per Mochi type, like kalloc_type/xzone) so that even a generation collision can’t land on a type-confused slot.

§3. Rust-family Ownership and Borrowing

Polonius “Alpha” (Rust 2025h2 goal, stabilization targeted 2026). Switches from NLL’s “lifetimes as sets of points” to “origins as sets of loans.” Accepts a superset of NLL (closes NLL problem case #3, enables lending iterators) at a budgeted 10–20% compile-time cost. Currently passes nearly all in-tree tests and crater runs; final blocker is one known soundness issue and diagnostics. URLs: https://rust-lang.github.io/rust-project-goals/2025h2/polonius.html , https://rust-lang.github.io/rust-project-goals/2026/polonius.html , https://github.com/rust-lang/polonius

Vale (most directly relevant to vm3). Vale invented generational references: every object stores a “current generation” int that is bumped on free; every reference remembers the target generation; dereference inserts a runtime check ref.gen == obj.gen. This is mathematically the same thing vm3 already does. Vale’s roadmap layers two optimizations on top: (a) Region Borrow Checking, a Rust-like checker that proves a region of objects can’t be freed during a scope, eliding the gen-check; (b) Hybrid-Generational Memory, “scope tethering” that pins an object’s generation across a known-live scope and uses static analysis to elide the rest. Vale also exposes Fearless FFI: because generations aren’t refcounts, handing a reference to a C function can’t corrupt your memory model. URLs: https://verdagon.dev/blog/generational-references , https://vale.dev/vision/safety-generational-references , https://vale.dev/roadmap , https://verdagon.dev/blog/zero-cost-memory-safety-regions-part-1-immutable-borrowing

Hylo (formerly Val). “Mutable value semantics.” The interesting mechanism is subscripts, a callable that projects (yields) a reference into a containing value rather than returning it. Variants: let, inout, sink, set. Calls are bracket-syntax (a[i]) and the projection is mutability-tracked through the callsite. Hylo had a major design talk “Designing Hylo” at ECOOP/PLSS 2025. URLs: https://hylo-lang.org/ , https://docs.hylo-lang.org/language-tour/subscripts , https://2025.ecoop.org/details/plss-2025-papers/12/Designing-Hylo-a-programming-language-for-safe-systems-programming

Mojo (2024–2026). Argument conventions are read (immutable ref), mut (mutable ref), var (owned, used with ^ transfer). Lifetimes are tracked as compiler-internal origins with ImmutOrigin/MutOrigin/MutExternalOrigin (for FFI memory not managed by Mojo)/MutAnyOrigin (escape hatch that disables ASAP destruction). Uses ASAP destruction (after every sub-expression). Path to Mojo 1.0 published Dec 5 2025; targeting late northern summer 2026. URLs: https://docs.modular.com/mojo/manual/values/ownership/ , https://docs.modular.com/mojo/manual/values/lifetimes/

Austral. Pure linear types (not affine, unlike Rust) + capability-based effects. The linear checker is ~600 lines of OCaml. Functions take an explicit capability argument (e.g., RootCap) and cannot perform an effect (alloc, I/O) without it; capabilities are linear themselves, so the call graph statically tracks who can do what. URLs: https://austral-lang.org/ , https://borretti.me/article/introducing-austral , https://borretti.me/article/how-australs-linear-type-checker-works

Mochi adaptation: Vale is the most important reference for MEP-41. vm3 should explicitly position itself as “Vale’s generational references, but as a VM rather than a static compiler.” Borrow two ideas: (1) region borrowing, if a function statically owns the only reference path into an arena slab during its execution, the verifier can elide gen-checks for that scope; (2) scope tethering, when a handle is held in a stack-local slot, the runtime can pin its generation for the duration of the frame, turning each subsequent deref into a no-op. The Polonius “origins as sets of loans” framing is a cleaner mental model than NLL for documenting MEP-41’s borrow rules.

§4. Capability-Based Reference Systems for Managed Runtimes (Pony, Verona, Inko)

Pony reference capabilities. Six caps, each a pair of local and global aliasing guarantees: iso (unique, sendable), trn (write-unique locally, has read-only aliases), ref (default mutable, actor-local), val (immutable, sendable), box (read-only, may have mutable aliases locally), tag (identity-only, sendable). recover blocks let you upgrade between caps when the source restrictions are met. Only iso, val, tag are sendable across actors, the entire data-race-freedom proof falls out of this matrix. URLs: https://tutorial.ponylang.io/reference-capabilities/reference-capabilities.html , https://tutorial.ponylang.io/reference-capabilities/capability-matrix.html

Project Verona (Microsoft Research), extremely active 2024–2025. Memory is divided into regions, each reachable through a single iso sentinel. Concurrent access is mediated by cowns (concurrent owners) acquired atomically by behaviours (the unit of scheduled work), Behaviour-Oriented Concurrency. Key 2024–2025 papers: “Reference Capabilities for Flexible Memory Management” (OOPSLA 2024), “When Concurrency Matters: Behaviour-Oriented Concurrency” (OOPSLA 2024), “Dynamic Region Ownership for Concurrency Safety” (PLDI 2025, co-authored with Guido van Rossum / Brandt Bucher / Eric Snow, strongly suggesting CPython collaboration on free-threading). The Verona runtime (verona-rt) outperforms actor-based models in 17/22 Savina benchmarks. URLs: https://microsoft.github.io/verona/publications.html , https://github.com/microsoft/verona-rt

Inko. Single-ownership + lightweight runtime reference counting, no GC, no compile-time borrow checker. Inspired by the “Ownership You Can Count On” paper. Mixes the ergonomic feel of Swift refcounting with move semantics; if you use a stale reference, you get a deterministic runtime panic, not undefined behavior. URLs: https://inko-lang.org/ , https://inko-lang.org/papers/ownership.pdf

Mochi adaptation: Pony’s six-capability matrix is overkill for a single-threaded VM, but the encoding (each capability = pair of local/global guarantees) is the right way to document Mochi’s reference rules in MEP-41. For Mochi’s eventual concurrency story, Verona’s region+cown+behaviour model is a better fit than the actor model, it lets you transfer a region of handles (an arena slab) atomically without breaking the generation invariant within. Inko’s lesson is the most pragmatic: if your runtime can detect stale-reference use and panic deterministically, you do not need static linearity to claim memory safety.

§5. Move-Only and Uniqueness in Mainstream Languages

Swift (borrowing/consuming/inout, ~Copyable). SE-0377 added the keywords; SE-0390 made ~Copyable types real (Swift 5.9, late 2023). WWDC24’s SE-0432 added borrowing/consuming pattern matching on noncopyable enums, the missing piece for switch on linear sum types. URLs: https://github.com/swiftlang/swift-evolution/blob/main/proposals/0377-parameter-ownership-modifiers.md , https://github.com/swiftlang/swift-evolution/blob/main/proposals/0432-noncopyable-switch.md , https://developer.apple.com/videos/play/wwdc2024/10170/

OCaml 5 + OxCaml modes (Jane Street, going public 2025). Jane Street’s OxCaml branch (open-sourced July 2025) ships a modal type system with axes: locality (local/global, in production at JS for >1 year), uniqueness (recently merged into the compiler), linearity, yielding (controls whether a callee can perform effects up-stack), and a planned sync axis. The uniqueness mode + a future “overwrite on unique” optimization will give OCaml in-place updates without an unsafe escape hatch. Jane Street’s production servers run OCaml 5 (announced at ICFP/SPLASH 2025). URLs: https://oxcaml.org/documentation/modes/intro/ , https://blog.janestreet.com/oxidizing-ocaml-parallelism/ , https://blog.janestreet.com/oxidizing-ocaml-ownership/ , https://blog.janestreet.com/oxidizing-ocaml-locality/ , https://anil.recoil.org/notes/icfp25-ocaml5-js-docker

Scala 3 capture checking (“Caprese”, Odersky). Capture sets are first-class types T^{cap1, cap2}. Significantly improved in Scala 3.8 (RC3 used in Scala Days 2025 demos); the Scala 3 compiler itself now passes capture checking (PR #16292). Notable 2026 application: “OPAW: Tracking Capabilities for Safer Agents” uses Scala 3 capture checking as a type-level sandbox for LLM-generated tool calls. URLs: https://github.com/scala/scala3/pull/16292 , https://scaladays.org/editions/2025/talks/the-first-steps-towards-practical , https://scaladays.org/editions/2025/talks/hands-on-capture-checking , https://blog.georgovassilis.com/2026/03/13/opaw-tracking-capabilities-for-safer-agents/

Linear Haskell (GHC). Linearity attached to the arrow (%1 ->) rather than to types. Multiplicity polymorphism lets a single library work for both linear and unrestricted callers. Still marked experimental in GHC 9.x, but Bartosz Milewski (Feb 2024) and POPL 2025’s “Affect: An Affine Type and Effect System” show continued momentum. URLs: https://simon.peytonjones.org/linear-haskell/ , https://bartoszmilewski.com/2024/02/07/linear-lenses-in-haskell/ , https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/linear_types.html

Mochi adaptation: OxCaml’s modes-as-orthogonal-axes is the cleanest way to layer optional restrictions on top of vm3 without forking the type system. Mochi could ship a “default” mode where every handle is freely copyable (the current world), and opt-in modes unique (single owner, enables in-place arena update) and local (cannot escape the current call frame, enables scope-tethered gen-check elision). Each mode is purely a verifier check; the bytecode is unchanged. Swift’s borrowing/consuming/inout vocabulary will be familiar to Mochi users and worth reusing verbatim.

§6. Static Analysis / Region Inference / RC-with-Reuse (Koka, Roc, Lobster)

Koka + Perceus + FBIP. Perceus is precise (garbage-free) compile-time-inserted reference counting with reuse analysis: pattern-matching deconstruction immediately reuses the freed cell for the next allocation, turning purely functional map into in-place mutation when the input is unique. Recent papers: “Frame-limited reuse in Perceus,” the “Fully In-Place (FIP) Calculus” (provably no allocation, constant stack), and “Tail Recursion Modulo Context: An equational approach” (Leijen and Lorenzen, JFP October 2025) which extends TRMC to nonlinear control (effect handlers / shift-reset). ICFP'25 distinguished paper: “First-order Laziness” by Lorenzen et al. Koka v3.1.3 released July 2025. URLs: https://dl.acm.org/doi/10.1145/3453483.3454032 , https://www.microsoft.com/en-us/research/publication/perceus-garbage-free-reference-counting-with-reuse/ , https://koka-lang.github.io/koka/doc/book.html

Roc. Compile-time reference counting derived from Perceus, with “Reference Counting with Reuse in Roc” (Folkertsma, Utrecht University thesis) and “Reference Counting with Frame-Limited Reuse.” Cycles are prohibited by language design (no direct mutation). Roc is rewriting its compiler in Zig as of early 2025; still pre-1.0 (alpha4, Aug 2024). URLs: https://studenttheses.uu.nl/bitstream/handle/20.500.12932/44634/Reference_Counting_with_Reuse_in_Roc.pdf , https://www.roc-lang.org/functional

Mochi adaptation: vm3 is handle-indexed and mark-sweep, but the Perceus reuse insight transfers: when the verifier knows a slot is dead after this instruction and the next allocation has the same type/size, emit a single SUPER-op freeAndAlloc that flips the generation, leaves the slab pointer alone, and returns the same handle index. This is reuse without RC, paid for at JIT time. The “Fully In-Place” calculus from Lorenzen/Leijen is the right academic anchor for proving that Mochi pattern-matches can reuse arena slots safely.

§7. Sandboxed Memory for Runtime Extensions

MSWasm (POPL 2023; OOPSLA 2024 follow-up). Extends Wasm with a segment memory distinct from linear memory, accessible only via unforgeable handle values (base, offset, bound, valid bit, id). Tagged-byte storage in segment memory prevents handle forgery from numeric writes. Compilers: rWasm (AOT), mswasm-graal (JIT on GraalVM), mswasm-llvm (CHERI-LLVM fork). Software overhead 22% (spatial only) to 198% (full); hardware MTE/CHERI brings this near zero. Iris-MSWasm (SPLASH/OOPSLA 2024) gave a full Coq mechanization of MSWasm 1.0 and a separation-logic proof of robust capability safety. URLs: https://cseweb.ucsd.edu/~dstefan/pubs/michael:2023:mswasm.pdf , https://github.com/PLSysSec/ms-wasm , https://dl.acm.org/doi/10.1145/3689722

V8 Sandbox / Heap Sandbox. Software-only intra-process isolation: all pointers within the V8 heap are replaced by 32-bit offsets (enabled by pointer compression) or by indices into out-of-sandbox pointer tables. Trusted Space (bytecode containers, JIT metadata) lives outside the sandbox behind a second indirection. Code Pointer Sandbox replaces direct code pointers with an index into a code-pointer table. Started rolling into Chrome 103 (sandboxed pointers); fully default in 2024. Real-world overhead ~1%; 2025 exploitation now requires a sandbox-escape primitive on top of the original UAF/OOB, the bar is dramatically higher. URLs: https://v8.dev/blog/sandbox , https://v8.dev/blog/pointer-compression , https://chromium.googlesource.com/v8/v8.git/+/refs/heads/main/src/sandbox/README.md , https://saelo.github.io/presentations/offensivecon_24_the_v8_heap_sandbox.pdf

RLBox (Firefox). Compile C library to Wasm, then wasm2c back to native C, fed through Clang. Memory isolation enforced by the Wasm sandbox; cross-boundary calls go through invoke_sandbox_function(); all return values and callback parameters are tainted (a compile-time tag the consuming code must explicitly sanitize). Ships in Firefox 95+ isolating Graphite, Hunspell, Ogg, Expat, Woff2. Still in active use in 2025; Mozilla pays bug bounties for sandbox bypasses even without a vulnerability in the isolated library. URLs: https://rlbox.dev/ , https://hacks.mozilla.org/2021/12/webassembly-and-back-again-fine-grained-sandboxing-in-firefox-95/ , https://www.usenix.org/system/files/sec20-narayan.pdf

Mochi adaptation: MSWasm is the closest existing standard to what vm3 already is, a handle-indexed segment memory with tagged forgery prevention. The MEP-41 spec should explicitly cite MSWasm and adopt its handle field layout (base, offset, bound, valid, id) as the normative description of a Mochi cell, with Iris-MSWasm as the formal model to point at. From V8’s sandbox, steal the trusted-space idea: vm3 metadata (function tables, type descriptors, JIT’d code) should live in a separate arena that user code’s handles physically cannot index into, even with a forged generation. RLBox’s taint type is the right pattern for Go FFI returns: any Go-returned value that re-enters Mochi must carry a static “untrusted” mark that forces sanitization before it can be stored in a typed slot.

§8. GC and Lifetime Advances for VMs

ZGC (Generational, default in Java 25). Sub-millisecond stop-the-world pause times via colored pointers + load/store barriers, now generational since JEP 439 (JDK 21). Java 25 ships Generational ZGC as the only ZGC flavor. Netflix runs >50% of critical streaming services on JDK 21 + Generational ZGC; pause times 20–30µs better than non-generational at P99; 4× throughput on Cassandra at 25% the heap. Trade-off: no compressed oops (15–30% memory overhead vs G1) and 5–10% extra CPU. URLs: https://openjdk.org/jeps/439 , https://wiki.openjdk.org/spaces/zgc/pages/34668579/Main , https://netflixtechblog.com/bending-pause-times-to-your-will-with-generational-zgc-256629c9386b , https://andrewbaker.ninja/2025/12/03/deep-dive-pauseless-garbage-collection-in-java-25/

MMTk + LXR. MMTk is a host-language-agnostic Rust GC toolkit; LXR is its hybrid RC+SATB-tracing collector with temporal coarsening (amortizes RC over many writes), 2-bit RC slots (stuck objects fall back to SATB), and synchronous-increment + async-decrement pauses. Stop-the-world LXR beats industrial concurrent GCs on tail latency (PLDI'22 result, increasingly cited). 2024–2025 adoption: Ruby 3.4 ships MMTk integration (currently only MarkSweep; Immix and LXR planned); Julia integrating MMTk (JuliaCon 2025). URLs: https://danglingpointers.substack.com/p/low-latency-high-throughput-garbage , https://www.mmtk.io/status , https://railsatscale.com/2025-01-08-new-for-ruby-3-4-modular-garbage-collectors-and-mmtk/ , https://railsatscale.com/2025-09-16-reworking-memory-management-in-cruby/paper.pdf

JavaScriptCore Riptide. Retreating-wavefront concurrent collector with space-time scheduler that throttles the mutator if allocation outpaces collection. Mostly-concurrent, generational via sticky mark bits, non-compacting, segregated storage. Foundational design from 2017 remains the architecture in 2025. URLs: https://webkit.org/blog/7122/introducing-riptide-webkits-retreating-wavefront-concurrent-garbage-collector/ , https://webkit.org/blog/12967/understanding-gc-in-jsc-from-scratch/

Static Hermes / Hermes V1 (React Native 0.82, 2025). Two LLVM backends: bytecode and native. Optional sound type annotations compile to direct field access on typed classes (shape-aware). React Native 0.82 makes Hermes V1 experimentally available; “static” optimizations (typed compilation, JIT) still ramping. AArch64 JIT shipped 2024 (template-interpreter style). URLs: https://github.com/facebook/hermes , https://speakerdeck.com/tmikov2023/optimizing-with-static-hermes-chain-react-2024 , https://blog.swmansion.com/welcoming-the-next-generation-of-hermes-67ab5679e184

WasmGC. Baseline in all browsers as of late 2024 (Chrome 119, Firefox 120, Safari 18.2). Part of Wasm 3.0 (September 2025). Real production: Google Sheets calculation worker runs 2× faster than JS via WasmGC. Kotlin/Wasm and Dart/Flutter are early adopters. .NET passed because the GC integration is too tight to their runtime. Toolchain limitation: LLVM does not target WasmGC. URLs: https://developer.chrome.com/blog/wasmgc , https://web.dev/blog/wasmgc-wasm-tail-call-optimizations-baseline , https://v8.dev/blog/wasm-gc-porting

Java Valhalla / JEP 401 (Value Classes and Objects). Early-access build of JEP 401 released October 2025; value class removes identity. Two optimizations: heap flattening (value objects inlined into containing objects and arrays, always read/written atomically) and scalarization (no allocation in JIT’d code). Some JDK classes (Integer, LocalDate) become value classes under preview. Null-restricted types are a separate JEP. Still preview. URLs: https://openjdk.org/projects/valhalla/value-objects , https://inside.java/2025/10/27/try-jep-401-value-classes/ , https://inside.java/2025/10/31/jvmls-jep-401/

Wasm shared-everything threads (proposal). Adds release-acquire memory order (vs the current SC-only), shared tables, and shared GC structs so WasmGC + threads can coexist. ThreadBoundData JS API bridges shared GC objects to unshared DOM nodes safely. URL: https://github.com/WebAssembly/shared-everything-threads/blob/main/proposals/shared-everything-threads/Overview.md

Mochi adaptation: Since vm3 piggybacks on Go’s GC for backing storage, you do not need to reinvent any of this. But two ideas matter: (1) Generational ZGC’s colored-pointer scheme is a strong reference for documenting how vm3’s metadata bits (generation, type tag, mutability) fit alongside the slab index in a single 8-byte handle, call out the precedent explicitly. (2) MMTk’s modular GC interface is the gold-standard architecture: even though Mochi will start with a single mark-sweep, MEP-41 should describe the slot lifetime API as a trait the VM can implement multiple ways (immediate-free, quarantine, mark-sweep, future LXR-style hybrid RC) so the design is not over-fitted to today’s collector. (3) Valhalla’s flattened value classes are exactly the pattern Mochi needs for small-record types, inline them into the containing arena slot instead of allocating a separate cell.

§9. Formal Verification of Memory Safety

RustBelt (POPL 2018, foundational). Iris-based Coq proof of semantic soundness for λRust + a corpus of unsafe Rust libraries. Foundation for everything below. URL: https://plv.mpi-sws.org/rustbelt/

RefinedRust (PLDI 2024). Foundational semi-automated functional-correctness verification of both safe and unsafe Rust, with a refinement type system proven sound (in Rocq) against a RustBelt-based model. Uses RustHorn-style prophecy variables (“borrow names”) to reason about &mut T. URL: https://iris-project.org/pdfs/2024-pldi-refinedrust.pdf

Aeneas. Translates safe Rust MIR to pure λ-calculus via the LLBC intermediate language; backends for F*, Coq, HOL4, Lean. ICFP 2024 added a soundness proof for the symbolic borrow-checker (Sound Borrow-Checking for Rust via Symbolic Semantics). Industrially used in Microsoft’s port of SymCrypt from C to verified Rust. URLs: https://aeneasverif.github.io/ , https://github.com/AeneasVerif/aeneas , https://lean-lang.org/use-cases/aeneas/ , https://arxiv.org/abs/2206.07185

Verus. Rust-syntax superset with forall/exists/requires/ensures, discharged via Z3. Verifies unsafe code, monomorphic only. URL: https://verus-lang.github.io/verus/guide/

Creusot. Deductive verification for safe Rust via the Pearlite specification language.

Kani. Bounded model checking; verifies a subset of Rust UB and user assertions. Used on Firecracker, s2n-quic, Hifitime.

AWS Standard Library Verification Effort. Cross-tool effort to verify the Rust stdlib using Verus + Creusot + Kani; bedrock community goal. URL: https://rust-lang.github.io/rust-project-goals/2024h2/std-verification.html

Iris-Wasm / Iris-MSWasm. Separation logic for full Wasm 1.0 and MSWasm; gives robust capability safety proofs (OOPSLA 2024).

hax. Cross-prover (F*, Coq, EasyCrypt, Lean) verification of security-critical Rust (2025 paper). URL: https://eprint.iacr.org/2025/142.pdf

Mochi adaptation: vm3 is small enough that an Iris-style separation-logic model is realistic for MEP-41 future work. The most cite-able analog is Iris-MSWasm, since MSWasm’s handle semantics is morally identical to vm3’s. Stake out the formal-correctness story: define a small λ-calculus model of vm3 (call it λvm3), describe handle/arena/generation operationally, and explicitly note in MEP-41 §7 (“future work”) that this can be lifted to Iris in the style of Iris-MSWasm. For an industrial story, point at Aeneas + SymCrypt, that’s the existing proof that “Rust verification used in production for memory-safety-critical code” is real, not aspirational.

§10. Spectre / Transient-Execution Mitigations for VMs

V8’s published retreat from pure-software mitigation. The V8 team concluded that software-only Spectre mitigations have unbounded complexity and ongoing maintenance cost (e.g., later compiler optimizations have silently undone earlier mitigations). Timer-resolution reduction + SharedArrayBuffer disabling were emergency measures; they explicitly state that some Spectre variants (especially v4) are infeasible to mitigate in software. The strategy pivoted toward the V8 sandbox (process-internal isolation) so Spectre-leaked secrets can’t reach OS resources. URL: https://v8.dev/blog/spectre

Switchpoline (ASIA CCS 2024). ARMv8 JIT mitigation that rewrites indirect branches into direct branches. 1.8% mean SPEC CPU 2017 overhead, 5µs JIT cost per new target. URL: https://www.misc0110.net/files/switchpoline_asiaccs24.pdf

SpecASan (ISCA 2025). Uses ARM MTE to extend tag-checking into the speculative execution path, speculative loads that fail MTE check are delayed until commit. Closes a class of Spectre leaks while preserving speculation perf. URL: https://dl.acm.org/doi/10.1145/3695053.3731119

“Do You Even Lift?” (POPL 2025). Compiler-level theorem stating which Spectre-safe properties survive lowering through optimization passes.

Branch Privilege Injection (USENIX Security 2025). New Spectre v2 variant; mitigation landscape now requires IBPB + IBRS + retpoline + RSB Stuffing + STIBP per microarchitecture.

Mochi adaptation: This is the most important “what you don’t have to build” thread. vm3 is hosted on Go and currently has no JIT. As long as that holds, Mochi’s Spectre exposure is whatever Go’s compiler emits, which means MEP-41 can punt to the Go team’s mitigation story. When a JIT does land, the V8-team lesson is the only one to internalize: do not invest in JIT-emitted Spectre defenses; instead make the runtime sandbox stronger so a Spectre leak is bounded to the user-Mochi heap. This argues for committing to a CHERI/MSWasm-style handle model up front: if a future Spectre leaks raw bytes from a Mochi arena, those bytes are still nothing without a forgeable handle to interpret them.

§11. Industry Surveys and Policy

Microsoft “~70%” reaffirmed. November 2025 Microsoft SFI Report restates that 70% of CVE-assigned vulnerabilities Microsoft resolves are memory-safety. Surface is shipping Rust-based UEFI firmware and Rust Windows drivers. ICSE 2025 Microsoft Research paper on LLM-assisted memory-safety annotation/Rust porting. URL: https://blogs.windows.com/windowsexperience/2025/11/10/advancing-security-with-windows-and-surface-microsoft-sfi-report-nov-2025/

Android: under 20% memory-safety bugs (Nov 2025). From 76% in 2019 → expected 24% by end-of-2024 → under 20% in 2025 (first time ever). Absolute counts: 223 in 2019 → <50 in 2024. “1000× reduction in memory-safety vulnerability density” in Rust code vs C/C++. Rust changes have 4× lower rollback rate and 25% less code-review time. First near-miss Rust memory-safety bug (linear overflow in CrabbyAVIF, CVE-2025-48530) was rendered non-exploitable by Scudo guard pages. URLs: https://security.googleblog.com/2025/11/rust-in-android-move-fast-fix-things.html , https://thehackernews.com/2025/11/rust-adoption-drives-android-memory.html

CISA roadmap deadline: January 1, 2026. Joint guide “The Case for Memory Safe Roadmaps” (CISA + NSA + FBI + Five Eyes); requires software manufacturers to publish a memory-safety roadmap by Jan 1, 2026. Exempts products with EOL before Jan 1, 2030. June 2025: CISA + NSA additional joint guide on MSL adoption. URLs: https://www.cisa.gov/case-memory-safe-roadmaps , https://www.cisa.gov/news-events/alerts/2025/06/24/new-guidance-released-reducing-memory-related-vulnerabilities , https://www.cisa.gov/news-events/news/cisa-nsa-fbi-and-international-cybersecurity-authorities-publish-guide-case-memory-safe-roadmaps

NSA “Memory Safe Languages: Reducing Vulnerabilities in Modern Software Development” (June 23, 2025, U/OO/172709-25). Endorses memory-safe-by-construction or hardware capabilities (CHERI); emphasizes language-level protections over developer discipline. URL: https://media.defense.gov/2025/Jun/23/2003742198/-1/-1/0/CSI_MEMORY_SAFE_LANGUAGES_REDUCING_VULNERABILITIES_IN_MODERN_SOFTWARE_DEVELOPMENT.PDF

EU Cyber Resilience Act (CRA). Cybersecurity requirements for digital products on the EU market by 2027.

Mochi adaptation: The policy environment hands MEP-41 its motivation paragraph for free. Mochi is already memory-safe by construction (no unsafe in user code) and Go-hosted; MEP-41 should frame itself as “the artifact that lets Mochi credibly claim compliance with the CISA Jan-2026 roadmap and NSA June-2025 guidance without hand-waving.” Borrow the 1000× density-reduction framing from Google Android, that’s the rhetorical hook for why “memory safety” is worth a numbered MEP.

§12. Use-After-Free Defenses (most relevant to vm3’s generation tags)

MarkUs (Ainsworth and Jones, 2020) and its 2024 evaluation. Quarantine + GC-style liveness check: freed memory cannot be reused until no pointers reach it. CAMP (USENIX Security 2024) measured ~10% overhead but found MarkUs missed 6 of 14 real-world UAF CVEs. URL: https://users.cs.northwestern.edu/~simonec/files/Research/papers/MODERN_USENIXSECURITY_2024.pdf

MiraclePtr / BackupRefPtr (Chrome). Reference-counted raw_ptr<T> on PartitionAlloc; quarantines + poisons (0xEF…EF) freed memory while any raw_ptr still exists. Fully rolled out across all platforms June 2023. As of July 2024, UAFs protected by MiraclePtr are no longer treated as security vulnerabilities by Chrome VRP. 5–6.5% memory overhead. May 2024 saw a $100,115 bypass (race on 29-bit refcount overflow); the bypass requires a separate race-condition primitive, so the bar is enormous. URLs: https://chromium.googlesource.com/chromium/src/+/main/base/memory/raw_ptr.md , https://security.googleblog.com/2022/09/use-after-freedom-miracleptr.html , https://www.securityweek.com/google-improves-chrome-protections-against-use-after-free-bug-exploitation/

Scudo Hardened Allocator (default on Android since 11, Fuchsia). Heap chunks have headers protected by checksum; primary/secondary class split; integrates GWP-ASan (probabilistic guard-page sampler, 1/5000 by default, ~70 KiB extra RAM per process). MTE-aware: uses PROT_MTE and random-tag per allocation. USENIX WOOT 2024 showed two exploitation techniques against Scudo; one was patched, the other is fundamental to large-chunk handling. URLs: https://llvm.org/docs/ScudoHardenedAllocator.html , https://source.android.com/docs/security/test/scudo , https://llvm.org/docs/GwpAsan.html , https://www.usenix.org/conference/woot24/presentation/mao

GWP-ASan in production (Trail of Bits, Dec 16 2025). Recommended for exploit detection in production, not just bug-finding. URL: https://blog.trailofbits.com/2025/12/16/use-gwp-asan-to-detect-exploits-in-production-environments/

Generation-tagging deployed in the wild. vm3’s 12-bit generation tag has direct precedent in: Vale’s generational references (covered in §3), MIE’s 4-bit hardware tag (§2), and conceptually in MiraclePtr’s deferred-reuse quarantine (every “quarantined” slot is functionally a slot with a not-yet-incremented generation).

Mochi adaptation: vm3 sits in the sweet spot of this literature. The MEP-41 design should explicitly enumerate:

  1. Generation width budget. 12 bits = 1/4096 collision probability per stale access. MIE uses 4 bits hardware (1/16); software can afford more. Document the tradeoff and consider 16 bits.
  2. Quarantine on free. Instead of immediately reissuing a slot after a generation bump, optionally hold it in a per-arena free-list ring buffer of length N. This is MiraclePtr/MarkUs in software, free given that the slab is already managed.
  3. Probabilistic guard pages (GWP-ASan analog). Allocate every Nth handle into a guard slab whose Cell layout is one-per-slot with a poisoned neighbor; any out-of-bounds index immediately faults. Cheap in Go since arenas are software-managed.
  4. Type-segregated arenas (Apple xzone analog). One arena per Mochi type prevents type-confusion even on a generation collision. This is already implied by vm3’s “typed Go-allocated arenas”, MEP-41 should call this out explicitly as a security property, not just an allocator-efficiency property.
  5. Generation as side-channel-protected secret (Apple TCE analog). Forbid user code from observing or comparing raw generation numbers; only the runtime’s deref opcode does the compare. This is the single most novel contribution MEP-41 can stake out, nobody else cleanly applies the Tag Confidentiality Enforcement lesson to a software handle scheme.
  6. The CrabbyAVIF lesson (Nov 2025). Even in a “memory-safe” language, a linear arithmetic bug in a parser can produce a writable out-of-bounds index; defense in depth (Scudo guard pages, generation bumps, type-segregated arenas) is what kept Android safe. Mochi should not assume static type safety obviates runtime defense in depth.

Closing meta-observations for MEP-41

Three threads dominate everything else and should anchor the document:

  1. The generational-reference idea (Vale, MIE, MiraclePtr) is converging across hardware, browsers, and academic languages simultaneously. vm3 is independently arriving at the same answer. MEP-41 is well-positioned to cite all three as prior art and claim Mochi as the first VM (vs hardware, allocator, or compiler) to do this cleanly.

  2. Modes / capabilities as orthogonal axes (OxCaml, Scala Caprese, Pony) is the right design vocabulary for layering optional safety on top of the base VM without forking the type system.

  3. The CISA Jan 1, 2026 deadline + Apple MIE shipping + Android <20% memory bugs makes Q1–Q2 2026 the right window to publish. The policy and industry tailwind is unusually strong; MEP-41 should land while the framing is fresh.