Implementation Status

Current release: 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.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.

Prior release: 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.