Public Truth Layer

Implementation Status

ANVAYA is an evidence-first operating system project. This page states, area by area, what is published, what is accepted specification, what is evidence-backed prototype asserted by repeatable QEMU boots, and what remains future work. Nothing here is aspirational: every prototype label corresponds to markers that CI re-asserts on each push. Current release: v1.0.0 (QEMU-Proven Milestone) - the terminal, feature-complete milestone of the 0.x line, with all five 1.0 completion gates A-E closed to their software scope (Gates B and D partial — external audit and physical A/B open): the Nucleus's accepted capability invariants are formally verified by bounded-exhaustive proofs plus Kani harnesses (unsafe-Rust TCB 0.44% vs Asterinas 14%); post-quantum crypto (ML-KEM/ML-DSA/SLH-DSA, KAT-verified against the official NIST ACVP vectors) is demonstrated across every trust surface with no demonstrated classical-only path; a reviewed threat model, tabletop, and design-time negative-test regression suite gate every fix (external audit pending); and a hot-path benchmark suite is published. This builds on 0.5 (native AI agents), 0.6 (constitution & human override), 0.7 (post-quantum & hardware-anchored), 0.8 (device mesh), and 0.9 (usable & sustainable). Honest scope: v1.0.0 is proven under QEMU and is not a production-deployed release — it does not claim a physical-hardware boot, an external third-party audit, hardware-enforced CHERI, or a hardware root of trust; the operational package signature is still Ed25519 and the audit chain a SHA-256 hash chain. Each is a documented open item.

Area	Label	Current Meaning
Manifesto	Published	Canonical principles and long-term direction are public.
Architecture & RFCs	10 Accepted	RFC 0001 through RFC 0010 are accepted, covering the capability model, AEC semantics, boot path, IPC, capability tables, nucleus contract, CSpace/handle representation, memory model, IPC surface v2, and the syscall ABI.
Governance	Proposed	Bootstrap remains founder-led while broader governance structures are formed.
Nucleus boot path	Verified First Light	The RISC-V nucleus boots in QEMU under OpenSBI with CI-asserted smoke evidence on every push.
RFC 0010 syscall surface	Proof-Backed Complete	As of v0.4.0 every syscall row in the accepted RFC 0010 table is proof-backed in the nucleus dispatch facade — ABI version and features, startup claim/finish, cap.identify/delegate/revoke/drop, cspace.alloc_slot and cspace.delete_slot, the five IPC calls, the five memory calls, task yield/exit/set-quota, trap_subscribe and trap_return, irq_bind and irq_ack, and wait/cancel — with denial-path probes for each and an ABI feature mask of bits=0x7ffffff.
Process dispatch registry	Evidence-Backed Prototype	A bounded kernel-resident registry maps active satp identities to per-process syscall dispatch contexts. The real U-mode trap path resolves dispatchers registry-first, and sret-continue entries carry a bounded continue budget so registry-served ecalls resume directly into U-mode; ANVAYA PROCESS DISPATCH REGISTRY OK and ANVAYA PROCESS DISPATCH SRET CONTINUE OK are required by QEMU smoke, and as of v0.2.130 two live tasks exchange registry-gated IPC with capability transfer while the bounded storage and network cores run over live dispatch (ANVAYA LIVE STORAGE SERVICE OK, ANVAYA LIVE NETWORK SERVICE OK), and as of v0.2.134 the live service executes from a signed-loaded code frame with tamper denial before mapping (ANVAYA LIVE SIGNED SERVICE OK), executes a WASM app and mediated cores over live dispatch, loads signed code that survives a virtio-blk roundtrip (ANVAYA LIVE PERSISTED PACKAGE OK), and runs on an allocator-derived multi-frame stack (ANVAYA MULTI FRAME STACK OK).
Capability semantics	Evidence-Backed Prototype	Attenuation, no-amplification, delegation with lineage tracking, revocation with descendant invalidation, slot reclamation, and reserved-slot lifecycle are asserted by QEMU evidence, with denial paths proved alongside success paths.
Memory isolation	Evidence-Backed Prototype	Owned Sv39 page-table frames, per-process satp contexts, translated user-copy windows, page-permission validation, shared-frame derivation, unmap and stale-mapping denial, and revocation-driven invalidation are proved under process satp identities, and the frame allocator reclaims freed frames through a bounded free-list and cross-CSpace reference counting, auto-reclaiming a frame only when its last reference drops (ANVAYA PRODUCTION ALLOCATOR OK, ANVAYA FRAME REFCOUNT OK).
Scheduler semantics	Evidence-Backed Prototype	Bounded ready/running/blocked slots, priority dispatch, timer preemption, budget expiry with task_set_quota control, wait-token queues, starvation aging, and a 37-dispatch scheduler-bound multi-syscall process loop are asserted in QEMU.
Init & service manager	Evidence-Backed Prototype	Capability-gated declarations, start/stop/restart transitions, failure reporting, registry lookup with rights-checked resolution, table-full denial, and restart limits are proved, including a scheduler-bound startup handoff from manifest init.
Service IPC	Evidence-Backed Prototype	Storage, network, installer, and service-registry services complete full-record RFC 0010 IPC with capability transfer, shared-frame buffers, wait-token completion/cancel/timeout, and audit continuity — bound through runner loader descriptors and compared across two persistence boots.
Signed packages & installer	Evidence-Backed Prototype	Signed bundles verify once, archive into a content-addressed store, journal and replay across boots, and launch with narrowed grants; tampered signatures are denied by both installer and runner before execution, and content is addressed by a real SHA-256 cryptographic hash (ANVAYA STORAGE SHA256 OK).
WASM/WASI runtime	Evidence-Backed Prototype	A bounded no-std WASM interpreter with WASI capability mediation runs twelve signed proof apps with deny-by-default file, DNS, TCP, clock, stdio, endpoint, and storage profiles through raw, installed, and loader-mapped execution, with the full i32 and i64 opcode sets (arithmetic, division with divide-by-zero and overflow traps, bitwise, shifts, and signed/unsigned comparisons), all four numeric value types (i32, i64, f32, f64), and numeric type conversions (wrap, extend, convert, demote, promote, and NaN-trapping truncation) proved before ANVAYA WASM RICHER OPS OK, ANVAYA WASM I64 OK, ANVAYA WASM F32 OK, ANVAYA WASM F64 OK, ANVAYA WASM CONVERT OK, and wide-type linear-memory load/store (i64/f32/f64) before ANVAYA WASM MEM WIDE OK, and sub-width i32 byte/halfword load/store (load8/load16 signed and unsigned, store8, store16) before ANVAYA WASM MEM NARROW OK, and a genuinely external rustc/LLVM-compiled wasm32 module (with WebAssembly globals support) executing before ANVAYA WASM EXTERNAL TOOLCHAIN OK, plus a two-function external module driving a real inter-procedural call before ANVAYA WASM EXTERNAL CALL OK, and a larger (261-byte, three-function) external module exceeding the former signed-package size cap before ANVAYA WASM EXTERNAL LARGE OK, and a WASI-targeted external module calling wasi_snapshot_preview1.fd_write through the capability-mediated path before ANVAYA WASM EXTERNAL WASI OK.
Virtio drivers	Evidence-Backed Prototype	The bounded virtio-MMIO core completes live virtio-blk sector read/write with two-boot persistence and package-archive restore, plus virtio-net TX, DNS TX, TCP retransmit TX, and RX queue proofs, and IPv4 longest-prefix-match routing plus ARP-neighbor-resolved forwarding (ANVAYA IP ROUTING OK, ANVAYA IP FORWARDING OK), and ICMP echo request/reply processing (ANVAYA IP ICMP ECHO OK) in QEMU.
Production loader & dispatcher	Released (0.4.0)	Released in 0.4.0: the production loader admits signed single- and multi-page process images through the scheduler and RFC 0010 boundary, with installer-driven admission and image-declared capability instances bound to named objects (ANVAYA PRODUCTION LOADER OK, ANVAYA PRODUCTION LOADER MULTIPAGE OK, ANVAYA LOADER CAPABILITY INSTANCE OK).
Live forwarding TCP/IP & audit service	Released (0.4.0)	Wire-learned ARP, ICMP echo reply, and forwarded TCP over the live NIC, with a protocol RX dispatch loop routing frames by protocol; block-backed persistence verified by kernel-wide SHA-256; and a production audit service behind a service-registered endpoint over scheduler dispatch (ANVAYA NET RX DISPATCH OK, ANVAYA STORAGE SHA256 POLICY OK, ANVAYA AUDIT SERVICE DISPATCH OK).
Signatures, quotas & fault isolation	Released (0.4.0)	Kernel-wide Ed25519 (RFC 8032) package signatures replace the placeholder primitive; a WASI-0.3 async-import subset carries capability-scoped quotas onto launch grants; and a timer-preempted long-lived U-mode computation runs with per-process fault isolation — a fault kills only the faulting process, audited, while a sibling continues (ANVAYA PACKAGE SIGNATURE OK, ANVAYA WASI LAUNCH QUOTA OK, ANVAYA LONG LIVED PROCESS OK, ANVAYA FAULT ISOLATED OK).
AEC runtime, broker & approval service	Future Work (0.5)	The Agent Execution Context runtime, the Intelligence Broker creation path, and the approval and constitutional-constraint services remain specification-stage until 0.5, when the userspace substrate carries executable evidence against RFC 0002 and RFC 0023.

Current prototype target

The active implementation targets QEMU virt on RV64GC with OpenSBI firmware and an S-mode Rust nucleus: single hart, deterministic panic path, and bounded, auditable proof slices. Three repeatable evidence suites gate every release — the boot smoke check, the two-boot virtio-blk persistence comparison, and the v0.3 application demo — and the smoke suite fails on any kernel panic in the normal boot log.

Anvaya v1.0.0 ("QEMU-Proven Milestone") is released: all five 1.0 completion gates (A-E) are closed to software scope (Gates B and D partial) — formal bounded-exhaustive verification of the accepted Nucleus invariants plus Kani harnesses, a threat model, response tabletop, and design-time negative-test regression suite (external audit pending), post-quantum crypto demonstrated across every trust surface with no demonstrated classical-only path, a published benchmark suite, and a fully evidenced acceptance matrix. It builds on the 0.4.0 "Production Substrate", a production image loader/dispatcher (single- and multi-page images, installer-driven admission, image-declared capability instances), live forwarding TCP/IP with a protocol RX dispatch loop, block-backed persistence with kernel-wide SHA-256 integrity, a production audit service over scheduler dispatch, service-grade IPC/memory hardening, and a WASI-0.3 async subset with capability-scoped quotas — plus real Ed25519 package signatures, timer-preempted long-lived computation, and per-process fault containment, each with code, tests, and repeatable QEMU evidence. The AEC/agent runtime of 0.5 ("AI Agents Run Natively") is the current frontier.

The RFC repository carries a vision traceability matrix and an ANVAYA 1.0 acceptance matrix. Use them to decide whether a target-state claim is stable, evidence-backed, provisional, planned, rejected, or superseded.