Implementation Status

v1.8.3 fixes the intermittent qemu-virt boot hang present since before v1.8.2: a device interrupt taken while a client or service runs in user mode is now claimed through the bare kernel map, fatal reports print through it, and a restarted driver binding drains the PLIC source its predecessor left latched. v1.8.2 added the shakti-cclass kernel target for a SHAKTI C-class bitstream (Buildable, QEMU shakti_c only), with OpenSBI and Rust machine-mode monitor lanes and a private loading kit for IIT Madras. Fresh exact-source local gates at the v1.8.3 tag cover all 135 model harnesses, pinned Verus obligations and negative controls, Lean, QEMU with both SHAKTI lanes, six-boot recovery and four crash cuts, ACVP, accounting and documentation. transport=service-loopback, polling=0 and kernel_fallbacks=0 remain; M1, M6 and M8 stay PARTIAL. v1.9 is deferred with its source and evidence preserved. QEMU-proven research software; physical board acceptance and external audit remain pending.

v1.8.2 adds the shakti-cclass kernel target for a SHAKTI C-class bitstream on a Digilent Arty A7-100T: a SHAKTI UART console, four stated device-tree admission rules for the vendor tree, the SBI TIME timer and a runtime-probed escape. On QEMU shakti_c it reaches first light under OpenSBI v1.7 and, under the Rust machine-mode resident monitor, runs the signed hello-status app and fires the PMP-gated escape; read-only probes and a private loading kit went to IIT Madras. SHAKTI is Buildable with no physical boot claimed. v1.8.2 was tagged and released on GitHub under an owner-amended proof scope and was not deployed to anvaya.dev; v1.8.3 carries it forward with the complete local proof.

v1.8.1 maintains the v1.8 research release with constant-space CPU ISA admission, thirteen compiled Lean transport theorems and self-contained pinned ACVP preparation. The selected 8 GiB cap covers both job and aggregate, with zero swap and one job. Fresh exact-source local gates cover all 135 model harnesses, pinned Verus obligations and negative controls, Lean, QEMU, six-boot recovery and four crash cuts, ACVP, accounting and documentation. Signed userspace Broker, model and checkpoint-storage services, bounded WASM and capability refinement retain the v1.8 scope. transport=service-loopback, polling=0 and kernel_fallbacks=0 remain; M1, M6 and M8 stay PARTIAL. v1.9 is deferred with its source and evidence preserved. QEMU-proven research software; physical board acceptance and external audit remain pending.

v1.8.0 completes intelligence and verification maturation with signed Broker, model and checkpoint-storage services in separate U-mode tasks. The exact registered bounded WASM model executes with fuel and capability limits; AECs bind signed goals, process identity, quota and approvals to real tool endpoints. Six-boot recovery and four crash cuts retain quota/history, reject stale authority and damaged checkpoints, and prevent replayed effects. Shared-runtime capability refinement covers the published finite transitions and full property inventories, with wrapper, serialization, cross-CSpace and SMP assumptions disclosed. All 135 model harnesses, pinned Verus obligations and negative controls, Lean, QEMU, native recovery, ACVP and documentation gates are bound to the released source and executed locally. The privileged intelligence route is retired. The runtime keeps transport=service-loopback, polling=0 and kernel_fallbacks=0. M1, M6 and M8 remain PARTIAL; verification claims stay within their published scope. This is QEMU-proven research software, with physical board acceptance and external audit still pending.

v1.7.2 closes audit findings F01–F19 across capability authority, IPC, driver and storage recovery, and native intelligence. Signed Broker, model and checkpoint-storage services run in separate U-mode tasks; the six-boot/four-crash-cut gate covers retained charges, replay refusal, restart liveness, and rollback/corruption/truncation denials. Protected freshness anchors and a durable clock floor survive recovery. The superseded privileged intelligence path is removed. Complete local Kani refinement, Verus/Lean, QEMU, native recovery, ACVP and documentation gates are pinned to the released source. The runtime keeps transport=service-loopback, polling=0 and kernel_fallbacks=0. This is QEMU-proven research software; M1, M6 and M8 remain PARTIAL, without physical-hardware or external-audit claims.

v1.7.1 "Closed-scope repairs" closes the 20 findings in the already-delivered capability, driver, storage, network and verification paths. Capability ancestry and selective revocation survive dropped handles; signed Driver rights, DMA quotas and resident-page limits are enforced; exact capability sockets retain port/DNS restrictions and generation-safe identities. ABI 0.3 provides kernel-issued reply tickets and real U-mode cancellation receipts. Durable receive queues drain, a real 160-byte namespace CRDT delta merges in U-mode, storage headers protect commit metadata, and full-sector corruption is rejected before writing. CRDT failures are atomic, virtio indices wrap safely, block errors propagate, and future-dated energy inputs are refused. The runtime keeps transport=service-loopback, polling=0 and kernel_fallbacks=0. This remains a QEMU-proven research release; M1, M6 and M8 remain PARTIAL, with no physical-hardware or external-audit claim. Product core is 21,530 lines; nucleus/src is 22,259; core plus the 1,641-line transport extension is 23,171. The model disclosure counts 3,620 non-test source lines separately. The 25,605 combined release ceiling and 15,000 core target are unchanged.

v1.7.0 "Capability Sockets" — a socket is a capability carrying kind, resource identity, rights and generation, and the TCP/UDP/IP/ARP/ICMP/DNS stack runs in a hybrid-signed U-mode task with its own pid, CSpace and SATP and no device authority. NetworkAuthority's two unauthenticated constructors are gone and from_capability is the only way to obtain network authority; the bypass that let an ambiently-built authority skip identity binding is closed. Handles carry their issuing generation, so one held across a task restart is refused as stale. The task persists its DNS cache and socket table across dispatches, serves typed requests over real kernel IPC with delegated frames, proves five denials and survives its own death with a fresh-generation replacement. Task-composed frames 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 with wire_irqs=1 and polling=0. Mesh object sync crosses those sockets. Extraction #5 leaves zero network-service names in product core: core 20,757 → 20,740, nucleus/src 21,469, privileged TCB 22,379 → 22,362. Honest scope: socket payloads do not leave the machine — they reach their reader through the service's own receive queue (transport=service-loopback) — so manifesto M8 advances DEBT → PARTIAL, not DELIVERED; TCP/UDP over the wire, DNS over the wire, ICMP echo, congestion control, IPv6 and TLS remain planned areas of accepted RFC 0032, and no physical hardware or external audit is claimed.

v1.6.0 "Content-Addressed Storage" — durable content becomes a userspace service. A hybrid-signed storage task runs as a distinct scheduled U-mode task with its own CSpace, page tables, SATP and multi-page stack and 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); the capability-checked namespace is a last-writer-wins CRDT with explicit tombstones under the strict total order (lamport, actor, tombstone, algorithm, id), proven by four new Kani harnesses (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 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: core 21,870 → 20,757, nucleus/src 22,581 → 21,476, privileged TCB 23,492 → 22,379; manifesto M6 advances DEBT → PARTIAL. Honest scope: QEMU-proven; not a production filesystem and not a power-loss durability claim; no physical hardware or external audit is claimed.

v1.5.2 "Durable Block Client" — 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. The separately Kani-verified nucleus-model state machines remain privileged code measured apart at 3,037 non-test lines.

v1.5.1 — a correctness and enforcement patch over v1.5.0 "Driver Domains" from a full post-release review: an IRQ PLIC-source wedge on stale-endpoint interrupts, a dead device-unsafe ratchet, a driver buffer_offset overflow, and a weak-memory used-ring acquire fence are fixed. 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 the counted privileged TCB (product core + extension) is 23,456. v1.5.1 also surfaces a disclosure metric: the allocation-free, Kani-verified nucleus-model state machines (device/DMA/IRQ/request tables) re-exported into the kernel are privileged code measured separately at 3,037 non-test lines, so the counted TCB is not read as the whole privileged footprint.

v1.5.0 "Driver Domains" — 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, crash/restart cleanup, and opaque-frame net reuse. This is not a physical-hardware or IOMMU-backed DMA-isolation claim.

v1.4.1 "Verify-Only Kernel" — 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: the package signing path (all three write_signed_* writers, kernel_package_pqc_sign, both signing seeds) moves to a new anvaya-package proofsign module, leaving nucleus/src verify-only — no signing code, no signing seeds, while KernelProofSignature and both pinned public keys stay; the launcher decision logic (dispatch_launch_service_request and its with_args_and_memory sibling, LaunchServiceError) moves to anvaya-runner beside run_installed_wasm_package; and 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 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.

v1.4.0 "The Real Launcher" — 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); docs/NUCLEUS_EXTRACTION.md gains its second worked example. Gate C makes the 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; manifesto M2 moves PARTIAL → DELIVERED, while M7 (WASM Application Runtime) stays PARTIAL — its launch-mechanism gap is closed, but three other WASI extension points (Intent, Intelligence Broker, Energy) remain unscheduled. 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 too-narrow check-script regex), all found and fixed, alongside a retroactive Gate B stale-marker oversight. CORE_CEILING 25,616 → 25,801, HARNESS_TOKENS 47,312 → 48,087, both amended and logged. Honest miss at release: nucleus_lines ended 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 at release and closed by v1.4.1's relocations. Harness marker oracle byte-exact throughout: 1,572 markers, diff=empty.

v1.3.6 "Honest Core/Harness Accounting" (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, hardware.rs, rt.rs, platform.rs — 5,363 lines) 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 (widened 4,096 → 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 (the 1,571-marker oracle staying diff-empty).

v1.3.5, "RSI on the Verifier" (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; all now go through a new shared scripts/lib/assert-markers.sh as declarative rows, 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, independently re-verified by 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.

v1.3.4, a one-line version-banner fix (no functional kernel change) — the boot banner and interactive-shell about command no longer claim the stale v1.0.0-only "QEMU-Proven Milestone" title next to the version number; HARNESS_TOKENS machine-lowered 43,898 → 43,896 as a side effect.

v1.3.3, a documentation-only truth-parity patch that backfilled CHANGELOG.md, STATUS.md, and the site's changelog/status/llms mirrors to close a release-doc gap that had opened across three tags.

v1.3.2 "Dissolve the Proof Bodies — Spec Rows · Shared Interpreters · Honest Floor" — 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, 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 — 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 in the process. Honest scope: the goal's 5× token target (≤30,789) was not met and was amended, by a logged MANIFESTO_ALIGNMENT.md amendment, to the measured honest floor of 43,898 — an adversarial audit (evidence/V1_3_2_TOKEN_FLOOR.md) showed the residual is byte-frozen marker text frozen by the stdout oracle, 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.

v1.3.1 "100× the Proof Harness — Spec Tables · Byte-Exact Oracle · RSI" — 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 100×/≤553) across 9 proof-gated RSI cycles with zero markers deleted or reworded and zero proofs weakened. The boot ladder is now declarative — 73 spec rows (name, expected marker, invariant) in harness/spec.rs executed in boot order by one table-driven driver, with main.rs falling 539 → 470 — and a new byte-exact oracle in CI boots both kernels and requires the sorted ~1,571-marker ANVAYA transcript set to diff-empty against a committed baseline, additionally asserting every spec row's marker appears in the transcript. A third self-tightening ceiling, HARNESS_CEILING (55,254 → 506), joins CORE/MAIN in the machine-lowered ratchet state.

v1.3.0 "100× the Monolith — Self-Tightening Ratchet · RSI" — the release where the improver improves itself: nucleus/src/main.rs shrinks from 76,824 to 539 lines (142×; the target was 100×/≤768) across 12 proof-gated RSI cycles with zero 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), so the compiler's module tree — not a regex heuristic — is the core/harness boundary the alignment gate measures. The line-count ratchet is self-tightening: CORE_CEILING and MAIN_CEILING are machine-lowered (never raised) by the gate itself (CORE 22,112 → 21,226; MAIN 768 → 539), making any size regression a CI failure with no human edits; the boot ledger marker reports main_lines= asserted against the actual file, and per-cycle build+proof wall-clock logged to evidence/cycle-times.jsonl shows the nucleus rebuild falling 17.6s → 8.6s as the file shrank.

v1.2.0 "Scheduling & IPC to Spec" — the first 1.x release that is an architectural shift rather than an increment, bringing two Nucleus services to their manifesto specification: SMP multi-hart bring-up (parked secondaries released over SBI HSM into a real multi-hart scheduler with per-hart run queues, round-robin distribution, and work stealing), real-time scheduling (priority inheritance, admission control, and a measured bounded worst-case dispatch latency), and first-class asynchronous IPC (non-blocking bounded ports with backpressure) alongside synchronous call/reply. It retires the single-hart soundness assumption held since 0.x — the Kani harness count grows from 7 to 13 and all four proof scripts now run under qemu-system-riscv64 -smp 4 — so manifesto commitments M4 (real-time scheduling) and M11 (async message passing) both advance to DELIVERED (the boot ledger reads delivered=13 partial=3).

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