Implementation Status

What is vision, what is specified, and what exists today

ANVAYA is currently a specification-stage OS project with a verified first-light QEMU boot milestone, accepted local capability RFCs, a widened post-boot IPC plus table-backed object/task capability proof slice, an RFC 0010 syscall-facade slice, a v0.2 capability-backed memory-isolation substrate slice with owned Sv39 page-table materialization, bounded scheduler and init/service-manager semantics, a byte-backed process-manifest ABI, a mapped manifest-stack U-mode launch proof, a scheduler/launch-table-bound manifest init entry proof with stored Sv39 satp identity revalidation, one scheduler-bound cap.identify/cap.delegate/ipc.send/ipc.receive/ipc.reply/ipc.call/ipc.cancel/wait_one/cancel_token/mem.frame_alloc/mem.map/mem.unmap/cap.revoke multi-syscall proof with launch-table resume, scheduler-bound cap.delegate evidence with ANVAYA SCHEDULER PROCESS CAP DELEGATE OK pid=0xa313 and ANVAYA SCHEDULER PROCESS CAP DELEGATE REVOKE OK pid=0xa313, IPC send/receive/reply/call/cancel delivery, exact receive capability-field evidence, returned endpoint and device-frame capability evidence, cumulative send+receive+reply+call IPC audit validation, bad-length ipc.call failure evidence with reply_preserved=1, scheduler-bound pending-request cancel clearing, empty cancel idempotence, scheduler-bound revoked-endpoint failure/audit evidence: eight events with two failure records, a reusable process-bound memory syscall runner proof, a process-bound cap.delegate proof with ANVAYA USER PROCESS CAP DELEGATE OK pid=0xa315, initial no-std SDK/storage/network/package/installer/WASM/WASI/runner/example-app crates, a rights-checked service-registry resolution plus proof-harness endpoint IPC proof requiring ANVAYA WASM SERVICE REGISTRY RESOLUTION IPC OK with service=0xb803 and transfer_rights=0x2, a storage app package loader proof requiring ANVAYA WASM APP STORAGE PACKAGE LOADER OK with process=0xa804, an installed app package loader proof requiring ANVAYA WASM APP PACKAGE LOADER OK with process=0xa803, an installed storage runner proof requiring ANVAYA WASM APP INSTALL STORAGE RUNNER OK for installed storage-roundtrip packages, a signed package signature denial proof requiring ANVAYA WASM APP SIGNATURE DENIAL OK for tampered read-config bundles, a virtio-blk write/read-back proof through the bounded virtqueue path, a virtio-blk exact-pattern persistence proof, a storage-block package restore proof, virtio-net TX, ANVAYA VIRTIO NET DNS TX OK, and virtio-net RX proofs, plus bounded DNS A, DNS-over-UDP/IPv4 packet, and DNS Ethernet frame proofs with dns_eth_query=75. RFC 0010 now accepts the first Nucleus syscall ABI contract, RFC 0007 accepts the software CSpace/handle representation, and RFC 0002 accepts the Agent Execution Context semantic model; the production scheduler, production arbitrary userspace loader, full reusable scheduler/loader-bound U-mode ecall dispatcher, CHERI sealed-handle encoding, AEC runtime, broker creation path, approval service, and audit service remain future work. Production durable storage/package service integration, live TCP/IP state machines, timers, routing, and network service integration also remain future work. This page is the public truth layer for current maturity.

Area	Label	Current Meaning
Manifesto	Published	Canonical principles and long-term direction are public.
Architecture	Specified	Target-state design exists, but it should not be read as full implementation.
Governance	Proposed	Bootstrap remains founder-led while broader governance structures are formed.
Nucleus boot path	Verified First Light	Historical CI proof exists for the first-light boot path, and the widened local semantic slice is now asserted by the same smoke workflow.
DTB-backed inventory	Implemented	The prototype now reads the DTB header, a bounded set of memory ranges, and the reservation map for its current inventory surface.
Post-boot task and IPC slice	Evidence-Backed Prototype	One child task context, two deterministic local task records, one timer-backed event path, three synchronous request/reply round trips, and explicit failure outcomes exist in the prototype.
Capability semantics	Evidence-Backed Prototype	Endpoint-right attenuation, no-amplification, delegated IPC transfer, validated object/task delegation, parent-slot revocation, lineage isolation, and slot reclamation are now asserted by QEMU evidence.
Memory isolation substrate	Evidence-Backed Prototype	The v0.2 slice proves frame-cap creation, two task-owned CSpaces, owned root/L1/two-L0 page-table frames, Sv39-shaped PTE records, page-table materialization, satp activation/restore, map-time overflow denial, process-bound memory frame allocation/map/unmap/revoke dispatch, page-permission validation, requested-right denial, cross-CSpace frame revocation, all-staged-space mapping invalidation, stale mapping failure, and revoked-page fault records.
Scheduler semantics	Evidence-Backed Prototype	The nucleus proof now covers bounded ready/running/blocked task slots, priority dispatch, timer-tick preemption, budget expiry, single-runner dispatch, and starvation-aging selection.
Init/service manager semantics	Evidence-Backed Prototype	The bounded init/service-manager proof covers capability-gated declarations, duplicate and missing-capability denial, start/stop/restart transitions, failure reporting, registry lookup, rights-checked service-registry resolution, table-full denial, stopped-slot reclaim, and restart-limit checks.
Process manifest handoff	Evidence-Backed Prototype	The process-manifest proof parses a byte-backed ABI with init and service records, validates roles/rights/reserved fields, admits both records into the scheduler, dispatches init first, publishes service registry entries, and now has installed app package loader evidence plus rights-checked service-registry resolution plus proof-harness endpoint IPC evidence requiring ANVAYA WASM SERVICE REGISTRY RESOLUTION IPC OK with service=0xb803 and transfer_rights=0x2.
Service registry resolution IPC	Evidence-Backed Prototype	The QEMU proof resolves the running endpoint-receive service with explicit receive rights, dispatches service=0xb803 through the scheduler, sends an exact receive-only endpoint transfer with transfer_rights=0x2, marks it syscall-returned, and requires ANVAYA WASM SERVICE REGISTRY RESOLUTION IPC OK.
Storage app package loader	Evidence-Backed Prototype	The QEMU proof derives READ+WRITE application manifest rights from installed storage-roundtrip package launch grants, dispatches process=0xa804 through the launch table and scheduler proof, and requires ANVAYA WASM APP STORAGE PACKAGE LOADER OK.
Signed package signature denial	Evidence-Backed Prototype	The QEMU proof tampers the signed read-config bundle, proves the installer rejects it without recording an install, proves the runner rejects it before execution, and requires ANVAYA WASM APP SIGNATURE DENIAL OK.
Installed storage runner	Evidence-Backed Prototype	The QEMU proof installs storage-roundtrip, runs the installed record through service-backed storage dispatch, requires two bounded storage IPC calls and zero network IPC calls, and requires ANVAYA WASM APP INSTALL STORAGE RUNNER OK.
Manifest-backed U-mode launch	Evidence-Backed Prototype	The launch proof maps the manifest-declared init stack, materializes text plus stack leaves in owned Sv39 tables, runs a stack-touching ABI-version ecall under process satp, preserves trapped user sp, and denies a third distinct L0-table bucket at map time.
Scheduler-bound process entry	Evidence-Backed Prototype	The manifest init entry proof now binds a loaded launch record to the current running scheduler task and stored Sv39 satp identity, then revalidates scheduler and satp state before marking the launch syscall-returned.
Scheduler-bound syscall loop	Evidence-Backed Prototype	The manifest-loaded process proof now dispatches cap.identify, cap.delegate, ipc.send, ipc.receive, ipc.reply, ipc.call, ipc.cancel, wait_one, cancel_token, mem.frame_alloc, mem.map, mem.unmap, and cap.revoke through the same scheduler/launch-table binding, proving scheduler-bound cap.delegate narrowed-child-handle and parent-slot validation with ANVAYA SCHEDULER PROCESS CAP DELEGATE OK pid=0xa313, revoked child-handle denial after cleanup with ANVAYA SCHEDULER PROCESS CAP DELEGATE REVOKE OK pid=0xa313, send-request, receive-window, reply-request-window, call-request, call-reply, cancel, and wait-token validation, endpoint delivery, transferred timer authority, exact receive capability-field evidence, returned endpoint and device-frame capability evidence, cumulative send+receive+reply+call IPC audit success, bad-length ipc.call failure validation with reply_preserved=1, scheduler-bound pending-request cancel clearing, empty cancel idempotence, scheduler-bound revoked-endpoint failure/audit evidence: eight events with two failure records, scheduler process wait-token evidence with ANVAYA SCHEDULER PROCESS WAIT TOKEN OK pid=0xa313, mapping handle resolution, page-table entry validation, explicit unmap, stale mapping-handle denial, and transient frame revocation.
Process-bound memory syscalls	Evidence-Backed Prototype	A reusable process-bound U-mode syscall runner now exercises mem.frame_alloc, mem.map, mem.unmap, and cap.revoke through SyscallDispatchContext under active process satp, including stale mapping-handle denial and frame revocation evidence.
Process-bound cap.delegate	Evidence-Backed Prototype	A process-bound cap.delegate U-mode ecall proof now runs under the mapped process satp, validates process-local CSpace authority, returns a narrowed timer-capability child handle, checks parent-slot lineage, and requires ANVAYA USER PROCESS CAP DELEGATE OK pid=0xa315 in QEMU smoke.
SDK and service cores	Initial Crates + Proof Consumers	The main repository now contains no-std SDK, storage, network, package, installer, WASM, WASI, runner, and example-app crates with bounded capability checks, a rights-checked service-registry resolution plus proof-harness endpoint IPC proof requiring ANVAYA WASM SERVICE REGISTRY RESOLUTION IPC OK with service=0xb803 and transfer_rights=0x2, a storage app package loader proof requiring ANVAYA WASM APP STORAGE PACKAGE LOADER OK with process=0xa804, an installed app package loader proof requiring ANVAYA WASM APP PACKAGE LOADER OK with process=0xa803, an installed storage runner proof requiring ANVAYA WASM APP INSTALL STORAGE RUNNER OK, a signed package signature denial proof requiring ANVAYA WASM APP SIGNATURE DENIAL OK, bounded DNS A, DNS-over-UDP/IPv4 packet, and DNS Ethernet frame handling with dns_eth_query=75 evidence; production loader-launched services remain future work.
Virtio driver core	Evidence-Backed Prototype	The QEMU proof now probes virtio-blk and virtio-net MMIO devices, negotiates baseline virtio-blk features, programs the legacy queue, performs a sector-0 read, performs a virtio-blk write/read-back on sector 1, proves virtio-blk exact-pattern persistence across two QEMU boots with one raw image, proves a storage-block package restore from sector 2, proves virtio-net TX queue completion with a deterministic ARP/Ethernet frame, requires ANVAYA VIRTIO NET DNS TX OK for a bounded DNS Ethernet frame, proves virtio-net RX by validating QEMU's ARP reply, and proves bounded DNS A, DNS-over-UDP/IPv4 packet, and DNS Ethernet frame write/parse in the network core with dns_udp_query=61 dns_udp_response=77 dns_eth_query=75 dns_eth_response=91; production durable storage/package integration, live TCP/IP state machines, timers, routing, and network service integration remain planned.
CSpace and handle representation	Accepted RFC	RFC 0007 freezes per-task CSpaces, slot/generation/lineage metadata, format 0x1 software u64 handles behind RFC 0010 opaque handles, IPC import/export, revocation, stale failure, CHERI mapping, and software fallback.
Nucleus ownership boundary	Accepted RFC	RFC 0006 freezes the Nucleus as the privileged owner of capability validation, IPC primitive enforcement, scheduling primitives, address-space primitives, traps, interrupts, and startup handoff.
Nucleus syscall ABI	Accepted RFC + Proof Facade	RFC 0010 freezes the first userspace/Nucleus syscall contract; the nucleus now exercises a proof-backed facade for ABI version, capability, IPC send/receive/call/reply/cancel, wait/cancel, and memory calls, plus a scheduler/launch-table-bound manifest init ecall, one scheduler-bound cap.identify/cap.delegate/ipc.send/ipc.receive/ipc.reply/ipc.call/ipc.cancel/wait_one/cancel_token/mem.frame_alloc/mem.map/mem.unmap/cap.revoke loop with launch-table resume, ANVAYA SCHEDULER PROCESS CAP DELEGATE OK pid=0xa313, ANVAYA SCHEDULER PROCESS CAP DELEGATE REVOKE OK pid=0xa313, IPC send/receive/reply/call/cancel delivery, exact receive capability-field evidence, returned endpoint and device-frame capability evidence, cumulative send+receive+reply+call IPC audit validation, bad-length ipc.call failure validation with reply_preserved=1, scheduler-bound pending-request cancel clearing, empty cancel idempotence, scheduler-bound revoked-endpoint failure/audit evidence: eight events with two failure records, process-bound memory dispatch, and a process-bound cap.delegate proof under active process satp before a full reusable scheduler/loader-bound dispatcher exists.
Agent Execution Context model	Accepted RFC	RFC 0002 freezes AEC identity, goals, lifecycle, supervision, approval, quotas, audit, world-model boundaries, failure/cancellation, and relation to processes/tasks, capabilities, IPC, and RFC 0010 syscalls; no AEC runtime exists yet.
Vision/spec blueprint	Mixed Accepted/Draft RFC Suite	RFC 0001, RFC 0002, RFC 0003, RFC 0004, RFC 0005, RFC 0006, RFC 0007, and RFC 0010 are accepted; RFC 0008-0009 and RFC 0011-0031 continue drafting the remaining planned contracts needed for a contradiction-free 1.0 blueprint.
Userspace and runtime	Initial Bounded Crates	The SDK, service cores, package installer, WASM/WASI mediation, runner, ten proof apps, rights-checked service-registry resolution plus proof-harness endpoint IPC proof, storage app package loader proof, installed app package loader proof, and installed storage runner proof exist as bounded no-std groundwork; full production userspace services and loader-launched app execution remain future milestones.

Current prototype target

The active implementation slice targets QEMU virt on RV64GC using the default OpenSBI firmware and an S-mode Rust nucleus. It is still intentionally narrow: single hart, deterministic panic path, DTB-backed discovery of a bounded set of memory ranges plus reservation map, one child task context, one timer-backed event path, one timer request/reply proof path, one task-context request/reply proof path, one delegated endpoint-capability proof path, one bounded object/task capability-table proof path, explicit failure-path evidence, table-backed stale/revoked/lineage/slot and metadata failure evidence, lineage-isolation and slot-reclaim evidence, a proof-backed RFC 0010 syscall facade for ABI version, capability, IPC receive/call/reply, memory calls, malformed rights-bit denial, and revoke-driven mapping invalidation, a staged memory-isolation proof with two task-owned CSpaces, owned root/L1/two-L0 page-table frames, Sv39-shaped PTE rows, page-table materialization, one-shot satp activation/restore, U-mode page-fault capture, process-bound capability/IPC syscall proof paths, process-bound memory frame allocation/map/unmap/revoke dispatch, process-bound cap.delegate evidence with ANVAYA USER PROCESS CAP DELEGATE OK pid=0xa315, scheduler-bound cap.delegate evidence with ANVAYA SCHEDULER PROCESS CAP DELEGATE OK pid=0xa313 and ANVAYA SCHEDULER PROCESS CAP DELEGATE REVOKE OK pid=0xa313, frame-cap mapping, page-permission validation, requested-right denial, unmap, cross-CSpace frame revocation, all-staged-space mapping invalidation, stale mapping failure, revoked-page fault records, bounded scheduler and init/service-manager semantics, a byte-backed process-manifest ABI, a mapped manifest-stack U-mode launch proof, and a scheduler/launch-table-bound manifest init entry proof with stored Sv39 satp identity revalidation, one scheduler-bound cap.identify/cap.delegate/ipc.send/ipc.receive/ipc.reply/ipc.call/ipc.cancel/wait_one/cancel_token/mem.frame_alloc/mem.map/mem.unmap/cap.revoke multi-syscall proof with launch-table resume, scheduler-bound cap.delegate evidence with ANVAYA SCHEDULER PROCESS CAP DELEGATE OK pid=0xa313 and ANVAYA SCHEDULER PROCESS CAP DELEGATE REVOKE OK pid=0xa313, IPC send/receive/reply/call/cancel delivery, exact receive capability-field evidence, returned endpoint and device-frame capability evidence, cumulative send+receive+reply+call IPC audit validation, bad-length ipc.call failure evidence with reply_preserved=1, scheduler-bound pending-request cancel clearing, empty cancel idempotence, scheduler-bound revoked-endpoint failure/audit evidence: eight events with two failure records, process-bound cap.delegate evidence with ANVAYA USER PROCESS CAP DELEGATE OK pid=0xa315, initial SDK/service/runtime proof crates, a rights-checked service-registry resolution plus proof-harness endpoint IPC proof requiring ANVAYA WASM SERVICE REGISTRY RESOLUTION IPC OK with service=0xb803 and transfer_rights=0x2, a storage app package loader proof requiring ANVAYA WASM APP STORAGE PACKAGE LOADER OK with process=0xa804, an installed app package loader proof requiring ANVAYA WASM APP PACKAGE LOADER OK with process=0xa803, an installed storage runner proof requiring ANVAYA WASM APP INSTALL STORAGE RUNNER OK for installed storage-roundtrip packages, a signed package signature denial proof requiring ANVAYA WASM APP SIGNATURE DENIAL OK for tampered read-config bundles, a virtio-blk write/read-back proof, a virtio-blk exact-pattern persistence proof, a storage-block package restore proof, virtio-net TX, ANVAYA VIRTIO NET DNS TX OK, and virtio-net RX proofs, bounded DNS A, DNS-over-UDP/IPv4 packet, and DNS Ethernet frame proofs with dns_eth_query=75, an accepted RFC 0007 software CSpace/handle representation, an accepted RFC 0010 syscall ABI contract, and an accepted RFC 0002 AEC semantic model, but no production allocator, production scheduler, production arbitrary userspace loader, SMP, full reusable scheduler/loader-bound U-mode ecall dispatcher, CHERI sealed-handle encoding, AEC runtime, broker creation path, approval service, or audit service yet.

Follow-on work will extend the RFC 0010 syscall-dispatch facade into a real U-mode ecall path while keeping broad IPC semantics and the bounded DTB inventory contract provisional until executable mechanisms force wider representations. The next verification work is scheduler/loader-bound syscall dispatch, production arbitrary manifest-stack allocation, full service-grade memory/IPC paths, and broader process-bound userspace copy isolation; AEC implementation remains planned until the lower userspace process substrate, AEC registry, Intelligence Broker creation API, approval flow, and audit service have executable evidence against RFC 0002.

The RFC repository now carries a vision traceability matrix and ANVAYA 1.0 acceptance matrix. They should be used to decide whether a target-state claim is stable, evidence-backed, provisional, planned, rejected, or superseded.