Update log (ISO 8601)

Anvaya v1.0.0 ("QEMU-Proven Milestone") is released — the terminal, feature-complete milestone of the 0.x line (not a production-deployed release). All five 1.0 completion gates are closed to software scope with QEMU/CI evidence (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 (capability non-amplification, bounds, tag-revocation isolation, and cross-device delegation, 88k+ cases) plus Kani harnesses, with the unsafe-Rust TCB measured at 0.44% versus Asterinas 14% (ANVAYA VERIFICATION OK); a reviewed threat model, a security-response tabletop, and a design-time negative-test regression suite hold every modeled attack class fail-closed (ANVAYA THREAT REGRESSION OK assessment=design-time-negative-tests; external audit pending, not a live red-team); post-quantum crypto is demonstrated across every trust surface with no demonstrated classical-only path (ANVAYA PQC SURFACES OK; operational package signature still Ed25519 and audit a SHA-256 hash chain, hybrid rekey tracked); a hot-path benchmark suite is published (ANVAYA BENCH OK); and every acceptance-matrix row is evidenced. Honest scope: v1.0.0 is proven under QEMU and does not claim a physical-hardware boot, an external third-party audit, hardware-enforced CHERI, or a hardware root of trust — each is a documented open item. The anvaya-nucleus crate is bumped to v1.0.0; all three QEMU proof scripts and the full workspace test suite are green at release.

Anvaya v0.9.0 ("Usable & Sustainable") is released. All four 0.9 gates are closed: an Energy Broker makes energy a capability-carried resource with joule budgets metered fail-closed, SCI (ISO/IEC 21031) carbon accounting, and carbon-aware scheduling that never overrides safety (ANVAYA ENERGY BROKER OK); a capability-resolving intent router with a CLI personality (ANVAYA INTENT CLI OK); a headless framebuffer compositor with touch and voice personalities on the same router (ANVAYA COMPOSITOR OK); and a package manager for PQC (ML-DSA) signed packages with install/upgrade/remove and signature, version, and dependency checks (ANVAYA PACKAGE MANAGER OK).

Anvaya v0.8.0 ("Device Mesh") is released. All four 0.8 gates are closed via the new anvaya-mesh crate: a PQC-authenticated pairing handshake with SLH-DSA device-root identity attestation (ANVAYA MESH PAIRING OK); cross-device capability delegation carried by an ML-DSA proof-of-grant with attenuation and epoch-based remote revocation, re-checked on every use (ANVAYA MESH CAPABILITY OK); SHA-256 content-addressed sync with an order-independent CRDT namespace merge (ANVAYA MESH STORAGE OK); and capability-scoped agent routing with a signed context handoff (ANVAYA MESH AGENT OK). The two mesh nodes are two in-kernel node contexts over an in-memory wire — a small trusted mesh, not two separate QEMU processes.

Anvaya v0.7.0 ("Post-Quantum & Hardware-Anchored") is released. All four 0.7 gates are closed. A new anvaya-pqc crate implements ML-KEM (FIPS 203), ML-DSA (FIPS 204), and SLH-DSA (FIPS 205, SHAKE) plus X25519 and Keccak, each verified bit-exact against the official NIST ACVP known-answer vectors, with a hybrid X25519+ML-KEM KEM that refuses classical-only downgrades (ANVAYA PQC OK). The signed-package policy, agent identity, device attestation, and audit segments are re-keyed to hybrid Ed25519+ML-DSA with SLH-DSA for long-lived keys (ANVAYA PQC PACKAGE OK, ANVAYA PQC IDENTITY OK). A CHERIoT-style capability profile adds bounds+permissions+validity-tag enforcement (ANVAYA CHERI PROFILE OK), and a DICE-style measured-boot chain produces an ML-DSA attestation with tamper detection (ANVAYA MEASURED BOOT OK). Software profiles pending CHERI-RISC-V silicon and a hardware root of trust.

Anvaya v0.6.0 ("Constitution & Human Override") and the v0.6.1 hardening are released. A bounded three-tier constitutional rule engine with attested amendment, structured AEC rationales, audit format v3, and a firmware-owned hardware escape / human-override core, plus an experimental resident M-mode QEMU monitor that PMP-protects firmware policy and proves a three-boot hostile-supervisor gate. QEMU evidence and early 0.7 groundwork, not a completed hardware root of trust.

Anvaya v0.5.0 ("AI Agents Run Natively") is released. A bounded no-std Intelligence Broker version-binds model artifacts and mediates capability-scoped inference with quotas (ANVAYA INTELLIGENCE BROKER OK); the AEC runtime adds Ed25519 goal-bound identity, rooted supervision, attenuation-only capabilities, and contextual hash-chained audit (ANVAYA AEC LIFECYCLE OK); a side-effect-free world model with trust-root-verified approvals (ANVAYA AEC SANDBOX APPROVAL OK); and an SVID-style A2A core with capability-scoped agent cards and competing-goal arbitration (ANVAYA MULTI AGENT OK).

Anvaya v0.4.0 ("Production Substrate") is released. All six 0.4 completion gates are closed: a production image loader/dispatcher (single and multi-page segments, installer-driven admission, image-declared capability instances); live forwarding TCP/IP over the NIC 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 including recoverable page-fault-ack, shared-buffer teardown, and multi-service chained-audit continuity; and a bounded WASI-0.3 async-import subset with capability-scoped quotas carried onto launch grants. Pre-0.5 hardening replaced the placeholder package signature with a real kernel-wide Ed25519 primitive, proved a timer-preempted long-lived U-mode computation, and contained U-mode faults to the faulting process. The anvaya-nucleus crate is bumped to v0.4.0; the workspace unit tests and all three QEMU scripts are green at release. The next milestone is 0.5 - AI Agents Run Natively.

Release v0.3.26 closes Gate A's last two remainders, and with it all six 0.4 completion gates. A process-image package is installed through the package registry - the installer verifies the signature and derives the launch grants - and the loader then admits the same installer-verified package, so admission is driven from the installer path rather than composed in the kernel harness. Each image-declared dependency (a specific service object id) is bound to an endpoint capability instance carrying the grant's rights: a capability to a named object, not an abstract right. The proof binds the declared dependency 0xb701 to an endpoint instance, installs it in a real capability table and resolves it with SEND, has an ungranted MANAGE right refused, and refuses instance binding for an image that declares a dependency with no backing endpoint grant. QEMU evidence: ANVAYA LOADER CAPABILITY INSTANCE OK across smoke and demo. All six 0.4 gates (A-F) are now closed.

Release v0.3.25 advances Gate A: the AVPI process-image limits rise to two pages per segment and the production loader admits an image whose data segment spans two pages. The layout planner rounds each segment up to its page count, the loader allocates one text plus two data plus one stack frame, copies the image bytes across the two data frames, maps all four pages, materializes the address space, and byte-verifies the data segment across the page boundary - a page-crossing copy bug would fail the verify - before the full admit, dispatch, U-mode abi.version, clean task.exit lifecycle. QEMU evidence: ANVAYA PRODUCTION LOADER MULTIPAGE OK with data_pages=2 across smoke and demo.

Release v0.3.24 closes Gate F's last two remainders. anvaya-wasi gains a bounded WASI-0.3-aligned async-import subset: a future<u64> with begin/poll/await, where a poll returns a retryable pending status until the host resolves it and then yields the value exactly once, metered against the fd-I/O budget (streams and multi-value futures are explicitly deferred). anvaya-runner derives a capability-scoped quota from a package's installer-emitted launch grants - more capability earns more budget across all four classes, a grant-free app gets only the base - so the same grants that decide what an app may touch also bound how much it may consume. The kernel proof installs an app, derives its quota from the installed record's grants, has the runner enforce that quota when instantiating the module (baseline runs to exit; a starved re-derivation is refused fail-closed), and round-trips an async future metered against the launch quota. QEMU evidence: ANVAYA WASI LAUNCH QUOTA OK across smoke, demo, and both persistence boots.

Release v0.3.23 closes Gate B's last generalization item. A new classifier reads a received Ethernet frame's EtherType and, for IPv4, its transport-protocol byte, returning a protocol class (ARP, IPv4-ICMP, IPv4-TCP, other-IPv4, non-IPv4) and failing closed on frames too short to classify. The kernel dispatch loop runs a six-frame batch crossing the RX boundary and hands each to exactly the right handler: the ARP reply learns a neighbor, the ICMP echo request generates a validated reply, the TCP SYN produces a forwarding decision toward its off-link peer through the ARP-learned gateway, and the IPv4-UDP, non-IPv4, and runt frames are counted drops or fail-closed. No handler ever sees a frame of another class, and the TCP forward resolves only after ARP taught the neighbor cache. With the live ARP/ICMP/TCP paths (v0.3.10 to v0.3.13), Gate B is complete. QEMU evidence: ANVAYA NET RX DISPATCH OK across smoke, demo, and both persistence boots.

Release v0.3.22 closes Gate E's last two remainders. A shared frame runs its full lifecycle - mapped, written through and read back, cleanly unmapped and re-mapped, then revoked, after which the stale mapping write-probe, a stale unmap, and a re-map through the revoked handle all fail closed, and the freed frame is reclaimed to a fresh lineage at the same physical address. Separately, three distinct service processes each complete a live send/receive/reply cycle over scheduler dispatch; the append-only SHA-256 hash-chained kernel audit trail grows by exactly the nine dispatched syscalls, re-verifies from genesis, and attributes its new segment to all three service identities. With pressure-reclaim (v0.3.14) and recoverable page-fault-ack (v0.3.21), Gate E is complete. QEMU evidence: ANVAYA MEM SHARED BUFFER TEARDOWN OK and ANVAYA SERVICE AUDIT CONTINUITY OK across smoke, demo, and both persistence boots.

Release v0.3.21 adds recoverable page-fault handling toward Gate E. A U-mode task computes, then stores to a page that is present in its address space but armed invalid (the frame is allocated and its leaf PTE built; only the valid bit is cleared). The store traps as a store/AMO page fault; the trap handler recognises the armed address, makes the page present through the kernel identity mapping, and returns without advancing the program counter so the faulting store re-executes and completes. The task resumes, reads the value back through the now-mapped frame, and exits with a result verified against an independent in-kernel computation, with the stored value confirmed in the frame's physical memory. Unlike the v0.3.19 kill path, the faulting task survives and makes progress - the fault to ack to resume to progress loop that mem.fault_ack models, driven by a genuine trap. QEMU evidence: ANVAYA MEM PAGE FAULT ACK OK across smoke, demo, and both persistence boots.

Release v0.3.20 closes Gate D's last open item: the audit service is declared and started in the init/service manager, resolved through the rights-checked service registry (an over-privileged resolution is refused), and serves typed AUDT requests over live scheduler dispatch. A client process sends the request as a full RFC 0010 record through SYSCALL_IPC_SEND from U-mode; the service process receives and replies over its own dispatch context, deriving its authority from the transferred capability's rights - a WRITE-authorized append and an INSPECT-authorized chain verify succeed while a READ-only append is refused fail-closed. All nine dispatched syscalls land on the IPC audit path with zero failures. QEMU evidence: ANVAYA AUDIT SERVICE DISPATCH OK across smoke, demo, and both persistence boots.

Release v0.3.19 closes the fault-blast-radius gap: under the timer-preempted two-task machinery from v0.3.18, one U-mode task computes 800k iterations and then stores to an address its address space never mapped. The store/AMO page fault is contained at the trap boundary - the faulting task is killed and never scheduled again, the kill is recorded as an event on the chained kernel audit trail (re-verified from genesis by the end-of-boot continuity proof), and the sibling task keeps computing through further timer quanta to a result verified against an independent in-kernel computation. The kernel does not panic and boot runs to completion. With v0.3.17 (real Ed25519 signatures) and v0.3.18 (long-lived preemption), both load-bearing pre-0.5 honest-gap slices are closed and the 0.5 start gate is satisfied. QEMU evidence: ANVAYA FAULT ISOLATED OK with killed=1 audited=1 survivor_verified=1 continued=1.

Release v0.3.18 delivers the first convergence of the isolation and computation halves: two isolated U-mode tasks (own satp-keyed address spaces) run register-only xorshift64 workloads for 1.5M and 1.0M iterations while a supervisor timer interrupt preempts the running task at arbitrary instruction boundaries every 200 microseconds - the full trap frame, sepc, and satp are parked and the sibling's context restored in place. The tasks genuinely interleave on interrupt-driven quanta rather than running as one-shot proof excursions, and each task's final value is verified against an independent in-kernel computation of the same sequence, so a context-switch corruption of even one register fails the boot. QEMU evidence pins the exact results behind ANVAYA LONG LIVED PROCESS OK across smoke, demo, and both persistence boots.

Release v0.3.17 closes the top pre-0.5 honest gap: the package "signature" is now a real signature. A bounded no_std SHA-512 + Ed25519 (RFC 8032) implementation (pinned to the RFC 8032 and FIPS 180-4 test vectors) replaces the placeholder that encoded the signed-region length as a u16, kernel-wide, under the unchanged trust-policy chain. The kernel proof re-verifies the RFC 8032 vector in-kernel, asserts the committed public key matches its seed derivation, and denies tampered-signature, tampered-content, wrong-key, and non-canonical-scalar variants fail-closed before ANVAYA PACKAGE SIGNATURE OK with placeholder_sites=0, asserted by smoke, demo, and both persistence boots. The persisted package archive spans two sectors to carry the 64-byte signatures with the same digest and tamper evidence. Signing keys are build-time proof keys; production key custody remains later-milestone work.

Release v0.3.16 closes the audit-persistence loop: the boot's live dispatch audit trail persists to its own block sector alongside a SHA-256 digest of the record region, and a prior boot's persisted trail is digest-verified AND hash-chain-verified from genesis before it is accepted - two independent integrity layers. A flipped on-disk byte is rejected at both layers. Two-boot QEMU evidence asserts ANVAYA AUDIT TRAIL BLOCK HASH VERIFIED OK on the second boot and its absence on the first, with the every-boot ANVAYA AUDIT TRAIL BLOCK OK marker carrying tamper_denied=2 across smoke, demo, and both persistence boots.

Release v0.3.15 lands the 0.4 quota gate's core: per-app capability-scoped resource budgets across four classes - interpreter fuel, guest memory pages, mediated file-I/O bytes, and socket operations. Delegation can only attenuate a budget, never amplify it; charges are all-or-nothing so a refused operation spends nothing; and mediated writes are gated on both rights and budget. The kernel proof runs the same module cleanly under its granted quota and denies it fail-closed under starved fuel and memory budgets, meters a granted write and refuses the next byte, and refuses the zero-budget socket class - the multi-tenant DoS defense upstream WASI still lacks. QEMU evidence includes ANVAYA WASI QUOTA OK with fail_closed=4 asserted by smoke and the app demo.

Release v0.3.14 opens the 0.4 memory-hardening gate: a frame allocator confined to a four-frame window is driven to exhaustion - further allocation fails closed rather than corrupting state - then explicit frees and the last-reference drop of a thrice-shared refcounted frame return capacity, and allocation resumes reusing exactly the reclaimed frames. Double-free and out-of-range frees stay denied under pressure, and reclaim accounting is asserted against the allocator's own counters. QEMU evidence includes ANVAYA MEM PRESSURE RECLAIM OK asserted by smoke and the app demo.

Release v0.3.13 completes the live-networking evidence set: a new ICMP-over-IPv4/Ethernet frame layer validates received echo frames fail-closed (ethertype, IPv4 header and checksum, protocol, ICMP checksum), the kernel injects an echo request at the same RX-processing boundary real frames cross, denies a tampered variant, and transmits the generated echo reply over the live virtio-net TX ring as a fourth device round addressed back through the wire-learned gateway. All three 0.4 live-networking evidence items are now on the wire: ARP resolution, an ICMP echo reply, and a forwarded TCP segment. QEMU evidence includes ANVAYA NET LIVE ICMP ECHO REPLY OK with rounds=4 asserted by smoke and the app demo.

Release v0.3.12 completes the live networking chain: a TCP SYN toward an off-link destination is addressed by the forwarding decision over the wire-learned neighbor - the frame's destination MAC is the ARP-resolved gateway link target, not a QEMU endpoint constant - and transmitted over the live virtio-net TX ring as a third device round with a fresh descriptor. Route resolution, neighbor miss, a real ARP request and reply, wire-resolved forwarding, and a forwarded TCP segment on the wire now all happen in one boot on one live device. QEMU evidence includes ANVAYA NET LIVE TCP FORWARDED OK with rounds=3 asserted by smoke and the app demo.

Release v0.3.11 closes the live ARP cycle: a fresh neighbor cache misses for the gateway and forwarding fails closed; the miss drives a second real ARP request out the virtio-net TX ring - an available-ring advance plus device notify, exactly how a production driver transmits its next frame - the reply arrives in the reposted RX buffer off the wire, the resolved neighbor enters the cache, and the retried forward succeeds with the live MAC. Two full TX/RX rounds on the same live device in one boot. QEMU evidence includes ANVAYA NET LIVE ARP CYCLE OK with rounds=2 asserted by smoke and the app demo.

Release v0.3.10 opens the 0.4 live-networking gate: the IPv4 routing table and neighbor cache are wired to the live virtio-net path. The neighbor entry is learned from the real ARP reply frame the device received from the QEMU network - the gateway MAC comes off the wire, not from proof constants - and forwarding produces complete frame-sendable decisions for an off-link destination through that wire-learned next hop and for the on-link gateway directly. A destination whose next hop was never ARP-resolved fails closed before any frame could be sent. QEMU evidence includes ANVAYA NET LIVE FORWARDING OK source=wire_arp asserted by smoke and the app demo.

Release v0.3.9 wires the audit core to real dispatch: every syscall audit event the dispatcher records now also lands in an append-only, SHA-256 hash-chained kernel audit trail - a bounded window with explicit overflow accounting that never blocks the syscall path. The end-of-boot continuity proof re-derives the full hash chain from genesis over the boot's live dispatch events, checks dense sequencing, and reads the first record through the capability-gated ordered window, confirming it is a real dispatcher event. QEMU evidence includes ANVAYA AUDIT SERVICE LIVE OK asserted by smoke and the app demo across a full boot of live dispatch activity.

Release v0.3.8 opens the 0.4 audit gate: a new anvaya-audit service crate implements an append-only, SHA-256 hash-chained, capability-gated audit log with an SDK-typed IPC surface. Every record is bound into a hash chain rooted in a fixed genesis, so any mutation, reorder, or splice of committed records is detected by re-walking the chain; the core exposes no mutation API besides append, sequences are dense, and reads return an ordered window. Append requires WRITE, reads require READ, and verification requires INSPECT - each denied fail-closed. The kernel proof drives appends, four rights denials, an ordered query window, chain verification, tamper and reorder rejection, and the typed IPC round-trip before ANVAYA AUDIT SERVICE OK, asserted by QEMU smoke and the app demo.

Release v0.3.7 completes the 0.4 storage-integrity gate's code surface: every remaining kernel content store and recovery path - the in-memory installer archive, the installer service's archived IPC dispatch and journal recovery, the trust journal archive, and the live storage-service store - now uses SHA-256, and the kernel no longer instantiates the deterministic proof hash anywhere. Content addresses across install, archive, replay, and service IPC are real SHA-256 digests end to end, verified on write and on replay with tamper rejection. QEMU evidence includes the new ANVAYA STORAGE SHA256 POLICY OK marker with proof_hasher_sites=0, and every existing marker re-verified green across smoke, demo, and the two-boot persistence scripts.

Release v0.3.6 completes SHA-256 on-disk integrity across all three persisted block artifacts: the live-package sector now carries a SHA-256 digest of its package region, and the disk read verifies the digest before signature verification even runs - a flipped on-disk byte is denied at both the digest layer and the signature layer. Together with v0.3.3 through v0.3.5, the package archive, the loader journal, and the live package are all SHA-256-verified on write and on replay, and content-store reads are integrity-checked. QEMU evidence includes the extended ANVAYA LIVE PERSISTED PACKAGE OK marker with digest_verified=1 and hash_tamper_denied=1.

Release v0.3.5 closes the read side of the storage-integrity loop: ContentStore::get_verified re-hashes stored bytes against the SHA-256 content address before returning them and fails closed with a new IntegrityViolation error, so a store whose backing bytes were corrupted after write can no longer serve silently damaged content. The block package-archive path now uses verified reads for both archived packages. Unit tests corrupt a stored byte and prove the plain read serves damaged bytes while the verified read refuses. QEMU evidence includes ANVAYA STORAGE READ VERIFIED OK asserted by smoke, demo, and both persistence boots.

Release v0.3.4 extends SHA-256 on-disk integrity to the loader-service journal: the persisted journal sector now carries a SHA-256 digest of its record region, and every replay - the same-boot write-readback and the cross-boot recovery - recomputes the digest over the restored bytes and fails closed on mismatch before any record is parsed. A tamper proof flips one on-disk record byte and shows the stored-digest comparison rejects it. Together with v0.3.3, both persisted block artifacts - the package archive and the loader journal - are now SHA-256-verified on write and on replay, with two-boot QEMU evidence including ANVAYA LOADER JOURNAL BLOCK HASH VERIFIED OK.

Release v0.3.3 lands the first Anvaya 0.4 storage-integrity slice: the virtio-blk package archive now uses SHA-256 as its on-disk integrity policy. The persisted 32-byte content ids are real SHA-256 digests of the archived package bytes, and both the same-boot write-readback path and the cross-boot replay path recompute and verify the digest before any package is accepted - journal recovery refuses records whose bytes do not hash to the recorded content id. A tamper proof flips one on-disk byte and shows digest verification and journal recovery both reject it fail-closed. Two-boot QEMU evidence asserts ANVAYA STORAGE BLOCK HASH VERIFIED OK on the second boot (and its absence on the first), with ANVAYA STORAGE BLOCK HASH OK and the tamper-denial marker on every boot.

Release v0.3.2 extends the production image loader to service-role images: an admitted service image derives its Service manifest fail-closed (non-service roles and images without a RECEIVE grant are rejected before any handoff) and registers with the init/service manager from the image-derived launch record. The QEMU proof denies a service image under the apps-only policy and a send-only service image at manifest derivation, then drives the full lifecycle - declare, start, running lookup with rights-gated resolve, scheduler dispatch, one RFC 0010 syscall in U-mode through the dispatch registry, clean task exit, stop, and retire - before ANVAYA PRODUCTION SERVICE LOADER OK and ANVAYA PRODUCTION SERVICE LOADER DENIALS OK, both asserted by QEMU smoke and the app demo.

Release v0.3.1 lands the first Anvaya 0.4 slice: the production image loader. A new AVPI process-image format carries real text and data segments, an entry offset, a stack requirement, and declared service dependencies inside a signed package, and the loader admits image bytes fail-closed - signature, launch policy, image format, and dependency availability are all verified before any resource is touched. The address-space layout and the scheduler launch record are derived from the admitted image and its launch grants instead of proof-seeded constants. The QEMU proof rejects a tampered signature, two malformed payloads under valid signatures, an over-capability image, and a missing-dependency image, then admits the signed image, maps its text/data/stack from the image bytes, and runs scheduler admit, dispatch, one RFC 0010 syscall in U-mode through the process dispatch registry, and a clean task exit, before ANVAYA PRODUCTION LOADER OK and ANVAYA PRODUCTION LOADER DENIALS OK, both asserted by QEMU smoke and the app demo.

Anvaya 0.3.0 is released: the first usable single-node developer-preview OS slice. The RISC-V nucleus boots in QEMU under OpenSBI, isolates real userspace processes through the RFC 0010 syscall boundary, runs a manifest-driven init/service manager with capability-protected IPC/storage/network services, and installs and executes signed WASM/WASI applications - including genuinely external rustc/LLVM-compiled modules and a WASI fd_write path. Also proof-backed: the full four-value-type bounded WASM interpreter, virtio-blk two-boot persistence, virtio-net/DNS/TCP, IPv4 routing with ARP forwarding and ICMP echo, and a SHA-256 (FIPS 180-4) content-address policy. Every claim is re-asserted by repeatable QEMU evidence across the cumulative v0.2.1 to v0.2.171 line.

Release v0.2.171 adds a real cryptographic content-address policy to the storage core: a bounded no_std SHA-256 (FIPS 180-4) implementation and a Sha256Hasher that addresses content by its full 32-byte digest, replacing the earlier deterministic proof hash. Unit tests verify SHA-256 against the published FIPS 180-4 vectors (empty, abc, and a two-block message) and confirm content addressing is deterministic and tamper-evident. The nucleus QEMU proof checks both NIST vectors, confirms deterministic addressing, and proves tamper evidence before ANVAYA STORAGE SHA256 OK. A cryptographic hash policy is now proof-backed.

Release v0.2.170 adds ICMP echo (ping) request/reply processing to the network core - the reachability primitive of an IP stack (gate 7). It encodes echo requests with a computed internet checksum, validates type/code/checksum on read, and turns a validated request into its type-0 reply echoing identifier, sequence, and payload with a fresh checksum. All bounded and fail-closed on bad type, bad checksum, and under/oversized messages. Two unit tests and the nucleus QEMU proof cover the request-reply round-trip, checksum validation, and denials before ANVAYA IP ICMP ECHO OK.

Release v0.2.169 ties routing to the link layer with an ARP/neighbor cache and a complete IPv4 forwarding decision (gate 7). A bounded Ipv4NeighborCache maps next-hop addresses to Ethernet addresses, and Ipv4RoutingTable::forward picks the route by longest-prefix match, resolves the next hop to a MAC, and returns a ForwardingDecision (next hop, link target, interface, on-link) - or NotFound on an ARP miss. Three unit tests and the nucleus QEMU proof cover the on-link and via-gateway forwarding chains and the ARP-miss path before ANVAYA IP FORWARDING OK. The route to next-hop to MAC to interface chain is now proof-backed.

Release v0.2.168 adds an IPv4 routing table with longest-prefix-match resolution to the network core - the core routing primitive for gate 7. A bounded Ipv4RoutingTable installs canonical CIDR routes (prefix, length, gateway, interface) and resolves a destination to a next hop by choosing the most specific matching prefix, falling back to a 0.0.0.0/0 default; on-link routes return the destination itself. It fails closed on non-canonical or over-long prefixes, a full table, and uncovered destinations. Two unit tests and the nucleus QEMU proof cover longest-prefix selection, default fallback, on-link resolution, and denials before ANVAYA IP ROUTING OK.

Release v0.2.167 runs the first WASI-targeted external toolchain module, combining external-module execution (gate 14) with capability-mediated WASI (gate 12). A genuinely rustc/LLVM-compiled fixture imports wasi_snapshot_preview1.fd_write, builds an iovec in linear memory pointing at a hello wasi data segment, and calls fd_write. A unit test proves it parses and fails closed under the deny-by-default host; the nucleus QEMU proof runs it under the same stdio capability as the hand-written stdio-write app, and the mediated fd_write reports 11 bytes written before ANVAYA WASM EXTERNAL WASI OK. A real external module now exercises the capability-mediated WASI path end to end.

Release v0.2.166 widens signed-package capacity: the kernel proof signature now encodes the signed-region length as a full u16 (both signature bytes) instead of a single length byte plus a marker, removing an artificial 255-byte cap on signed WASM modules while keeping the two-byte signature footprint so package sizes are unchanged. A third external rustc/LLVM fixture (261 bytes, over the old cap) has three functions where compute() calls triple()=3i and square()=i*i, summing to 154. A unit test and the nucleus QEMU proof both execute it to 154 before ANVAYA WASM EXTERNAL LARGE OK - realistic-size external modules can now be signed and run.

Release v0.2.165 broadens external-toolchain WASM coverage to inter-procedural calls. A second genuinely rustc/LLVM-compiled fixture has two functions: compute() loops i in 0..7 and calls a non-inlined triple(i)=i*3, summing to 63. LLVM emits a real loop/block/br_if/return in compute and a genuine call to triple, plus shadow-stack global.get and memory spills. A unit test and the nucleus QEMU proof both execute it to 63 before ANVAYA WASM EXTERNAL CALL OK. External compiler output now runs with cross-function control flow.

Release v0.2.164 executes a genuinely external toolchain-compiled WASM module - a real rustc/LLVM wasm32-unknown-unknown build (committed with source and provenance), not a hand-encoded array. This required WebAssembly globals support: the parser reads the global section, instantiation seeds a runtime globals array, and global.get/global.set execute with an immutable-global guard; the export parser now tolerates memory and global export kinds. The module's compute() sums i*3 over 0..7 == 63 via LLVM's closed-form lowering. A unit test and the nucleus QEMU proof both execute it to 63 before ANVAYA WASM EXTERNAL TOOLCHAIN OK - the first external-toolchain module to run on Anvaya.

Release v0.2.163 adds sub-width i32 memory access to the bounded WASM interpreter: i32.load8_s/load8_u/load16_s/load16_u and i32.store8/store16 - the byte/bool and 16-bit accesses that real toolchain-compiled WASM emits pervasively. Loads sign/zero-extend to i32; stores write only the low 1-2 bytes; all bounds- and page-limit-checked. A unit test proves store8 truncation, load8 sign/zero extension, store16, load16_u (total 4914) and load16_s sign extension (-1). The nucleus QEMU proof runs both modules over guest memory before ANVAYA WASM MEM NARROW OK, a concrete step toward executing externally compiled WASM modules.

Release v0.2.162 adds wide-type linear-memory load/store to the bounded WASM interpreter: i64.load/store, f32.load/store, and f64.load/store. i64/f64 use new 8-byte little-endian memory movers with the same bounds and page-limit checks as the i32 path; f32/f64 reuse the integer movers via bit reinterpret. A unit test proves a full 8-byte i64 round-trip (40<<32|2 == 42) plus f64 and f32 value round-trips. The nucleus QEMU proof runs both modules over guest memory before ANVAYA WASM MEM WIDE OK, asserted by smoke and the app demo.

Release v0.2.161 adds numeric type conversions to the bounded WASM interpreter: i32.wrap_i64, i64.extend_i32_s/u, f32/f64.convert_i32_s, f32.demote_f64, f64.promote_f32, and i32.trunc_f32_s (which traps on NaN and out-of-range inputs rather than saturating). A unit test routes 40 across all four value types and confirms 42, another proves zero-extension, and a third proves the NaN-truncation trap. The nucleus QEMU proof runs both round-trip modules before ANVAYA WASM CONVERT OK, asserted by smoke and the app demo.

Release v0.2.160 adds f64 double-precision support to the bounded WASM interpreter, completing the four numeric value types (i32, i64, f32, f64). f64 values use the full 64-bit stack slot as IEEE-754 bits, an 8-byte little-endian reader decodes f64.const, and f64.add/sub/mul/div plus f64.eq/ne/lt/gt/le/ge are implemented. A unit test proves 1.5 + 2.0 == 3.5 in f64, and the nucleus QEMU proof runs the module before ANVAYA WASM F64 OK.

Release v0.2.159 adds f32 floating-point support to the bounded WASM interpreter: f32 values occupy the low 32 bits of a value-stack slot as IEEE-754 bits, a 4-byte little-endian reader decodes f32.const, and f32.add/sub/mul/div plus f32.eq/ne/lt/gt/le/ge (yielding i32) run on the RISC-V hardware float unit. Two unit tests prove 1.5 + 2.0 == 3.5 and 2.0 < 1.5 == false, and the nucleus QEMU proof runs the addition module before ANVAYA WASM F32 OK.

Release v0.2.158 completes the i64 opcode set in the bounded WASM interpreter: div_s/div_u/rem_s/rem_u with divide-by-zero and i64::MIN / -1 overflow traps, and/or/xor/shl/shr_u, and ne/lt_u/gt_u comparisons. Unit tests prove full-width division (0x100000000 /u 2 == 0x80000000), a bitwise identity, and the divide-by-zero trap; the nucleus QEMU proof runs the division module before the updated ANVAYA WASM I64 OK marker.

Release v0.2.157 adds 64-bit integer value support to the bounded WASM interpreter: the value stack now holds 64-bit slots (i32 values occupy the low bits and i32 ops truncate/extend against that storage), a signed 64-bit LEB128 reader decodes i64.const, and i64.add/sub/mul/eqz/eq are implemented. A unit test proves 0x7fffffff + 0x7fffffff == 0xfffffffe in full 64-bit width, and the nucleus QEMU proof runs the same module before ANVAYA WASM I64 OK.

Release v0.2.156 completes the i32 integer opcode set in the bounded WASM interpreter with correct trap semantics: div_s/div_u/rem_s/rem_u enforce divide-by-zero traps and the i32::MIN / -1 overflow trap for div_s, plus shr_s and the signed and remaining comparisons. New unit tests cover division, the divide-by-zero trap, and remainder, and the nucleus QEMU proof adds a signed-package 84 /u 2 = 42 division module before the updated ANVAYA WASM RICHER OPS OK marker (19 i32 ops).

Release v0.2.155 widens the bounded WASM interpreter with i32.mul, i32.and, i32.or, i32.xor, i32.shl, i32.shr_u, i32.lt_u, and i32.gt_u (shift amounts masked to the operand width per spec). Two interpreter unit tests plus a nucleus QEMU proof package, sign, and execute modules computing 42 and 2 through the runner before ANVAYA WASM RICHER OPS OK. Arithmetic, bitwise, shift, and unsigned-comparison i32 ops now run on the interpreter.

Release v0.2.154 sources TCP retransmission timing from the real hardware timer: the retransmission proof reads the supervisor-timer counter (TIMER_TICKS, advanced by the timer interrupt) as its time base, arms a socket's retransmit deadline relative to that hardware base, and proves a poll at the base is pending while a poll at the base-relative deadline is due. Deterministic deltas over a real hardware time source keep the exact-match evidence harness intact, before ANVAYA LIVE TIMER RETRANSMIT OK.

Release v0.2.153 makes frame reclamation safe and automatic through cross-CSpace reference counting: FrameAllocator tracks per-frame reference counts, mem.map acquires a reference and mem.unmap releases one, and a frame is auto-reclaimed to the free-list only when its last reference drops, so a frame shared across address spaces is never reclaimed while still mapped. The QEMU proof drives the real map/unmap syscalls, holds a frame shared across three references, proves reclaim only on the final release plus reuse, and denies releasing an already-reclaimed or untracked frame, before ANVAYA FRAME REFCOUNT OK.

Release v0.2.152 promotes the frame allocator from bump-only to a production allocator with reclamation: FrameAllocator carries a bounded LIFO free-list, free() returns a frame for reuse, allocate() reuses a reclaimed frame before bumping, and reclamation fails closed on misaligned, out-of-range, and double-free inputs. The QEMU proof allocates five frames, frees three, proves LIFO reuse and reclaim accounting, and denies the three error classes before ANVAYA PRODUCTION ALLOCATOR OK. Frames are no longer permanently consumed on allocation.

Release v0.2.151 adds a live memory syscall over registered dispatch: task A allocates a frame through mem.frame_alloc from its registered dispatch context and the returned frame handle resolves in its kernel-owned CSpace with the requested READ|WRITE|MAP authority, before ANVAYA LIVE MEM SYSCALL OK. ABI, IPC, wait, task, and memory syscalls are all exercised on the live registered-dispatch path.

Release v0.2.150 proves the live IPC failure-audit path: a fail-closed send from the live client over registered dispatch is recorded as an audited failure, advancing the cumulative live audit to seven events with one failure and the last error reflecting the denial, before ANVAYA LIVE IPC DENIAL OK. Live IPC success and failure audit are now both asserted end to end.

Release v0.2.149 asserts the IPC audit surface end to end on the live path: at the end of the live two-task cycle the kernel-resident audit log holds exactly the six live IPC events with zero failures and the last audited task and syscall reflecting the final service reply, before ANVAYA LIVE AUDIT CONTINUITY OK. v0.2.148 also brought the full storage surface (put, get, namespace, list, object length) onto the live path.

Release v0.2.148 broadens the live storage surface: the live storage service performs a MANAGE-authority namespace bind, a READ-authority namespace resolve, a content listing, and an object-length query, with a namespace-put-without-MANAGE denial failing closed, before ANVAYA LIVE STORAGE NAMESPACE OK. Put, get, namespace, list, and object length now all run over the live dispatch substrate.

Release v0.2.147 completes live TCP over the dispatch substrate: a scoped-authority connect to 203.0.113.10:443 (ANVAYA LIVE TCP SOCKET OK), send/acknowledge/receive data transfer with rights checks (ANVAYA LIVE TCP DATA OK), and timer-driven retransmission with a bounded attempt counter (ANVAYA LIVE TCP RETRANSMIT OK), alongside the live DNS and NIC-RX-to-service paths.

v0.2.145 adds a Getting Started (Developer Preview) guide to the README: prerequisites, one-command verification for the unit tests and all three QEMU evidence scripts, a table of exactly what each script proves, and the interactive and panic boot paths, so a developer can reproduce every marker locally.

v0.2.143 brings a real device-received frame into service-layer state: the virtio-net RX proof binds the live ARP reply's sender IPv4 into a network-service DNS record and resolves it back under dns-allowed READ authority, with a dns-denied resolve failing closed, before ANVAYA LIVE NET RX SERVICE OK. v0.2.141 also brought the two guest-memory catalog apps onto the live service before ANVAYA LIVE GUEST MEMORY SERVICE OK.

v0.2.142 completes live-execution coverage of the whole app catalog: the live service now executes all twelve checked-in catalog apps over the live dispatch substrate — the ten non-guest-memory apps through SDK-derived launch plans and the two guest-memory apps through the guest-memory runner — with a completeness tally asserting the executed count equals the catalog size before ANVAYA LIVE CATALOG COMPLETE OK. Every v0.3 example app runs over the live service path.

v0.2.140 broadens the live catalog: each app's declared SDK capability profile is translated into package requirements and host grants, packaged, signed, and executed over the live service. write-log, dns-lookup, and clock-now join hello-status and read-config, so five catalog apps now run over the live dispatch substrate before ANVAYA LIVE SDK LAUNCH OK. v0.2.139 also brought WASI capability mediation onto the live path before ANVAYA LIVE WASI SERVICE OK.

v0.2.138 wires the live dispatcher, live service, and loader proofs across the full end-to-end evidence path: the reproducible v0.3 app demo now requires the eighteen live markers (process dispatch registry, sret-continue, auto-registration, kernel-owned CSpace and tables, live two-task scheduling, live init/service registry, live task IPC and wait, live storage/network/full-record/signed/WASM service cores, and loaded/signed-loaded/persisted image plus multi-frame stack dispatch), and the two-boot virtio-blk persistence check requires the persisted-package marker on both boots. Since CI runs all three evidence scripts, these proofs are re-asserted on every push. v0.2.137 also added production arbitrary multi-frame stack allocation.

v0.2.134 lands the loader convergence: live service task B executes entirely from a signed-loaded code frame — the signed native payload verifies under the kernel trust policy with a tampered variant denied before any mapping, loads into a fresh frame, and maps executable in B's kernel-owned address space — while B serves the complete live cycle from that page: registry-gated compact receive/reply, the bounded storage and network cores, the full-record authority-transfer exchange, and its scheduler exit before ANVAYA LIVE SIGNED SERVICE OK. A live registry-dispatched service running from signed-loaded code is the production loader-launched service shape named in the v0.3 milestone statement.

v0.2.130 completes the live-substrate service arc: two live tasks with distinct satp identities exchange registry-gated RFC 0010 IPC with capability transfer through kernel-owned dispatch, service task B runs the bounded content-addressed storage core (put/get roundtrip with a read-only-put denial before ANVAYA LIVE STORAGE SERVICE OK) and the bounded network core (MANAGE DNS insert, dns-allowed resolve, denied resolution before ANVAYA LIVE NETWORK SERVICE OK) over the live dispatch path, and the client observes completion via wait_one.

v0.2.121 ships sret-continue registry dispatch. Process dispatch registry entries now carry a bounded continue budget: registry-served U-mode ecalls dispatch through the registered context, advance sepc past the ecall, and sret directly back into U-mode without the supervisor trampoline. A three-ecall U-mode image proves two consecutive in-U-mode sret-continue resumes plus a trampoline return before ANVAYA PROCESS DISPATCH SRET CONTINUE OK, required by QEMU smoke.

A bounded kernel-resident process dispatch registry now maps active satp identities to per-process syscall dispatch contexts, and the real U-mode trap path resolves dispatchers registry-first. Registration denials and hit-counter continuity are proved before ANVAYA PROCESS DISPATCH REGISTRY OK.

irq_bind and irq_ack are proof-backed with a new Irq capability kind, MANAGE/RECEIVE bind authority, and monotonically increasing acknowledged sequences before ANVAYA SYSCALL IRQ BIND OK and ANVAYA SYSCALL IRQ ACK OK. Every syscall row in the RFC 0010 table is now proof-backed, with the ABI feature mask reporting bits=0x7ffffff.

RFC 0010 trap_return is proof-backed: a bounded three-word trap-return frame copies in through the translated user-copy window, subscription-gated cause validation applies, and the dispatch-context-bound pending trap is consumed on success before ANVAYA SYSCALL TRAP RETURN OK with five denial probes.

RFC 0010 trap_subscribe is proof-backed: RECEIVE endpoint authority, bounded trap-mask validation, held MANAGE-on-caller-task authority scanning, and a bounded subscription table with same-task mask update are proved before ANVAYA SYSCALL TRAP SUBSCRIBE OK with five denial probes.

RFC 0010 task_set_quota is proof-backed: a MANAGE TaskContext capability, bounded user-copy quota records, and scheduler budget application through a dispatch-context-bound SchedulerProof are proved before ANVAYA SYSCALL TASK SET QUOTA OK. The release also fixes a stale scheduler-loop count pin from v0.2.115 and makes QEMU smoke fail on any kernel panic in the normal boot log.

RFC 0010 cspace.alloc_slot is proof-backed with a new Reserved CSpace slot state, MANAGE-gated reservation, E_NO_SPACE exhaustion, and cspace.delete_slot reclaim with generation-bumped stale-handle denial, raising the scheduler-bound manifest loop to 37 dispatches.

Scheduler dispatchers now rebind through runner loader descriptors across startup-app exits, service IPC continuations, and shared-buffer paths, with service loader IPC continuity, wait, audit, and runtime aggregates compared across two persistence boots before ANVAYA SERVICE LOADER IPC CONTINUITY PERSISTENCE COMPARE OK.

Added a QEMU-visible storage startup app manifest proof for installed storage-roundtrip: ANVAYA STARTUP APP MANIFEST LOADER OK and ANVAYA STARTUP APP EXIT OK record process=0xa806, records=3, admitted=3, selected_priority=8, rights=0x41, state=syscall-returned, scheduler_state=running, status=9, and pending_waits=0 while production arbitrary loader-launched app execution remains future work.

Added a QEMU-visible network service reply wait-timeout proof for installed network-echo: ANVAYA WASM NETWORK SERVICE WAIT TIMEOUT OK records client=0xa803, service=0xb805, wait_token=0x815, wait_deadline=12, wait_state=timed-out, tick=12, expired=1, switches=2, pending_waits=0, client_state=running, and service_state=blocked while production loader-launched userspace services remain future work.

Added a QEMU-visible storage service reply wait-timeout proof for installed storage-roundtrip: ANVAYA WASM STORAGE SERVICE WAIT TIMEOUT OK records client=0xa804, service=0xb804, wait_token=0x814, wait_deadline=12, wait_state=timed-out, tick=12, expired=1, switches=2, pending_waits=0, client_state=running, and service_state=blocked while production loader-launched userspace services remain future work.

Added a QEMU-visible startup app service IPC cancel cleanup proof for installed network-echo: ANVAYA STARTUP APP SERVICE IPC CANCEL OK records client=0xa806, service=0xb701, reason=0xca17, cleared=1, audit=7, failures=1, send_generation=30, generation=32, launch_state=syscall-returned, and pending_waits=0 before terminal task_exit while arbitrary production loader-launched app execution remains future work.

Added a QEMU-visible startup app stale returned-handle denial proof for installed network-echo: ANVAYA STARTUP APP SERVICE IPC CALL DROP DENIAL OK records client=0xa806, service=0xb701, handle=0x1e0010000100005, syscall=0x201, error=bad-handle, audit=5, failures=1, launch_state=syscall-returned, and pending_waits=0 before terminal task_exit while arbitrary production loader-launched app execution remains future work.

Added a QEMU-visible startup app service IPC call returned-handle cleanup proof for installed network-echo: ANVAYA STARTUP APP SERVICE IPC CALL DROP OK records client=0xa806, service=0xb701, handle=0x1e0010000100005, dropped=1, error=stale, syscall=0x103, launch_state=syscall-returned, and pending_waits=0 before terminal task_exit while arbitrary production loader-launched app execution remains future work.

Added a QEMU-visible startup app service IPC call proof for installed network-echo: ANVAYA STARTUP APP SERVICE IPC CALL OK records client=0xa806, service=0xb701, transfer_rights=0x2, parent_cspace=0xc506, audit=4, launch_state=syscall-returned, and pending_waits=0 before terminal task_exit while arbitrary production loader-launched app execution remains future work.

Added a QEMU-visible startup app terminal exit proof for installed network-echo: ANVAYA STARTUP APP EXIT OK records process=0xa806 exiting after service reply/resume with status=10, launch_state=exited, scheduler_state=exited, current_idle=1, and pending_waits=0 while arbitrary production loader-launched app execution remains future work.

Added a QEMU-visible startup app service IPC reply/resume proof for installed network-echo: ANVAYA STARTUP APP SERVICE IPC REPLY OK and ANVAYA STARTUP APP RESUME OK record client=0xa806, service=0xb701, transfer_rights=0x2, parent_cspace=0xc506, wait_token=0x806, wait_state=completed, wait_data=0x2, pending_waits=0, and switches=3 while arbitrary production loader-launched app execution remains future work.

Added a QEMU-visible startup app service IPC-send proof for installed network-echo: ANVAYA STARTUP APP SERVICE IPC SEND OK records client=0xa806 sending to service=0xb701, transfer_rights=0x2, parent_cspace=0xc506, wait_token=0x806, selected_priority=5, and pending_waits=1 while service receive/reply for this startup-dispatched app and arbitrary production loader-launched app execution remain future work.

Added a QEMU-visible startup app manifest loader proof for installed network-echo: launch grants now feed a three-record init/service/application manifest, ANVAYA STARTUP APP MANIFEST LOADER OK records process=0xa806, records=3, admitted=3, selected_priority=8, asid=0xa106, cspace=0xc506, and state=syscall-returned while arbitrary production loader-launched app execution remains future work.

Added a QEMU-visible network service reply wait-token proof for installed network-echo: client=0xa803 now parks on wait_token=0x805 for service=0xb805, the service completes that token with the typed DNS reply length, the scheduler resumes the client with pending_waits=0, and the v0.3 app demo prints ANVAYA WASM NETWORK SERVICE WAIT TOKEN OK while production loader-launched service waits remain future work.

Added a QEMU-visible storage service reply wait-token proof for installed storage-roundtrip: client=0xa804 now parks on wait_token=0x804 for service=0xb804, the service completes that token with the typed storage reply length, the scheduler resumes the client with pending_waits=0, and the v0.3 app demo prints ANVAYA WASM STORAGE SERVICE WAIT TOKEN OK while production loader-launched service waits remain future work.

Hardened QEMU smoke failure reporting, widened the bounded virtio block poll budget, and revalidated the startup service reply wait-token proof on GitHub Actions: the release keeps the same proof markers for ANVAYA STARTUP SERVICE DISPATCH OK with wait_token=0x701, wait_deadline=8, pending_waits=1, ANVAYA STARTUP SERVICE IPC REPLY OK, and ANVAYA STARTUP INIT RESUME OK with wait_state=completed, wait_event=0xb701, wait_data=0x2, pending_waits=0, generation=18, and scheduler_state=running while production loader-bound service IPC remains future work.

Added a QEMU-visible startup service reply wait-token wakeup proof: after startup.claim_root/startup.finish and ipc.send, ANVAYA STARTUP SERVICE DISPATCH OK now records wait_token=0x701, wait_deadline=8, pending_waits=1 for service=0xb701, service replies with ANVAYA STARTUP SERVICE IPC REPLY OK, and ANVAYA STARTUP INIT RESUME OK now requires wait_state=completed, wait_event=0xb701, wait_data=0x2, pending_waits=0, generation=18, and scheduler_state=running while production loader-bound service IPC remains future work.

Added a QEMU-visible startup init resume proof: after startup.claim_root/startup.finish, startup init sends the service request through RFC 0010 ipc.send, service=0xb701 receives and replies with ANVAYA STARTUP SERVICE IPC REPLY OK, then the scheduler unblocks init, blocks the service, dispatches init again, and requires ANVAYA STARTUP INIT RESUME OK with switches=2, selected_priority=7, init_state=running, service_state=blocked, generation=18, syscall=0x0, and scheduler_state=running while production loader-bound service IPC remains future work.

Added a QEMU-visible scheduler-bound startup client IPC proof: after startup.claim_root/startup.finish, ANVAYA SCHEDULER PROCESS STARTUP HANDOFF OK records generation=7, the startup handoff stores the manifest init satp identity, resumes init from the syscall-returned launch table, sends the service request through RFC 0010 ipc.send before blocking init, records ANVAYA STARTUP SERVICE CLIENT IPC SEND OK for service=0xb701 with parent_cspace=0xc501, audit=1, generation=9, and scheduler_state=running, then requires ANVAYA STARTUP SERVICE DISPATCH OK at generation=10, ANVAYA STARTUP SERVICE UMODE ECALL OK at generation=12, and ANVAYA STARTUP SERVICE IPC REPLY OK with audit=3 and generation=16 while production loader-bound service IPC remains future work.

Added a QEMU-visible startup service client IPC send proof: after scheduler-bound init runs startup.claim_root/startup.finish, schedules the claimed manifest, starts and dispatches service=0xb701, startup init now sends the service request through RFC 0010 ipc.send under the stored init satp, transfers receive-only endpoint authority from parent_cspace=0xc501, records ANVAYA STARTUP SERVICE CLIENT IPC SEND OK with audit=1 and generation=7, then the same service receives and replies with ANVAYA STARTUP SERVICE IPC REPLY OK at audit=3 while production loader-bound service IPC remains future work.

Added a QEMU-visible startup service IPC reply proof: after scheduler-bound init runs startup.claim_root/startup.finish, schedules the claimed manifest, starts and dispatches service=0xb701, and that service returns abi.version, the same service now resumes under its stored satp, receives a transferred endpoint capability, replies with receiver-local authority, records ANVAYA STARTUP SERVICE IPC REPLY OK with transfer_rights=0x2, parent_cspace=0xc501, audit=2, generation=13, launch_state=syscall-returned, and scheduler_state=running while production loader-bound service IPC remains future work.

Added a QEMU-visible startup service U-mode ecall proof: after scheduler-bound init runs startup.claim_root/startup.finish, schedules the claimed manifest, starts service=0xb701, and dispatches it, the service now receives its own asid=0xa102 and cspace=0xc502, runs a mapped U-mode abi.version ecall, records syscall-returned launch state at generation=9, and requires ANVAYA STARTUP SERVICE UMODE ECALL OK with scheduler_state=running while production loader-bound service startup remains future work.

Added a QEMU-visible startup service dispatch proof: after scheduler-bound init runs startup.claim_root, schedules the claimed manifest, starts the service, and runs startup.finish, the startup launch table records init's syscall return, blocks init in the scheduler, dispatches service=0xb701 as the next running launch, and requires ANVAYA STARTUP SERVICE DISPATCH OK with generation=7, switches=1, selected_priority=8, init_state=blocked, launch_state=running, and scheduler_state=running while production loader-bound service startup remains future work.

Added a QEMU-visible startup manifest schedule proof: after manifest init runs startup.claim_root, the claimed launch table now admits the init and service records, registers and starts the service through the init manager, dispatches init first, and requires ANVAYA STARTUP MANIFEST SCHEDULE OK with admitted=2, ready=1, scheduler_ready=1, running_services=1, generation=5, and registry_generation=2 while production loader-bound service startup remains future work.

Added a QEMU-visible scheduler/launch-table-bound startup handoff proof: the manifest init process now runs startup.claim_root and startup.finish through the U-mode syscall path, validates the copied process-manifest ABI, returned root CSpace and init task handles, finish status, launch-table resume, and stored satp continuity, and requires ANVAYA SCHEDULER PROCESS STARTUP HANDOFF OK pid=0xa701 while the production loader-bound init path remains future work.

Added a QEMU-visible RFC 0010 startup handoff proof: startup.claim_root now copies and validates the process-manifest ABI from the caller's userspace window, returns root CSpace and init task handles, rejects nonce, length, version, reserved-argument, and duplicate claims, while startup.finish requires manage authority on the init task and rejects wrong-kind, reserved-argument, and duplicate finish paths. The proof-backed ABI feature bitmap is now 0x1fffff and QEMU requires ANVAYA SYSCALL STARTUP CLAIM ROOT OK, ANVAYA SYSCALL STARTUP FINISH OK, and ANVAYA SYSCALL DISPATCH FACADE OK entries=21 probes=83 while the production loader-bound init path remains future work.

Added a QEMU-visible RFC 0010 task_exit syscall proof: the nucleus now dispatches task_exit through the syscall facade, rejects nonzero reserved arguments, exposes the TASK_EXIT feature bit through the SDK and abi.features bitmap 0x7ffff, requires ANVAYA SYSCALL TASK EXIT OK and ANVAYA SYSCALL DISPATCH FACADE OK entries=19 probes=75, and proves terminal scheduler plus scheduler/launch-table-bound process exit state with ANVAYA SCHEDULER TASK EXIT OK and ANVAYA SCHEDULER PROCESS TASK EXIT OK while the production scheduler/loader-bound dispatcher remains future work.

Added a QEMU-visible RFC 0010 task_yield syscall proof: the nucleus now dispatches task_yield through the syscall facade, rejects nonzero reserved arguments, exposes the TASK_YIELD feature bit through the SDK and abi.features bitmap 0x3ffff, and requires ANVAYA SYSCALL TASK YIELD OK plus ANVAYA SYSCALL DISPATCH FACADE OK entries=18 probes=73 while the production scheduler/loader-bound dispatcher remains future work.

Added a QEMU-visible rights-checked service-registry resolution plus proof-harness endpoint IPC proof: the nucleus now resolves the running endpoint-receive service from the init/service registry, dispatches service=0xb803 through the scheduler, delivers an exact receive-only endpoint transfer with transfer_rights=0x2, marks it syscall-returned, and requires ANVAYA WASM SERVICE REGISTRY RESOLUTION IPC OK while production registry-routed userspace service IPC remains future work.

Added a QEMU-visible storage app package loader proof: the nucleus now 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 while production loader-launched userspace services remain future work.

Added a QEMU-visible installed storage runner proof: the nucleus now 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 while production loader-launched userspace services remain future work.

Added a QEMU-visible signed package signature denial proof: the nucleus now tampers the signed read-config bundle, proves runtime/anvaya-installer rejects it without recording an install, proves runtime/anvaya-runner rejects it before execution, and requires ANVAYA WASM APP SIGNATURE DENIAL OK while production trust-root and key policy remain future work.

Added an installed app package loader proof: the nucleus now derives application process-manifest rights from the installed network-echo package launch grants, dispatches it as application process=0xa803 through the launch table and scheduler proof, and requires ANVAYA WASM APP PACKAGE LOADER OK while production loader-launched userspace app execution remains future work.

Added a scheduler-bound cap.delegate proof: the scheduler/launch-table-bound manifest-loaded process delegates timer authority under the stored process satp, validates the narrowed child handle, parent slot, and rights, revokes the temporary proof handles, proves the returned child handle is denied as revoked in the same scheduler-bound process context, and now requires ANVAYA SCHEDULER PROCESS CAP DELEGATE OK pid=0xa313 plus ANVAYA SCHEDULER PROCESS CAP DELEGATE REVOKE OK pid=0xa313 in QEMU smoke while production arbitrary userspace loader integration remains future work.

Added a scheduler process wait-token proof: the scheduler/launch-table-bound manifest-loaded process now dispatches wait_one timeout, cancel_token, canceled wait, and completed wait outcomes under the stored process satp, revalidates launch-table resume between returns, and now requires ANVAYA SCHEDULER PROCESS WAIT TOKEN OK pid=0xa313 in QEMU smoke while production service-grade wait-token integration remains future work.

Added a process-bound cap.delegate RFC 0010 U-mode ecall proof: the nucleus runs cap.delegate under the mapped process satp, validates process-local CSpace authority, returns a narrowed timer-capability child handle, checks parent-slot lineage, revokes temporary proof handles, and now requires ANVAYA USER PROCESS CAP DELEGATE OK pid=0xa315 in QEMU smoke while the full reusable scheduler/loader-bound dispatcher remains future work.

Added a bounded DNS Ethernet frame proof: services/anvaya-net now wraps DNS-over-UDP/IPv4 packets in Ethernet frames with MAC and ethertype validation, the network-service core proof requires dns_eth_query=75 dns_eth_response=91 before ANVAYA NETWORK SERVICE CORE OK, and the live virtio-net TX proof requires ANVAYA VIRTIO NET DNS TX OK for a 75-byte DNS Ethernet frame while live TCP/IP state machines, timers, routing, and network service integration remain future work.

Added a bounded DNS-over-UDP/IPv4 packet proof: services/anvaya-net now wraps deterministic DNS A query/response packets in IPv4 and UDP headers, validates IPv4 header checksums and UDP pseudo-header checksums, fails closed on malformed packet shapes, ports, addresses, protocols, and short outputs, and the nucleus QEMU proof requires dns_udp_query=61 dns_udp_response=77 before ANVAYA NETWORK SERVICE CORE OK while live TCP/IP state machines, timers, routing, and network service integration remain future work.

Added a bounded DNS A packet proof: services/anvaya-net now writes and parses deterministic DNS A query/response packets, uses an answer-name compression pointer so maximum valid names fit inside the 512-byte bound, fails closed on malformed packet shapes, and the nucleus QEMU proof requires dns_query=33 dns_response=49 before ANVAYA NETWORK SERVICE CORE OK while live TCP/IP and DNS-over-UDP/IP service integration remain future work.

Added a live virtio-net RX proof: the nucleus configures QEMU virtio-net RX queue 0 with a writable DMA packet buffer, triggers the deterministic ARP request through TX queue 1, waits for TX and RX used-ring completion, validates zero-length TX completion plus the returned ARP reply from 10.0.2.2 to 10.0.2.15, and leaves full TCP/IP packet handling and network service integration as future work.

Added a live virtio-net TX proof: the nucleus configures the QEMU virtio-net transmit queue, DMA-submits a deterministic ARP/Ethernet frame through the bounded virtqueue path, waits for used-ring completion, validates healthy device status and interrupt state, and leaves virtio-net RX plus full TCP/IP packet handling as future work.

Added a live storage-block package restore proof: the nucleus archives the signed network-echo WASM package through the storage core, writes it to QEMU virtio-blk sector 2, reads it back, revalidates the content and package ids, reinstalls the restored bytes, and launches the restored installed record.

Added a two-boot virtio-blk exact-pattern persistence proof: the nucleus validates the deterministic sector-1 proof pattern byte-for-byte, the QEMU script reuses one raw block image across two completed boots, and storage/package service integration remains planned.

Added a live virtio-blk write/read-back proof: the nucleus writes a deterministic sector-1 pattern to QEMU virtio-blk, reads it back through the bounded virtqueue path, and keeps block persistence across separate QEMU runs planned.

Aligned the core docs, public site, LLM surfaces, changelog truth claims, and search index around the scheduler-bound revoked-endpoint audit evidence: eight events with two failure records, while preserving search recall for the literal audit=8 transcript marker.

Extended the scheduler/launch-table-bound manifest process loop with a delegated-child revoked-endpoint ipc.send failure before memory dispatch, preserving launch-table resume validation, preserved queued request state, no reply mutation, failure-closed Revoked results, and audit evidence: eight events with two failure records.

Extended the scheduler/launch-table-bound manifest process loop to cap.identify, ipc.send, ipc.receive, ipc.reply, ipc.call, ipc.cancel, mem.frame_alloc, mem.map, mem.unmap, and cap.revoke with checked launch-table resume, scheduler-bound pending-request cancel clearing, empty cancel idempotence, cumulative IPC audit=7 validation, and the existing send/receive/reply/call, mapping, unmap, and revoke proof coverage.

Extended the scheduler/launch-table-bound manifest process loop to cap.identify, ipc.send, ipc.receive, ipc.reply, ipc.call, mem.frame_alloc, mem.map, mem.unmap, and cap.revoke with checked launch-table resume, translated send, receive, reply, call-request, and call-reply window validation, endpoint queue delivery, transferred timer capability checks, returned endpoint and device-frame capability evidence, cumulative send+receive+reply+call IPC audit success validation, scheduler-bound bad-length ipc.call failure/audit validation with reply_preserved=1, and the existing mapping/unmap/revoke proof.

Extended the scheduler/launch-table-bound manifest process loop to cap.identify, ipc.send, ipc.receive, ipc.reply, mem.frame_alloc, mem.map, mem.unmap, and cap.revoke with checked launch-table resume, translated send-request, receive, and reply-request window validation, endpoint queue delivery, transferred timer capability checks, returned endpoint capability field evidence, cumulative send+receive+reply IPC audit success validation, and the existing mapping/unmap/revoke proof.

Extended the scheduler/launch-table-bound manifest process loop to cap.identify, ipc.send, ipc.receive, mem.frame_alloc, mem.map, mem.unmap, and cap.revoke with checked launch-table resume, translated send-request and receive-window validation, endpoint queue delivery, transferred timer capability checks, cumulative send+receive IPC audit success validation, exact receive capability field evidence, and the existing mapping/unmap/revoke proof.

Extended the scheduler/launch-table-bound manifest process loop to cap.identify, ipc.send, mem.frame_alloc, mem.map, mem.unmap, and cap.revoke with checked launch-table resume, translated send-window validation, endpoint queue delivery, transferred timer capability checks, IPC audit success validation, and the existing mapping/unmap/revoke proof.

Extended the scheduler/launch-table-bound manifest process loop to cap.identify, mem.frame_alloc, mem.map, mem.unmap, and cap.revoke with checked launch-table resume, mapping handle resolution, page-table entry validation, explicit unmap proof, stale mapping-handle denial, and frame revocation.

Added a launch-table resume contract and widened the scheduler/launch-table-bound manifest process proof from cap.identify to a cap.identify, mem.frame_alloc, and cap.revoke loop with checked scheduler task, Sv39 satp identity, transient frame authority, and frame revocation.

Added a scheduler/launch-table-bound U-mode cap.identify syscall proof for a manifest-loaded process, reusing the stored Sv39 satp identity and running scheduler-task binding, rejecting wrong trap records in host tests, asserting a new QEMU marker, and refreshing v0.3 status evidence.

Added a scheduler/launch-table-bound manifest init entry and return proof that binds the launch record to a running scheduler task and stored Sv39 satp identity, rejects stale scheduler or satp drift in host tests, emits a QEMU proof marker, and refreshes v0.3 status evidence.

Added a reusable process-bound U-mode syscall runner for mem.frame_alloc, mem.map, mem.unmap, and cap.revoke under active process satp, validating transient frame authority, mapping authority, page-walk resolution, stale mapping-handle denial, and frame revocation.

Mapped the manifest-declared init stack, materialized text plus stack leaves in owned Sv39 tables, ran a stack-touching ABI-version U-mode ecall under the process satp, preserved trapped user sp through the sscratch trap path, and denied a third distinct L0-table bucket at map time.

Connected the parsed process manifest to the init launch path, dispatched the init process first, ran an ABI-version U-mode ecall from the manifest entry under process satp, and marked the launch record syscall-returned while keeping production stack materialization planned.

Added a bounded byte-backed process-manifest ABI parser with magic/version validation, fixed init/service records, role and right decoding, reserved-bit denial, empty-manifest denial, atomic launch-table loading, host tests, and QEMU smoke assertions.

Added executable process-manifest handoff evidence, a v0.3 goal gate document, U-mode ecall proof expansion, bounded scheduler semantics, bounded init/service-manager semantics, owned page-table materialization, satp activation/restore, and process-bound syscall proof paths.

Added a proof-backed RFC 0010 dispatch facade for ABI version, capability, IPC receive/call/reply, and memory calls, including malformed-rights denial and revoke-driven mapping invalidation, plus Sv39-shaped PTE records in the staged memory mapping proof while keeping U-mode ecall dispatch and satp switching future work.

Accepted RFC 0007 as the software CSpace and handle representation contract, freezing per-task CSpaces, slot/generation/lineage metadata, opaque u64 handle format 0x1, IPC import/export, revocation, stale-handle failure, CHERI mapping, and software fallback while keeping CHERI sealed-handle encoding future profile work.

Accepted RFC 0002 as the Agent Execution Context semantic model and aligned status, traceability, acceptance, roadmap, glossary, and public mirrors around accepted AEC semantics with runtime implementation still planned.

Accepted RFC 0010 as the first userspace/Nucleus syscall contract and aligned status, traceability, roadmap, and public mirrors around the frozen ABI boundary.

Denied requested or invalid page rights, added host-side permission tests, and extended staged frame revocation evidence across producer and auditor CSpaces/address spaces.

Added the first capability-backed memory-isolation proof slice with frame caps, task-owned CSpaces, staged address spaces, map/unmap, revocation invalidation, stale mapping failure, and page-fault evidence.

Published local site mirrors for the vision traceability and 1.0 acceptance matrices so the public docs page does not depend on private GitHub blob visibility.

Filled RFC 0001 and RFC 0002, added RFC 0006-0031 as draft contracts, and published draft vision traceability plus 1.0 acceptance matrices.

Moved the public site and nucleus proof workflows to Node 24-backed GitHub Actions pins after the v0.1.6 release validation.

Tightened object-family lineage, metadata validation, parent-slot revocation, lineage isolation, slot reclamation, and route-check CI coverage for the capability table proof.

Added a bounded internal capability table with slots, lineage, rights, object metadata, narrowed two-task delegation, and table-backed parent/derivative invalidation evidence.

Added executable evidence for endpoint capability attenuation, no-amplification, delegated IPC transfer, and parent/derivative revocation.

Accepted RFC 0004, added explicit IPC failure-path evidence, widened DTB-backed inventory, and added a second task-context request/reply slice.

Published the verified first-light proof bundle, accepted the boot-path RFC, and added a prototype child-task timer/IPC handoff slice.

Published the implementation-status page and added the first-light RISC-V/QEMU nucleus scaffold to the main repository.

Added structured data, machine-readable files, and documentation pages.

Initial public release of the ANVAYA OS website and manifesto.

The ANVAYA Manifesto is published as the core reference document.