Update log

Anvaya v1.7.0 ("Capability Sockets") is released. A socket is now a capability carrying kind, resource identity, rights, and generation rather than an in-process index: NetworkAuthority's two unauthenticated constructors are gone and from_capability is the only way to obtain network authority anywhere in the tree. The bypass that made this load-bearing is closed — validate_net_ipc_capability checked resource id and lineage only when the authority carried metadata, so an ambiently-built authority skipped identity binding entirely, and a pre-existing test asserted that bypass succeeded; its expectation inverts with the fix. Socket handles pack (generation << 24) | index, so a handle held across a task restart is refused as stale instead of silently addressing whatever socket now occupies its index, and StaleSocket stays distinct from BadSocket end to end. Network IPC wire v2 adds SocketBind (MANAGE, port-range checked, with port theft as its own PortNotGranted denial) and SocketClose, preserving v1 operation numbering; NetworkAuthority::attenuate narrows rights, ports, and DNS permission, refuses every widening direction, and is transitive. Extraction #5 ships services/anvaya-net-task as the fourth image in an AVDB 1.2 bundle (header 128 → 160 bytes, with four format denials proven including a zero-length fourth package that would otherwise parse as a successful boot), admitted as PackageRole::Service with its own pid, CSpace, and SATP. The task persists its DNS cache and socket table across dispatches, serves typed requests over real kernel IPC with delegated frames and per-request capability drop, proves five denials (wrong resource, insufficient rights, foreign lineage, stale generation, and a stale generation after restart), and survives its own death with a fresh-generation replacement at a distinct pid. Frames the task composes transit a real device: a task-built ARP request relayed to the signed v1.5 U-mode virtio-net driver draws a real ARP reply — 74 bytes, opcode 2, sender 10.0.2.2, target 10.0.2.15, checked field by field — with wire_irqs=1 and polling=0, the task holding no device capability and the driver holding no network policy. Mesh object sync crosses those capability sockets between two distinct client tasks and is accepted by ContentStore::accept_synced under its content-address check; only pairing, routing, and delegation still use the in-memory wire. Product core compiles zero network-service names: core 20,757 → 20,740 lines, total nucleus/src 21,469, combined privileged TCB 22,379 → 22,362, the privileged transport extension byte-identical at 1,622 lines / 7 unsafe. The marker oracle is diff-empty at 1,425 markers / 68 spec rows and a new scripts/check-net-service.sh binds every accepted marker to task pid/SATP/generation provenance. RFC 0032 is Accepted. Honest scope: this is QEMU-proven and not a delivered network stack — socket payloads do not leave the machine, reaching their reader through the service's own receive queue (transport=service-loopback, which the focused gate refuses to let drift into transport=wire), so manifesto M8 advances DEBT → PARTIAL and not DELIVERED; TCP and UDP over the wire, DNS over the wire, ICMP echo end to end, congestion control, IPv6, and TLS remain planned areas of accepted RFC 0032; and no physical hardware or external audit is claimed.

Anvaya v1.6.0 ("Content-Addressed Storage") is released. A hybrid-signed storage service runs as a distinct scheduled U-mode task — its own CSpace, page tables, SATP, and multi-page stack — with no device authority; clients in other address spaces call it over real kernel IPC with a delegated frame plus their own LocalObject authority, and the task drops both imported capabilities per request. Content is addressed by algorithm-tagged SHA3-256 over bounded, domain-separated Merkle object trees (256-byte chunks, 8 maximum), and the capability-checked namespace is a last-writer-wins CRDT with explicit tombstones whose dominance is the strict total order (lamport, actor, tombstone, algorithm, id); four new Kani harnesses take the repo total 25 → 29. The task authors and validates its own DriverMessageV1 records through the frozen v1.5.2 block client, relayed to the signed U-mode virtio-block driver with kernel_fallbacks=0, and commits an AVCS A/B snapshot (header LBA 128, slots 129 and 137); boot two recovers boot one's committed objects off disk and re-verifies every content id under SHA-3 before serving. Nine denials are proven, including an authority kind refused at the IPC boundary, a one-byte disk tamper that fails recovery closed and then succeeds once repaired, and task death with exactly one terminal client result plus fresh-generation recovery. Extraction #4 leaves zero storage-service names in product core: product core 21,870 → 20,757 lines, total nucleus/src 22,581 → 21,476, combined privileged TCB 23,492 → 22,379, the privileged transport extension byte-identical at 1,622 lines / 7 unsafe, and nucleus-model's 3,037 non-test lines measured separately; manifesto M6 advances DEBT → PARTIAL. The marker oracle is diff-empty at 1,424 markers / 68 spec rows, a new four-lane scripts/check-storage-service.sh gates the service, and the 32,960-byte storage image ships as the third image in a 66,567-byte AVDB 1.1 bundle. RFC 0020 is Accepted and RFC 0028 carries an accepted A1 hash-policy amendment. Honest scope: this is QEMU-proven and not a production filesystem — the store is four bounded object slots over a 1 KiB arena with four namespace registers, snapshots and garbage collection are accepted-but-open areas of RFC 0020 (the arena does not reclaim), sync is local-first only with no transport or peer discovery until 1.7, the inherited SHA-256 surfaces (audit chains, AEC digests, package/archive digests, protected-monitor tip, installer archive) keep SHA-256, QEMU persistence across a clean reboot is not a power-cut test, and no physical hardware or external audit is claimed.

Anvaya v1.5.2 ("Durable Block Client") is released. The kernel-private virtio-block client is lifted into a reusable, capability-scoped adapter (Read/Write/Flush over the existing Driver ABI, data only in delegated shared frames, generation-aware stale denial). AEC journal/effect/audit codecs and the installer package archive persist through that durable block client onto one exclusive proof-disk sector map; QEMU proves two-boot survival as the adapter's callers with polling=0 and kernel_fallbacks=0. Product core is 21,870 lines and the counted privileged TCB (product core + transport extension) is 23,492. SHA-3, Merkle, CRDT, namespace redesign, and storage-service extraction remain 1.6. No physical-hardware or IOMMU-backed DMA-isolation claim is made.

Anvaya v1.5.1 is a correctness and enforcement patch over v1.5.0 "Driver Domains," from a full post-release review. IRQ delivery no longer wedges a claimed PLIC source on a stale-endpoint interrupt; the product-core device-unsafe ratchet is restored; the virtio-block and virtio-net drivers use checked arithmetic on buffer_offset; and the virtio transport used-ring acquire fence is corrected for weak-memory ordering. QEMU proves the same interrupt-driven completion with polling=0 and kernel_fallbacks=0. Product core stays 21,834 lines; the privileged transport extension grows to 1,622 lines for the fence fix, so combined privileged TCB is 23,456, still below the release ceiling, and the 1,417-marker oracle is diff-empty.

Anvaya v1.5.0 ("Driver Domains") is released. Hybrid-signed virtio-block and virtio-net drivers execute as distinct scheduled U-mode tasks with capability-scoped device, DMA, IRQ, and IPC authority. QEMU proves interrupt-driven completion with polling=0 and kernel_fallbacks=0, two-boot block persistence, forced-death cleanup and restart, and opaque-frame net reuse. The no-IOMMU transport extension is separately verified and measured; this is not a physical DMA-isolation claim. The third Nucleus extraction lowers product core to 21,834 lines and combined privileged TCB to 23,452, while the 1,417-marker oracle remains diff-empty after an explicit old-path migration. FML13V01 remains Buildable, not physically boot-verified.

A site-only release — the kernel is unchanged at v1.4.1 ("Verify-Only Kernel"). The anvaya.dev layout is now responsive from 320px phones to ultrawide monitors, built on shared Container and PageHeader components instead of per-page wrappers. Copy is layered: plain language first, developer detail second, with the homepage hero cut to a short introduction and a compact current-release blurb. The status page's wall paragraphs are restructured into a scannable current-release section plus a per-release history, preserving every release's facts and honest-scope notes. The sharp-rectangle design rule is now enforced in typography as well (zero border radius on code, pre, and blockquote).

Anvaya v1.4.1 ("Verify-Only Kernel") is released — a user-authorized 3-cycle relocation follow-through closing v1.4.0's one honest miss (nucleus_lines < 26,851, the V1_4_GOAL.md definition-of-done item 2 target), via the dependency-crate relocation mechanism the v1.4.0 floor analysis had overlooked — the same move v1.2 used (AEC persistence → anvaya-aec, virtio-net TX → anvaya-virtio). Three relocations, no behavior change. First, the package signing path — all three write_signed_* writers, kernel_package_pqc_sign, and both signing seeds — moves to a new anvaya-package proofsign module, making nucleus/src verify-only: no signing code, no signing seeds, while KernelProofSignature and both pinned public keys stay. Second, the launcher decision logic (dispatch_launch_service_request and its with_args_and_memory sibling, plus LaunchServiceError) moves to anvaya-runner beside run_installed_wasm_package. Third, the energy broker's service-side dispatch convention (opcode→export selection, request-word argument layout, instantiate/invoke) moves to anvaya-wasm-apps beside ENERGY_BROKER_SERVICE_WASM, completing what the v1.1.0 energy extraction started — the kernel keeps the capability checks and the reply. Outcome: nucleus_lines 27,043 → 26,848, under the original 26,851 target — met, not amended; core_lines 25,801 → 25,606, below even the v1.3.6 pre-release 25,616; CORE_CEILING machine-lowered 25,801 → 25,622 → 25,606, no amendment needed — the arc only shrank. The lines did not get denser or hidden: the kernel source genuinely stopped containing signing logic, launcher business logic, and one service's dispatch convention. Transcript byte-exact throughout (1,572-marker oracle, diff=empty every cycle); cargo build/test, check-qemu-boot.sh, check-harness-markers.sh, and check-manifesto-alignment.sh green each cycle. Builds on v1.4.0 "The Real Launcher."

Anvaya v1.4.0 ("The Real Launcher") is released — the first release to run the 1.3.x RSI discipline against a manifesto-anchored feature gate instead of pure proof-harness compression, across three independent gates. Gate A gives LoaderServiceAuthority a real from_capability constructor (CapabilityKind::LocalObject + Rights::INVOKE at a dedicated resource id, replacing an unauthenticated ::new() at every production call site) and a real SYSCALL_LAUNCH_REQUEST a running process can invoke, handing off to a launcher service process over the same dispatcher/Endpoint machinery the audit-service proof already used (ANVAYA LAUNCH SYSCALL OK, plus fail-closed denials for a missing capability, wrong resource id, and wrong rights). Gate B serves anvaya-audit's append/verify logic as a launched WASM service over that syscall — the second nucleus extraction, retiring the in-kernel exec_audit_service_dispatch path the harness previously drove directly (ANVAYA AUDIT LAUNCH DISPATCH OK). Gate C makes the per-app package envelope a genuine Ed25519+ML-DSA-65 hybrid — both halves verified independently and combined through the existing hybrid_signature_verdict fail-closed combinator, denying a classical-only downgrade, a forged-classical half, and a forged-PQC half alike (WASM_APP_PACKAGE_BYTES 3,261 → 6,570; ANVAYA PACKAGE SIGNATURE OK, denials 4 → 7) — closing the last classical holdout the manifesto's PQC-by-default commitment named. The package envelope's growth broke six size assumptions only a live QEMU boot caught (virtio-blk sector capacity/collisions, ContentStore/StorageAuthority sizing, guest-memory page-window chunking, stale signature-offset boundaries, and a check-script regex too narrow for the larger chunks= count), all found and fixed; a retroactive Gate B oversight (a stale retired-marker assertion across three scripts) was fixed alongside it. CORE_CEILING 25,616 → 25,801, HARNESS_TOKENS 47,312 → 48,087, both amended and logged. Manifesto M2 (PQC the default for all cryptographic operations) moves PARTIAL → DELIVERED; M7 (WASM Application Runtime) stays PARTIAL — its specific launch-mechanism gap is closed, but the three other WASI extension points (Intent, Intelligence Broker, Energy) remain unscheduled, honestly rescoped rather than claimed complete; M1 records its second nucleus extraction. Not met: nucleus_lines ends the release at 27,043, above the pre-release 26,851 baseline — one extraction was never going to outrun two new kernel mechanisms on line-count arithmetic alone, reported honestly rather than dropped. Harness marker oracle byte-exact throughout: 1,572 markers, diff=empty. Builds on v1.3.6 "Honest Core/Harness Accounting."

Anvaya v1.3.6 ("Honest Core/Harness Accounting") is released — no functional kernel change. check-manifesto-alignment.sh only ever counted main.rs + src/harness/ + src/core/; four files declared via lib.rs's own pub mod tree — lib.rs's non-test body itself, plus hardware.rs, rt.rs, and platform.rs — sat outside all three, invisible to the ratchet since whenever src/core/platform.rs was first extracted in the v1.3.0 era, all reachable from the kernel [[bin]] target and none dead code. All 5,363 uncounted lines classified by live call-site tracing rather than import presence, catching traps both ways: SchedulerProof/InitServiceManager are core despite "Proof" naming (real dispatch call sites in core/services.rs/core/sched.rs), while the signed-package ProcessImage admission pipeline is harness despite sounding equally load-bearing (zero call sites in core/*.rs). Physically relocated all four across four RSI cycles, finding and fixing a second, independent, pre-existing Rights type already living in core/nucleus.rs (resolved at the re-export layer only) and a real, pre-existing latent CHILD_STACK stack-overflow bug exposed — not introduced — by the pure code motion (core/process.rs's EnergyServiceRequest handler runs a WasmInstance directly on a 4,096-byte task stack with no overflow guard, already a tight fit; widened to 16,384 bytes). lib.rs shrinks 5,638 → 3,050 lines (non-test body: 2,653 → 64, now pure #[path] wiring); CORE_CEILING 21,157 → 25,616, HARNESS_CEILING 239 → 1,235, HARNESS_TOKENS 43,896 → 47,312, each amended once with a logged MANIFESTO_ALIGNMENT.md justification. Every source file the kernel binary compiles is now counted by exactly one of the two ceilings — no third, invisible bucket. Boot transcript byte-identical throughout (ANVAYA HARNESS MARKER ORACLE OK markers=1571 spec_rows=73 diff=empty, unchanged). Builds on v1.3.5 "RSI on the Verifier."

Anvaya v1.3.5 ("RSI on the Verifier") is released — a scripts-only patch, no functional kernel change. The three shell proof scripts (check-qemu-boot.sh, demo-v0-3-apps.sh, check-virtio-blk-persistence.sh) carried 566+ inline grep marker-assertion call sites, one hand-written line per boot marker — the same row-shaped-logic-disguised-as-repeated-code pattern that justified the 1.3.1→1.3.2 harness dissolution, one layer up the stack. All of them now go through a new shared scripts/lib/assert-markers.sh as one declarative row per check, gated by a new self-tightening SCRIPTS_LINES/SCRIPTS_TOKENS ratchet (2406→2362 lines, 43005→42670 tokens). check-qemu-boot.sh carried the real yield: 114 of its 125 named marker-pattern variables were referenced exactly once, so define+assert collapsed to a single inlined row, verified by independently re-sourcing the original variable chain in real bash before any line was deleted. Differential-verified against 33 honest+corrupted fixture logs, catching one real bug: three absence-checks written as bare top-level "! grep -q ..." were silently non-enforcing under set -e (bash exempts top-level negation from errexit); assert_row_absent closes it. nucleus/src/ untouched throughout, confirmed by the byte-exact harness oracle (ANVAYA HARNESS MARKER ORACLE OK markers=1571 spec_rows=73 diff=empty, unchanged) and nucleus/src/manifesto_ledger.rs regenerating with a 0-line diff every cycle. Builds on v1.3.4 "Version Banner Fix."

Anvaya v1.3.4 ("Version Banner Fix") is released — a one-line, no-functional-change patch. The boot banner and the interactive-shell about/ver/version/banner command both hardcoded the tagline "QEMU-Proven Milestone" next to the printed version number; that was v1.0.0's actual release name, but every release since has had its own name, so the banner had been claiming a stale title since v1.1.0. Both call sites now print just "ANVAYA OS v{version}". Neither call site is part of the automated boot marker set, so the byte-exact harness marker oracle is unaffected (ANVAYA HARNESS MARKER ORACLE OK markers=1571 spec_rows=73 diff=empty); HARNESS_TOKENS is machine-lowered 43,898 → 43,896 as a side effect of the trimmed string literal, no other ratchet moves. Full QEMU boot smoke and the manifesto alignment gate re-verified green before tagging. Builds on v1.3.3 "Truth-Parity Restoration."

Anvaya v1.3.3 ("Truth-Parity Restoration — Changelog & Status Backfill") is released — a documentation-only patch, no functional kernel change. The "update every release-doc mirror" step had silently lapsed for three releases running (v1.2.0 → v1.3.2): anvaya/CHANGELOG.md gains the v1.3.2 section that was never written despite the tag, GitHub release, and Cargo.toml version bump all pre-dating this fix, and anvaya/STATUS.md's "Current release" banner — stuck on v1.3.0 — now reflects v1.3.2's actual state. On the site side, content/changelog.json gains the v1.3.1 entry it had skipped (this JSON had jumped straight from v1.3.0 to v1.3.2), and the five public truth-parity mirrors flagged red by npm run check:truth — public/changelog.md, public/status.md, public/index.md, public/llms-ctx.txt, and public/llms-full.txt — are caught up through v1.3.2 and this release; the last two had drifted since v1.1.1, four releases behind. check:truth, check:llms, check:links, and check:routes are all green. Builds on v1.3.2 "Dissolve the Proof Bodies."

Anvaya v1.3.2 ("Dissolve the Proof Bodies — Spec Rows · Shared Interpreters · Honest Floor") is released — the proof harness sheds its last hand-written code. Every one of the 119 pub fn run_* proof bodies under nucleus/src/harness/ is dissolved into declarative spec rows executed by shared interpreters (dsx/dsxr op-row engines with register files, kvf/kvm piecewise marker emitters, qz!/capv/wcx dense row tables), so HARNESS_BODIES ratchets 119 → 0 — machine-lowered and gate-enforced — and new proofs arrive as rows, not code. The harness driver falls 506 → 239 lines and HARNESS_TOKENS falls 153,946 → 43,898 whitespace-delimited tokens (3.51×) across 24 commits (2026-08-02 → 2026-08-03), with the boot transcript byte-identical throughout: the 1,571-marker oracle stayed diff-empty across 23 green cycles and caught 2 boot-breaking bugs and 4 marker regressions along the way. Honest scope: the goal's 5× token target (≤30,789) was not met; it was amended by a logged MANIFESTO_ALIGNMENT.md amendment to the measured honest floor of 43,898 after an adversarial audit (evidence/V1_3_2_TOKEN_FLOOR.md) showed the residual consists of stdout-oracle-frozen marker text, spec-row data, and the interpreters themselves — closable only by whitespace-stripping or golf macros that would fake the metric the ratchet exists to protect (one such 24,604-token build was constructed, rejected, and reverted on principle). HARNESS_TOKENS is pinned at the floor and remains machine-lowered, never raised. Builds on v1.3.1 "100× the Proof Harness" (55,254 → 506 harness lines, 73-row spec ladder, byte-exact marker oracle, HARNESS_CEILING).

Anvaya v1.3.1 ("100× the Proof Harness — Spec Tables · Byte-Exact Oracle · RSI") is released — the proof suite compresses itself the way v1.3.0 compressed the kernel. nucleus/src/harness/ shrinks from 55,254 to 506 lines (109×; target was 100×/≤553) across 9 proof-gated RSI cycles, with zero markers deleted or reworded and zero proofs weakened. The boot proof ladder becomes declarative: nucleus/src/harness/spec.rs holds 73 spec rows — Spec { name, expected marker, invariant fn } over a shared SpecCtx (boot info, resource inventory, child task, virtio transports, net-retransmit proof) — executed in exact boot order by one table-driven driver, run_specs; main.rs's two ladder blocks collapse into two driver calls (539 → 470, MAIN_CEILING machine-lowered). A new byte-exact oracle (scripts/check-harness-markers.sh, wired into qemu-smoke CI and rsi-cycle.sh) boots both kernels and requires the sorted ~1,571-line ANVAYA marker set to diff-empty against the committed evidence/harness-marker-baseline.txt, masking only fields check-qemu-boot.sh itself asserts by regex (poll counters, physical-address/satp/pte/sepc layout values that shift with kernel image size, bench ticks, ledger line-counts) — and additionally asserts every spec row's expected marker appears in the transcript (spec_rows=73), so a proof that stops printing its marker is a CI failure. A third self-tightening ratchet, HARNESS_CEILING (55,254 → 506), joins CORE/MAIN in scripts/ratchet-state.env, machine-lowered by the alignment gate. All ~909 QEMU marker assertions, workspace tests, and the verification gate stay green. Builds on v1.3.0 "100× the Monolith."

Anvaya v1.3.0 ("100× the Monolith — Self-Tightening Ratchet · RSI") is released — the release where the improver improves itself. nucleus/src/main.rs shrinks from 76,824 to 539 lines (142×; the goal's target was 100×/≤768) across 12 proof-gated RSI cycles, with zero QEMU markers deleted, zero proofs weakened, and no ceiling raised. The 118 run_* boot-proof harnesses now live under nucleus/src/harness/ and the product core under nucleus/src/core/ (+ core/boot.S for the boot/trap assembly) — the compiler's module tree, not a regex heuristic, is now the core/harness boundary the manifesto alignment gate measures. The nucleus line-count ratchet is self-tightening: CORE_CEILING and MAIN_CEILING live in scripts/ratchet-state.env and are machine-lowered (never raised) by check-manifesto-alignment.sh --write — CORE_CEILING 22,112 → 21,226 and MAIN_CEILING 768 → 539 over the release — so any size regression is a CI failure with no human edits. The boot marker ANVAYA MANIFESTO LEDGER OK now reports main_lines= and the QEMU proof asserts it against the actual file and the live ratchet state. Per-cycle build+proof wall-clock is logged to evidence/cycle-times.jsonl: the nucleus rebuild fell from 17.6s to 8.6s as the file shrank, evidence that iteration speedups compound. All ~900 QEMU marker assertions, the Kani/bounded verification gate, the workspace tests, and every feature-build variant stay green. The product core remains ~21.2k lines vs the ~15k manifesto target — the module seams cut here stage the 1.4–1.6 extraction debt.

Anvaya v1.2.0 ("Scheduling & IPC to Spec — SMP · Real-Time · Async") is released — the first 1.x release that is an architectural shift rather than an increment: it brings two of the four Nucleus services (Scheduling #3 and IPC #2) up to their manifesto specification and, in doing so, removes the single-hart soundness assumption the entire proof train had rested on since 0.x. Four gates, each shipping code, tests, and repeatable QEMU evidence now under qemu-system-riscv64 -smp 4. Gate A (SMP bring-up): the boot hart releases the parked secondary harts via SBI HSM hart_start into a real multi-hart scheduler with per-hart 64 KiB stacks and trap state, bounded per-hart FIFO run queues, round-robin distribution, and work stealing; shared kernel state is made SMP-safe under a documented four-rule spinlock discipline with no cross-hart &'static mut aliasing, and released harts idle in wfi woken by real SBI IPI doorbells (ANVAYA SMP SCHEDULER OK harts=4 ... executed=12 double_claims=0 distinct_executors=4 steals=12). Gate B (real-time): priority-based scheduling with priority inheritance that bounds priority inversion, utilization-based admission control, a measured bounded worst-case dispatch latency (timestamped on every live preemption, observed to fit well inside one scheduling quantum), and a periodic real-time task driven one model tick per real supervisor timer interrupt that meets every deadline (ANVAYA RT SCHEDULE OK wcet_ticks=... deadline_met=1 misses=0). Gate C (asynchronous IPC): first-class async message ports — non-blocking send, poll/wait, bounded queues with Busy backpressure, capability-scoped endpoints, kernel-stamped sender identity and sequences, and correct cross-hart delivery under SMP — standing alongside the existing synchronous call/reply, delivering the manifesto's "synchronous and asynchronous message passing" (ANVAYA ASYNC IPC OK ... cross_hart_msgs=24 per_sender_fifo=1); with matching SDK client wrappers. Gate D (soundness & ratchet closure): the pure SMP/async models were extracted into a dependency-free no_std crate (anvaya-nucleus-model) re-exported by the nucleus so the proven types are the types the kernel runs, which makes them Kani-verifiable without codegen'ing the kernel binary — the Kani harness count grows from 7 to 13 (all VERIFICATION:- SUCCESSFUL: run-queue linearizability, bounded refusal, no-two-harts-run-the-same-task, pop/steal disjointness, async-port linearizability, async backpressure, plus the pre-existing cross-hart capability-safety-under-lock proof), each with an always-on bounded-exhaustive counterpart re-run every boot (ANVAYA SMP SOUNDNESS OK invariants=6 single_hart_assumption=retired); VERIFICATION.md replaces its "single-hart execution assumption" section with an honest multicore execution model (what is Kani-proven, what the documented lock discipline argues, and the trusted boundary: the spinlock implementation, the sub-Acquire/Release memory model, and the SBI/HSM firmware). Manifesto commitments M4 (scheduling priority-based with real-time guarantees; universal scale) and M11 (synchronous and asynchronous message passing) both advance to DELIVERED (the boot ledger now reads delivered=13 partial=3 debt=4 hw_exempt=1). The nucleus core ratchet held without a ceiling amendment: the release opened with a front-loaded extraction (the AEC on-disk persistence formats to anvaya-aec, the virtio-net TX packet builders to anvaya-virtio) that dropped the core from 22,111 to 21,301, and the subsequent SMP/RT/async core work brought it back to 22,086 — still under the pre-existing 22,112 ceiling, so net core is flat-or-down. Verified under QEMU: all four proof scripts run under -smp 4, workspace tests green, 13 Kani harnesses SUCCESSFUL, SDK compile-fail proofs, the alignment gate and nucleus ratchet, clippy -D warnings clean on every kernel feature combo, service-crate coverage unchanged and intact (the crates that were literal 100% remain 100%, and the new model crate is 100%), the crypto ACVP baseline untouched, and a 0.45% unsafe-Rust TCB. No physical-hardware or external-audit claim is added.

Anvaya v1.1.1 is released — a review-and-polish patch on v1.1.0 "North Star Realignment", the outcome of a meticulous review of the release against its goal doc and the manifesto. No functional kernel change (boot markers identical except the alignment-ledger counts). It corrects stale retired-marker references (the energy broker's marker became ANVAYA ENERGY SERVICE OK when it was extracted to a userspace WASM service in v1.1.0, but three docs still cited the old ANVAYA ENERGY BROKER OK), makes the SDK's type-state capability wrapper move-only so a capability cannot be duplicated and attenuation genuinely consumes the wider capability (faithful to the manifesto's unforgeable-tokens principle), and honestly reclassifies manifesto commitment M2 (PQC as the default for all cryptographic operations) from delivered to partial — the operational trust anchor, audit-chain seal, and identity attestation are hybrid/PQC, but the per-app 512-byte package envelope signature is still Ed25519 because it cannot hold ML-DSA-65's ~3.3 KB signature, so full-envelope hybrid awaits the larger WASI package format in 1.4 (the boot marker now reads delivered=11 partial=4). The change leans toward under-claiming over over-claiming, per the manifesto's interpretability discipline. Verified under QEMU: all four proof scripts, workspace tests, SDK compile-fail proofs, the alignment gate and nucleus line-count ratchet, clippy -D warnings clean on every kernel feature combo, and 100% pqc-lib coverage with the crypto ACVP baseline untouched. No physical-hardware or external-audit claim is added.

Anvaya v1.1.0 ("North Star Realignment") is released — the first release of the 1.x line, turning the system back toward the manifesto after a line-by-line audit (MANIFESTO_ALIGNMENT.md, 13 deviations classified). Four gates: (A) a machine-checked manifesto alignment ledger of 21 commitments with per-row evidence, a CI gate that verifies every delivered row's evidence resolves, and a nucleus line-count ratchet (main.rs must stay under the 75,951-line baseline, now 75,945) — emitting ANVAYA MANIFESTO LEDGER OK; (B) post-quantum cryptography as the operational default — the package trust anchor is now hybrid Ed25519 + ML-DSA-65 with classical-only downgrade and forged halves refused, the audit chain tip is ML-DSA-65-sealed, and HQC + FN-DSA are tracked as real code (ANVAYA PQC OPERATIONAL OK); (C) the first nucleus extraction — the energy broker's decision logic moved out of the kernel into a sandboxed import-free WASM service invoked over capability-scoped IPC, proven identical to the reference crate by differential tests (ANVAYA NUCLEUS EXTRACTION OK, with an extraction playbook); (D) type-state capability traits in the SDK where operations are gated by type and delegation can only narrow, with trybuild compile-fail proofs showing that widening a capability or invoking without authority are type errors (ANVAYA CAPABILITY TRAITS OK). Manifesto errata E1 (the ~15KB/~15k-lines contradiction) and E2 (prototype vs 2030 Production 1.0 versioning) are logged. Verified under QEMU: all four proof scripts, workspace tests, SDK compile-fail proofs, Kani 6/6, TCB 0.45%, ACVP 1827/0, 100% service-crate coverage, and clippy -D warnings clean on every kernel feature combo. No physical-hardware or external-audit claim is added.

Anvaya v1.0.2 is released: service-crate test coverage reaches a literal 100.0000% of regions, lines, and functions (8103/8103, 4173/4173, 374/374), with the last gaps closed by behavior-preserving refactors validated bit-exact against all 1,827 pinned NIST ACVP vectors; kernel `clippy -D warnings` is now clean on the riscv64 target across every feature combination (the workspace lint gate had never covered the no_std kernel); a per-gate execution ledger confirms all 643 proof-script markers individually emitted in fresh live QEMU transcripts (only the 8 physical-hardware gates remain exempt); V1_1_GOAL.md defines the 1.x 'North Star Realignment' arc from a 13-deviation manifesto audit (alignment ledger, PQC as operational default, first nucleus extraction with a 75,951-line ratchet, type-state capability traits); and the manifesto receives its first logged errata (E1: ~15KB corrected to ~15k lines; E2: prototype versioning runs ahead of the 2030 'Production 1.0' bar). No physical-hardware or external-audit claim is added.

Anvaya v1.0.1 is released as a patch on the QEMU-Proven Milestone: post-1.0 adversarial-audit fixes land as new commits (honest markers and claims, a 1 MiB boot stack with a low-water canary guard, mesh domain-separation tags with a non-vacuous delegation proof, ML-KEM input-validation guards), a `verification` CI workflow runs the bounded-exhaustive proofs, all six Kani harnesses, and the full pinned 1,827-vector NIST ACVP sweep on every push, service-crate test coverage is driven to ~100% of reachable code, and an opt-in `interactive-shell` cargo feature adds a real capability-scoped serial REPL (used by the anvaya.dev/demo live boot) plus the ASCII boot banner. No physical-hardware or external-audit claim is added.

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.