Architecture

Technical Specification v0.1

Implementation note: this document describes the target-state architecture. The current repository only implements a first-light boot scaffold and should not be read as feature parity with every interface sketched below. Normative status for target claims is tracked in the RFC traceability matrix in AnvayaOS/rfcs; RFC 0007 is now the accepted software CSpace/handle representation and RFC 0010 is the accepted syscall ABI contract. The current nucleus has a proof-backed syscall facade for the implemented capability, IPC, and memory subset plus bounded scheduler, init/service- manager, process-manifest ABI/handoff, and bounded wait-token semantic proofs plus one scheduler/launch-table-bound manifest init entry/return proof and one scheduler-bound IPC/capability/memory syscall-loop proof. The repository also now has an initial no-std RFC 0010 SDK ABI crate, while the full reusable U-mode ecall dispatcher, userspace process loader, production scheduler, production init/service manager, final app/WASM SDK, and CHERI hardware-specific encoding remain future work.

Table of Contents

1. Overview
2. Design Principles
3. System Layers
4. Nucleus (Microkernel)
5. Capability System
6. Agent Execution Contexts
7. System Services
8. Storage Model
9. Application Runtime
10. Security Architecture
11. Hardware Requirements
12. Scaling Model

Overview

AnvayaOS is a capability-based, target-state AI-native operating system designed for RISC-V hardware. This document specifies the technical architecture that implements the vision described in the MANIFESTO, with current status labels called out where a target-state claim is not implementation parity.

Architectural Goals

Design Principles

1. Capability-First

Every resource access requires an explicit, unforgeable capability token. There is no ambient authority, no root user, no magic paths.

Traditional: process → syscall → kernel checks permissions → access
ANVAYA:     process → present capability → kernel validates → access

2. Microkernel Foundation

The Nucleus provides only four services:

1. Capability management
2. Inter-process communication (IPC)
3. Scheduling
4. Memory management

Everything else runs in userspace, isolated by capabilities.

3. AI as Citizen

Status: Accepted AEC semantic model with bounded evidence-backed 0.5 runtime implementation.

AI agents are not modeled merely as applications running on the OS; in the accepted RFC 0002 design they are accountable AECs with:

• Identity (cryptographic attestation)
• Goals (declared intentions)
• Capabilities (explicit permissions)
• Accountability (audit trails)

4. Formal Verification

Target-state: the Nucleus is formally verified using Verus/Creusot to mathematically prove:

• Capability semantics are correctly enforced
• Memory safety is guaranteed
• IPC cannot violate isolation

5. RISC-V Native

ANVAYA exploits RISC-V features unavailable on legacy architectures:

• CHERI extensions for capability hardware
• Custom extensions for AI acceleration
• Open ISA for hardware-software co-design

System Layers

┌─────────────────────────────────────────────────────────────────────────┐
│ LAYER 5: APPLICATIONS                                                    │
│ • WASM modules (sandboxed, portable)                                    │
│ • Native applications (Rust, capability-safe)                           │
│ • AI Agents (AECs)                                                      │
├─────────────────────────────────────────────────────────────────────────┤
│ LAYER 4: SYSTEM SERVICES                                                 │
│ • Intelligence Broker (AI orchestration)                                │
│ • Energy Broker (sustainability)                                        │
│ • Intent Router (multi-modal UI)                                        │
│ • Filesystem, Network, Device Manager                                   │
├─────────────────────────────────────────────────────────────────────────┤
│ LAYER 3: APPLICATION RUNTIME                                             │
│ • WASM Runtime (Wasmtime)                                               │
│ • ANVAYA WASI Extensions                                                │
│ • Capability Traits Library                                             │
├─────────────────────────────────────────────────────────────────────────┤
│ LAYER 2: PRIVILEGED EXTENSIONS (Optional, Verified)                      │
│ • Network Fast Path                                                     │
│ • Storage Fast Path                                                     │
│ • Tensor Fast Path                                                      │
│ • Graphics Fast Path                                                    │
├─────────────────────────────────────────────────────────────────────────┤
│ LAYER 1: NUCLEUS (Formally Verified, ~15k lines)                         │
│ • Capability Management                                                 │
│ • Inter-Process Communication                                           │
│ • Scheduler (Real-time aware)                                           │
│ • Memory Manager                                                        │
├─────────────────────────────────────────────────────────────────────────┤
│ LAYER 0: HARDWARE                                                        │
│ • RISC-V CPU (RV64GC minimum)                                           │
│ • CHERI Extensions (capability hardware)                                │
│ • Optional: NPU, Crypto Accelerator, HSM                                │
└─────────────────────────────────────────────────────────────────────────┘

Nucleus (Microkernel)

Overview

The nucleus is the only AnvayaOS component intended to run in supervisor mode. Platform firmware remains below it in machine mode; the experimental QEMU protected profile makes that boundary explicit with a small resident monitor described in PROTECTED_MONITOR.md. The nucleus is:

• Small: ~15,000 lines of Rust
• Verified: Formal proofs of correctness
• Minimal: Only four core services

Accepted Nucleus ABI Boundary

RFC 0010 freezes the first userspace/Nucleus syscall contract. The accepted boundary is a RISC-V ecall ABI with:

• a7 syscall number
• a0-a6 call arguments as listed in each syscall row
• unused argument registers must be zero, and unknown nonzero flag bits return ANVAYA_E_UNSUPPORTED
• a0 primary return value
• a1 stable AnvayaError
• a2 auxiliary return value

The accepted call families are version/startup, capability and CSpace ops, IPC send/receive/call/reply/cancel, memory frame/map/unmap/share/fault calls, task/trap and interrupt calls, wait/cancel calls, and proof/debug calls. Each RFC 0010 row defines inputs, outputs, required rights, failure modes, audit events, and current implementation status.

Current executable status: the nucleus now has a kernel-resident syscall dispatch facade for abi.version, cap.identify, cap.delegate, cap.revoke, ipc.send, ipc.receive, ipc.call, ipc.reply, bounded ipc.cancel, wait_one, cancel_token, mem.frame_alloc, mem.map, and mem.unmap. The QEMU evidence exercises the RFC 0010 register envelope, format 0x1 software handles, invalid syscall failure, malformed-handle failure, local IPC send/receive/call/reply/cancel, handle-backed IPC transfer slots, bounded CSpace IPC import/export, attenuation, revocation, capability-table lookup, staged frame-cap allocation, map/unmap, rights denial, alias revocation, revoked-endpoint IPC denial, IPC audit hooks, fault recording, and bounded scheduler semantics for ready/running/blocked states, duplicate admission denial, priority dispatch, timer-tick preemption, block/unblock, idle/no-self-switch behavior, priority-preserving budget expiry, single-runner dispatch, wait-token timeout/cancel/complete unblocking, and starvation aging. It also exercises bounded init/service-manager semantics for capability-gated declaration, duplicate and missing-capability denial, start, invalid-start denial for already-running and failed services, failure reporting, restart, stop, running-service registry lookup, table-full denial, stopped-slot reclaim, and restart-limit checks. The same proof harness now includes a bounded byte-backed process-manifest ABI and handoff for init and service process records, magic/version/reserved-field validation, capability grant/requirement validation, missing-capability and duplicate-init denial, scheduler admission, init-first priority dispatch, and service registry publication from a service manifest. The provisional parser accepts only major version 0 with minor versions up to 1, rejects future minor versions and any nonzero reserved fields, and recognizes the application role byte for the later app-loader path while this proof image exercises only init/service handoff. The QEMU proof now also feeds the init manifest entry/asid/cspace/capability grant through a scheduler/launch-table-bound entry dispatcher into one mapped satp stack-touching ABI-version U-mode ecall, maps the declared init stack, materializes text plus stack leaves, and marks the launch record syscall-returned. The proof also now routes one scheduler/launch-table-bound manifest process through a reusable syscall return/resume path for cap.identify, ipc.send, ipc.receive, ipc.reply, ipc.call, ipc.cancel, mem.frame_alloc, mem.map, mem.unmap, and cap.revoke, revalidating the running scheduler task, stored Sv39 satp identity, process user-copy window, translated send-request, receive, reply-request, call-request, call-reply, and cancel windows, endpoint queue delivery, transferred timer capability, returned endpoint capability fields, returned device-frame capability fields, cumulative send+receive+reply+call IPC audit success, scheduler-bound bad-length call failure/audit validation, scheduler-bound cancel clearing, empty cancel idempotence, cumulative IPC audit validation through seven events, scheduler-bound delegated child revoked-endpoint failure with preserved queued request state, no reply mutation, cumulative IPC audit validation evidence: eight events with two failure records, transient frame authority, mapping authority, page-walk installation/removal, stale mapping-handle denial, frame revocation, and launch-table return state. A reusable process-bound memory syscall runner now re-enters one loaded U-mode process for mem.frame_alloc, mem.map, mem.unmap, and cap.revoke, validating transient frame/mapping authority and stale mapping-handle failure under active process satp; a bounded process-bound wait-token proof now covers wait_one timeout, cancel_token cancellation, and completed timer-token observation; the bounded scheduler proof now covers fixed wait-token slots that time out, cancel, or complete before unblocking the waiting task; the installed storage-roundtrip service proof now also records a bounded service reply timeout with wait_token=0x814, wait_state=timed-out, tick=12, expired=1, switches=2, and pending_waits=0; the installed network-echo service proof records the matching bounded network reply timeout with wait_token=0x815, wait_state=timed-out, tick=12, expired=1, switches=2, and pending_waits=0; production arbitrary manifest-stack allocation remains planned. Production service-grade wait-token integration beyond proof-harness service waits, a production audit service, a real scheduler/loader-bound U-mode syscall dispatcher across the full syscall surface, production scheduler integration, and production init/service-manager integration remain planned alongside CHERI hardware-specific encoding in RFC 0017 and RFC 0014/RFC 0015.

Nucleus Services

1. Capability Management

/// Core capability operations
trait CapabilityManager {
    /// Create a new capability (only Nucleus can do this)
    fn create(resource: ResourceId, permissions: Permissions) -> Capability;
    
    /// Validate a capability (called on every resource access)
    fn validate(cap: &Capability, operation: Operation) -> Result<(), Error>;
    
    /// Delegate a capability (create attenuated copy)
    fn delegate(cap: &Capability, restrictions: Restrictions) -> Result<Capability, Error>;
    
    /// Revoke a capability and all its derivatives
    fn revoke(cap: &Capability) -> Result<(), Error>;
}

Accepted representation: RFC 0007 stores capabilities in Nucleus-owned per-task CSpaces. A userspace handle is an opaque RFC 0010 u64 token using the accepted format 0x1 software encoding behind the ABI: slot index, generation, lineage tag, and format version. The slot record, not the integer, is the authority and carries object kind, object id, rights, owner task, full lineage id, parent metadata, and audit label.

Current executable status: the nucleus proves a bounded internal cap-table model and a v0.2 task-owned CSpace memory slice that match the accepted RFC 0007 semantics: capabilities name kernel-managed objects, delegation may only preserve or narrow rights, metadata must match the capability it describes, stale or forged handles fail closed, and revocation invalidates a parent-slot family without over-revoking unrelated lineage. The current proof also requires receiver-side CSpace manage authority, imports a receiver-local receive-only endpoint derivative from one CSpace into another, records source CSpace/slot parent metadata, rejects foreign receiver handles, denies attenuated reply use, rejects send-right amplification without mutating the receiver CSpace, and proves source-side cap.revoke propagation invalidates the imported derivative. The proof's exact six-slot and eight-slot capacities remain fixtures, but the software representation contract is now accepted. CHERI can harden the same model later; it is not required for correctness today.

2. Inter-Process Communication (IPC)

ANVAYA uses synchronous rendezvous IPC inspired by seL4:

/// IPC endpoint operations
trait IpcEndpoint {
    /// Send a message (blocks until received)
    fn send(endpoint: EndpointCap, message: &Message) -> Result<(), Error>;
    
    /// Receive a message (blocks until available)
    fn recv(endpoint: EndpointCap) -> Result<Message, Error>;
    
    /// Combined send-receive (call)
    fn call(endpoint: EndpointCap, request: &Message) -> Result<Message, Error>;
}

/// Message structure
struct Message {
    /// Small data payload (fits in registers)
    data: [u64; 4],
    /// Capabilities to transfer
    caps: [Option<Capability>; 4],
}

For async communication, userspace services provide channels built atop synchronous IPC.

3. Scheduler

The scheduler provides hierarchical, real-time-aware scheduling:

Priority Tiers:
├── TIER 0: Hard Real-Time (deadline < 100µs)
│   └── Sensor fusion, safety-critical, UI input
├── TIER 1: Soft Real-Time (deadline < 100ms)  
│   └── AI inference, audio, video rendering
├── TIER 2: Interactive (deadline < 500ms)
│   └── User applications, foreground tasks
└── TIER 3: Best-Effort (no deadline)
    └── Background tasks, batch processing

Each tier uses a different scheduling algorithm:

• Tier 0: Earliest Deadline First (EDF)
• Tier 1: Rate Monotonic Scheduling (RMS)
• Tier 2: Weighted Fair Queuing
• Tier 3: Round Robin

Energy-aware scheduling integrates with the Energy Broker to honor joule budgets.

Current executable status: the nucleus includes a bounded scheduler proof with fixed task slots, ready/running/blocked state transitions, priority-based dispatch, duplicate admission denial, timer-tick preemption, block/unblock behavior, idle/no-self-switch behavior, priority-preserving budget expiry, single-runner dispatch, bounded wait-token timeout/cancel/complete queues that unblock the waiting task, and starvation-aging selection. It is evidence for the scheduling semantics plus one manifest-backed process entry/return through the running scheduler task; it is not yet the production scheduler connected to general process dispatch.

4. Memory Manager

Memory management provides:

• Virtual address spaces per process
• Capability-tagged memory regions (CHERI)
• Page table management
• Physical memory allocation

Current executable status: the v0.2 nucleus isolation slice implements a staged kernel-internal memory model. It allocates frames from DTB-backed RAM, installs Frame and AddressSpace capabilities in task-owned CSpaces, maps and unmaps Sv39-shaped leaf PTE records, denies missing or insufficient authority, denies requested mapping rights outside frame authority, revokes matching frame-cap aliases across proof CSpaces, invalidates every staged mapping for a frame on frame-family revocation, and records a revoked-page fault. Owned page-table pages, hardware satp switching, production allocator policy, and copy rules are still future work. RFC 0010 accepts the syscall shape for memory calls, and the current syscall facade routes the proof-backed mem.frame_alloc, mem.map, mem.unmap, and process-bound transient-frame revocation calls into this staged substrate.

/// Memory operations
trait MemoryManager {
    /// Map a memory region with capability protection
    fn map(
        addr_space: AddressSpaceCap,
        phys: PhysicalRegionCap,
        virt: VirtualAddress,
        permissions: MemPermissions,
    ) -> Result<MemoryCap, Error>;
    
    /// Unmap a memory region
    fn unmap(cap: MemoryCap) -> Result<(), Error>;
    
    /// Create a shared memory region
    fn share(cap: &MemoryCap, target: ProcessCap) -> Result<MemoryCap, Error>;
}

Nucleus Verification

The Nucleus is specified to be verified using Verus and Creusot. For 1.0, accepted proof artifacts must establish:

1. Capability Integrity: Capabilities cannot be forged or escalated
2. Memory Safety: No buffer overflows, use-after-free, or data races
3. IPC Correctness: Messages are delivered exactly once, in order
4. Scheduler Correctness: Real-time deadlines are met when resources allow

Formal verification artifacts are a 1.0 acceptance gate. Current early releases use executable QEMU transcript evidence until RFC 0016 proof gates are satisfied.

Capability System

Implementation note: the concrete structures in this section are illustrative target-state sketches. The current milestone freezes local authority semantics, a bounded internal proof table, a v0.2 staged memory-isolation slice with task-owned CSpaces and Sv39-shaped PTE rows, the RFC 0007 software CSpace/handle representation, and the RFC 0010 syscall ABI envelope plus proof facade, but not hardware page-table switching, process-loader ABI, or CHERI hardware-specific encoding details.

Current Executable Slice

The current nucleus proof uses a bounded local object/task interaction to keep semantics ahead of representation:

• task 0xa001 owns a local object capability with read plus inspect authority
• task 0xa002 receives only inspect authority through delegation
• the derivative preserves object identity and lineage but records the new holder task
• attempted amplification to add write authority is rejected
• metadata mismatch, stale, wrong-lineage, wrong-slot, exhausted-slot, revoked-parent, revoked-derivative, and revoked-grandchild cases are explicit QEMU smoke assertions
• parent revocation walks parent-slot ancestry and invalidates derivative slots without invalidating an unrelated local-object lineage
• revoked slots can be reclaimed only with a generation bump, making old handles stale
• frame capabilities can be created from DTB-backed RAM and mapped only through an address-space capability with sufficient rights, and requested page rights must be contained in the resolved frame capability rights
• producer and auditor task contexts have separate proof CSpaces and staged address-space tables
• a bounded CSpace IPC import/export proof requires receiver-side CSpace manage authority, imports a receiver-local receive-only endpoint derivative into the auditor CSpace with source CSpace/slot parent metadata, and rejects foreign handles, attenuated reply use, and send-right amplification before proving source-side cap.revoke of the imported derivative
• missing frame authority, overbroad mapping rights, stale mappings, and revoked frame families fail closed in the QEMU transcript
• invalid or zero page permissions fail closed before capability lookup

Stable for this milestone:

• no ambient authority
• object identity plus rights define usable authority
• delegation cannot amplify
• handle resolution fails closed
• revocation applies to a parent and its derivative lineage
• unrelated object lineages remain valid when another family is revoked
• revoked slots are reusable only through generation-changing reclamation
• CSpace imports require receiver authority, preserve lineage, narrow rights, remain non-amplifying, and are revoked when the proven source slot is revoked
• memory mapping requires both frame authority and address-space authority
• frame-family revocation invalidates matching frame-cap aliases and existing staged mappings across the proof address spaces before reuse

Accepted by RFC 0007:

• per-task CSpace ownership
• format 0x1 software u64 handle encoding behind RFC 0010 opaque handles
• slot generation, lineage, parent metadata, and fail-closed stale-handle rules
• IPC import/export as receiver-local derivative slots
• software fallback on non-CHERI RV64GC targets

Still planned or hardware-specific:

• production CSpace capacity profile
• local object representation
• hardware page-table layout and satp switching
• userspace process-loader ABI beyond RFC 0010 startup handoff
• CHERI-backed sealed-handle or storage encoding

DTB Inventory Scope

DTB parsing remains deliberately bounded and allocation-free. Before the FML13V01 path touches UART MMIO, the nucleus validates the header and exact board profile, chosen console and alias, enabled harts and RV64 ISA floor, timebase, UART register contract, PLIC/CLINT references, RAM ranges, firmware handoff, FDT reservations, and static reserved-memory ranges. Unsupported, missing, colliding, or truncated inputs fail closed. For a physical candidate, the parser also accepts an all-or-nothing set of three strict lowercase /chosen identities: a per-attempt boot ID, the final Image SHA-256, and the canonical preserved-firmware SHA-256. Partial, malformed, uppercase, or zero identities fail closed. This is the accepted Buildable contract; it is not general FDT coverage or physical-board proof.

Platform Profile Scope

The v0.5.4 implementation uses a small no-std compile-time resource profile boundary. Since v1.8.2 exactly one of three features must be selected: qemu-virt, dc-roma-fml13v01 or shakti-cclass; nucleus/build.rs turns the choice into the anvaya_board cfg and a hardware_target cfg shared by the two physical boards, and zero or several features fail to compile. interactive-shell depends on qemu-virt. The SHAKTI C-class profile (shakti-cclass-arty100t) uses a SHAKTI uart_v2 console backend that polls STATUS at a width chosen at boot and never writes BAUD, CONTROL, DELAY or IEN; SBI TIME with the DTB's timebase between 1 kHz and 1 GHz; hart 0 fixed; and vendor-tree DTB admission, four stated rules (absent stdout-path, console without interrupt-parent, unparsable unneeded reg, low timebase) that each print when used and apply to no other profile. Its escape is not a declaration: the kernel probes the escape extension at run time and runs the app stage only when the firmware advertises it, which Anvaya's SHAKTI resident monitor does only after PMP fences the monitor and the CLINT. Boot hygiene is shared by all profiles: boot.S zeroes .bss and clears sscratch on the elected hart, and the physical boards also keep the DTB blob out of the frame allocator. QEMU retains its byte-stride UART, 10 MHz Sstc timer, and virtio-MMIO probe table. The FML13V01 profile exposes no QEMU virtio ranges and accepts its JH7110 32-bit, register-shift-2 UART, exact starfive,jh7110-syscrg baudclk=146/apb_pclk=145 topology, and 4 MHz SBI TIME resources only after firmware-provided DTB validation. Its RISC-V Image v0.2 header, boot-hart parking, load/entry bounds, and deterministic bundle make it Buildable. The physical-session builder hashes the completed Image, derives a firmware identity from the vendor manifest's preserved SPL/OpenSBI/U-Boot partitions, injects those values plus a random boot ID into a copy of the captured runtime DTB, and only then hashes the boot DTB. The untouched runtime DTB and modified boot DTB remain separate evidence, avoiding an impossible self-referential Image hash and preventing either DTB identity from being silently substituted. The FML runtime now has a bounded per-byte UART-ready poll, a single SBI TIME deadline/interrupt proof, SBI SRST readiness, boot-hart-only First light, and a real Ed25519-verified zero-grant hello-status interpreter run. These paths are compiled and acceptance-tested but remain physically unverified. scripts/prepare-fml13v01-media.py can prepare only a hash-pinned regular-file clone, and its tests prove that all changed sectors stay inside the allowlisted normal FAT partition while vendor firmware partitions remain byte-identical. The deterministic hardware-log verifier freezes the future physical marker/identity contract using explicitly synthetic fixtures. Neither test is physical evidence. A separate release preflight binds the final version, 12-item goal checklist, support-matrix claim, hardware inventory, distinct runtime and boot DTBs, actual Image and artifact bill of materials, canonical firmware identity, prepared-media bundle identity, physical UART result, validation/recovery markers, and allowlisted evidence hashes from a clean checkout. The canonical validation runner binds the exact clean evidence revision and physical UART-log SHA-256, records one ordered marker for each required lane, and proves the checkout is still clean before its final marker. Its behavior is exercised with fixtures, but the real preflight cannot pass at Buildable level. The physical runbook defines the evidence capture and release ceremony. V0_5_5_GOAL.md still requires runtime board evidence before physical FIRST LIGHT or APP OK claims.

Capability Structure

/// A capability is an unforgeable token granting access to a resource
#[repr(C)]
struct Capability {
    /// Unique identifier for the resource
    resource_id: u64,
    
    /// Permissions bitmap
    permissions: u64,
    
    /// Restrictions (attenuation)
    restrictions: Restrictions,
    
    /// Cryptographic tag (hardware-protected on CHERI)
    tag: CapabilityTag,
}

/// Example permission flags
bitflags! {
    struct Permissions: u64 {
        const READ     = 0b0001;
        const WRITE    = 0b0010;
        const EXECUTE  = 0b0100;
        const DELEGATE = 0b1000;
        // ... domain-specific permissions
    }
}

Capability Types

Capability Traits (Compile-Time Safety)

/// Capability trait for compile-time checking
pub trait Capability: Send + Sync {
    type Resource;
    type Operations;
    
    fn resource_id(&self) -> ResourceId;
    fn has_permission(&self, op: Self::Operations) -> bool;
}

/// Example: File read capability
pub struct ReadCap<T> {
    inner: RawCapability,
    _marker: PhantomData<T>,
}

impl<T> ReadCap<T> {
    /// Read operation - only available with ReadCap
    pub async fn read(&self) -> Result<T, Error> {
        // Kernel validates capability
        syscall::read(self.inner)
    }
    
    /// Delegate with further restrictions
    pub fn delegate(&self, restrictions: Restrictions) -> Result<ReadCap<T>, Error> {
        let new_cap = syscall::delegate(self.inner, restrictions)?;
        Ok(ReadCap { inner: new_cap, _marker: PhantomData })
    }
}

// WriteCap cannot call read(), ReadCap cannot call write()
// Enforced at compile time!

Current executable status: sdk/anvaya-sdk is the first checked-in no-std SDK surface. It exposes the RFC 0010 ABI version, syscall numbers, error codes, rights bits, opaque handles, timeout/result wrappers, and a mockable client for capability, IPC, memory, and wait/cancel calls. It includes a RISC-V ecall backend behind target cfg, but it is still an ABI crate rather than the final WASM/app SDK described by RFC 0021/RFC 0022.

Constitutional Capabilities

Some capabilities have special status:

/// Constitutional capability tiers
enum ConstitutionalTier {
    /// Cannot be modified without physical access
    Immutable,
    /// Requires formal amendment process to modify
    Constitutional,
    /// Normal policy-level capability
    Statutory,
}

/// Immutable capabilities (examples)
const IMMUTABLE_CAPS: &[&str] = &[
    "human_override",      // Always invocable
    "audit_log_read",      // Cannot be disabled
    "constitution_read",   // Always readable
];

/// Constitutional capabilities (require amendment to change)
const CONSTITUTIONAL_CAPS: &[&str] = &[
    "physical_actuator_control",  // Requires approval workflow
    "biometric_data_access",      // Requires explicit consent
    "cross_device_delegation",    // Requires cryptographic proof
];

Agent Execution Contexts

Status: Accepted RFC 0002 model plus evidence-backed bounded Gates B–C runtime. runtime/anvaya-aec implements trust-root-verified Ed25519 identity, declared goals and trusted goal policy, rooted supervision, explicit attenuation-only live capabilities, all accepted quota classes, lower process/task bindings and cleanup, authenticated lifecycle control, and per-AEC contextual hash-chained audit. AECs remain above ordinary processes/tasks and add no new Nucleus syscall family; QEMU proves an AEC-owned process through the existing CSpace, scheduler, SATP, IPC, and RFC 0010 substrate. Gate C adds the bounded side-effect-free world model, trusted-clock exact approval/effect boundary, quota reservation, a fully authenticated two-slot COW action journal, reserved reconciliation evidence, flush-ordered two-slot journal/audit persistence with authenticated selector metadata and QEMU corruption fallback probes, exact journal-to-archive checkpoint binding, restart-safe recovery, and reconciliation; Gate D supplies A2A separately.

Accepted AEC Boundary

RFC 0002 freezes these semantics:

• identity: aec_id, model identity, creator identity, runtime identity, signing root, creation time, and audit stream
• declared goals: human-readable intent, machine-readable intent, constraints, success criteria, non-goals, scope, expiry, priority, and amendment authority
• lifecycle states: created, runnable, planning, awaiting_approval, executing, suspended, cancelling, revoked, completed, failed, and terminated
• supervision: every supervisor chain must terminate in a human authority or an accepted constitutional policy authority; supervisor loops are invalid
• approval flow: approvals bind to an exact proposal hash, goal version, capability set, and expiry window
• quotas: compute, memory, model inference, storage, IPC, deadline, energy, and human-attention budgets are explicit AEC policy inputs
• world model: planning and simulation are allowed; external side effects are forbidden until capability, approval, quota, revocation, and audit checks pass
• failure/cancellation: failures, denials, revocations, quota exhaustion, and cancellations are explicit lifecycle/audit events

The process loader, immutable audit service, Intelligence Broker/AEC-creation bridge, AEC lifecycle, world-model/approval boundary, and capability-bound A2A core now have executable evidence across all four 0.5 gates. Production daemon deployment, durable world-model storage, approval UI, and the full 0.6 constitutional policy engine remain later work.

AEC Structure

Agent Execution Contexts (AECs) are ANVAYA's accepted spec primitive for AI agents:

/// Agent Execution Context
pub struct AgentExecutionContext {
    /// Unique AEC identity and cryptographic attribution
    identity: AgentIdentity,
    
    /// Declared goal (for scheduling, auditing, interpretation)
    goal: Goal,
    
    /// Capability set (what the agent can access)
    capabilities: CapabilitySet,
    
    /// World model (sandboxed reasoning space)
    world_model: WorldModel,
    
    /// Audit log (complete decision history)
    audit_log: AuditLog,
    
    /// Resource quotas
    quotas: ResourceQuotas,
    
    /// Supervisor (parent agent or human)
    supervisor: SupervisorRef,

    /// Current accepted RFC 0002 lifecycle state
    lifecycle_state: AecLifecycleState,

    /// Lower processes/tasks executing on behalf of this AEC
    process_set: ProcessSetRef,
}

/// Agent identity with cryptographic attestation
pub struct AgentIdentity {
    /// Unique identifier
    id: AgentId,
    /// Model hash (which AI model)
    model_hash: Hash,
    /// Creation timestamp
    created: Timestamp,
    /// Creator identity
    creator: CreatorId,
    /// Cryptographic signature
    signature: Signature,
}

/// Declared goal
pub struct Goal {
    /// Natural language description
    description: String,
    /// Structured intent (for machine processing)
    intent: Intent,
    /// Success criteria
    success_criteria: Vec<Criterion>,
    /// Constraints
    constraints: Vec<Constraint>,
    /// Explicit non-goals
    non_goals: Vec<NonGoal>,
    /// Who may amend this goal
    amendment_authority: AmendmentAuthority,
}

Cognitive Sandboxing

Status: Accepted boundary with an evidence-backed bounded Gate C implementation. Agents reason in isolated world models before affecting reality; durable general-purpose world-model storage and approval UI remain later work:

/// World model - sandboxed reasoning space
pub struct WorldModel {
    /// Agent's beliefs about the world
    beliefs: BeliefStore,
    
    /// Hypothetical actions (not yet executed)
    pending_actions: Vec<HypotheticalAction>,
    
    /// Simulated outcomes
    simulations: Vec<Simulation>,
}

impl AgentExecutionContext {
    /// Plan an action (in world model, no real effect)
    pub fn plan(&mut self, action: Action) -> PlanResult {
        // Reasoning happens in sandbox
        let hypothetical = self.world_model.simulate(action);
        self.audit_log.record_planning(action, hypothetical);
        hypothetical
    }
    
    /// Execute an action (requires approval, affects reality)
    pub async fn execute(&mut self, action: Action) -> Result<Outcome, Error> {
        // Check that action matches current declared goal and constraints.
        self.goal.validate_action(&action)?;

        // Check capability
        let cap = self.capabilities.get_for_action(&action)?;
        
        // Request approval (may involve human-in-the-loop)
        let approval = self.request_approval(&action).await?;

        // Re-check authority after approval to close revocation races.
        self.capabilities.resolve_current(&cap)?;
        
        // Record in audit log
        self.audit_log.record_execution(&action, &approval);
        
        // Actually execute
        let outcome = action.execute(cap).await?;
        
        // Update world model with actual outcome
        self.world_model.update_from_reality(&outcome);
        
        Ok(outcome)
    }
    
    /// Request approval from supervisor
    async fn request_approval(&self, action: &Action) -> Result<Approval, Error> {
        match self.supervisor {
            SupervisorRef::Human(human) => {
                // Human-in-the-loop approval
                human.request_approval(action).await
            }
            SupervisorRef::Agent(agent) => {
                // Supervisor agent approval
                agent.approve(action).await
            }
            SupervisorRef::Constitutional(rules) => {
                // Automatic approval based on constitutional rules
                rules.evaluate(action)
            }
        }
    }
}

Agent Lifecycle

Status: Accepted state model with bounded runtime and QEMU evidence in runtime/anvaya-aec; Gate C also proves the exact approval, effect, and reconciliation path with pre-effect quota and audit ordering.

┌──────────────┐
│   Created    │ ← AEC identity, goal, supervisor, quota, audit stream assigned
└──────┬───────┘
       │
       ▼
┌──────────────┐
│   Runnable   │ ← Eligible for runtime resources
└──────┬───────┘
       │
       ▼
┌──────────────┐                      ┌──────────────┐
│   Planning   │ ── approval needed ─▶│ Awaiting     │
│              │                      │ Approval     │
└──────┬───────┘                      └──────┬───────┘
       │ approval/policy allow              │ approval granted
       ▼                                      ▼
┌──────────────┐
│  Executing   │ ← Process/task uses caps, IPC, and RFC 0010 syscalls
└──────┬───────┘
       │
       ├──▶ Suspended / Cancelling / Revoked / Failed
       ▼
┌──────────────┐
│  Completed   │ ── cleanup ──▶ Terminated
└──────────────┘

Capability-Bound A2A Coordination

Status: Evidence-backed bounded Gate D core in services/anvaya-a2a.

• Agent Card-like descriptors are discoverable only through an exact peer Endpoint capability; the service exposes no ambient registry enumeration.
• Each registration, card, and message is bound to an authenticated caller process and a runtime-trust-root-verified SVID-style envelope over the AEC's signed Ed25519 model/config/goal/runtime identity. Registration additionally proves a live owner-held Endpoint capability with the exact advertised resource and lineage, and conflicting endpoint claims fail closed.
• Message capability transfer and sub-agent task delegation require explicit DELEGATE authority and derive an equal-or-narrower child capability set.
• Delegation receipts bind parent/child identity, task/subgoal, capability-set fingerprint, reserved and attenuated quotas, priority, expiry, and child attestation; the child grant is derived by the kernel into a separate CSpace.
• Per-caller message/delegation sequence high-water marks reject replay, and receive order is monotonic even when bounded queue slots are reused.
• Competing goal claims are signed by their SVID identities and arbitrated deterministically inside caller-held peer capability scope; forged claims or registered-identity mismatches fail before delivery.
• Registration, discovery, messaging, delegation, arbitration, and denials append to the production SHA-256 hash-chained audit core.

QEMU backs the peer and delegated-object records with real CSpace handles and requires ANVAYA MULTI AGENT OK only after caller binding, kernel and service non-escalation, message/transfer, quota-reserved task delegation, arbitration, identity denial, and exact audit-trace checks. Cross-node transport is a later mesh concern.

System Services

Current executable status: the repository has a bounded kernel-side init/service-manager semantics proof for capability-gated service declarations, start/stop/restart transitions, invalid-start denial for already-running and failed services, failure reporting, registry lookup, table-full denial, stopped-slot reclaim, and restart-limit checks. It is not yet a production userspace init process, live service supervisor, or service discovery implementation.

Current network substrate status: services/anvaya-net is the first checked-in network service core. It is no-std and validates DNS names, keeps a fixed-size DNS cache, encodes/decodes bounded DNS A query/response packets, wraps and parses those DNS packets in bounded UDP/IPv4 packets with IPv4 and UDP checksum validation, wraps them in bounded Ethernet frames with MAC and ethertype validation, checks TCP endpoints against scoped connect authority, models socket handles, and enforces read/write/manage/invoke rights for DNS and socket operations. It also exposes a bounded SDK IpcMessage request/response header and service-core dispatcher for DNS insert/resolve and TCP socket connect/endpoint/send calls over caller-provided buffers plus receive from service-owned pending data into caller output buffers, with version, shape, rights, handle, and optional resource/lineage validation. The nucleus QEMU proof exercises DNS insert/resolve, denied DNS, DNS A packet write/parse, DNS-over-UDP/IPv4 packet write/parse, DNS-over-UDP/IPv4 Ethernet frame write/parse, TCP connect/send/receive, and denied-port paths before printing ANVAYA NETWORK SERVICE CORE OK, while the virtio harness now proves one DNS-over-UDP/IPv4 Ethernet TX frame before ANVAYA VIRTIO NET DNS TX OK and one live virtio-net RX ARP reply before ANVAYA VIRTIO NET RX OK. It remains network-service groundwork: live TCP/IP state machines, timers, retransmission, routing, and userspace service integration are still v0.3 work.

Intelligence Broker

Status: Evidence-backed bounded v1 service core for model registry/load, inference, and audited AEC creation. The no-std services/anvaya-intelligence crate stores exact versioned artifacts, derives content-bound model capability resources, revalidates model and administrative grants on every privileged operation, enforces caller-bound session/inference quotas, invokes bounded model and MCP endpoint runtimes, maps MCP tools/call arguments to exact endpoint capabilities, appends an ordered MCP record binding the exact request, capability, and result before any later model execution, and appends every accepted/denied operation to the production contextual hash-chained audit log. QEMU proves the service behind live registered scheduler/SATP dispatch with ANVAYA INTELLIGENCE BROKER OK; the Gate B proof creates its primary AEC through the Broker bridge. Agent coordination lives in the bounded services/anvaya-a2a Gate D core.

The target interface continues beyond the implemented Gate A subset:

/// Intelligence Broker API
pub trait IntelligenceBroker {
    /// Register a model
    fn register_model(&self, model: ModelSpec) -> Result<ModelId, Error>;
    
    /// Load model for inference
    fn load_model(&self, id: ModelId, target: LoadTarget) -> Result<ModelCap, Error>;
    
    /// Run inference
    fn infer(&self, cap: ModelCap, input: Tensor) -> Result<Tensor, Error>;
    
    /// Create an agent
    fn create_agent(&self, spec: AgentSpec) -> Result<AgentExecutionContext, Error>;
    
    /// Coordinate multiple agents
    fn coordinate(&self, agents: &[AgentId], task: Task) -> Result<CoordinationPlan, Error>;
}

/// Load target for models
enum LoadTarget {
    /// Load on local device
    Local,
    /// Load on edge node
    Edge { max_latency: Duration },
    /// Load in cloud
    Cloud { provider: CloudProvider },
    /// Let broker decide
    Auto { constraints: InferenceConstraints },
}

Energy Broker

Manages energy as a first-class resource:

/// Energy Broker API
pub trait EnergyBroker {
    /// Allocate energy budget
    fn allocate(&self, joules: u64, deadline: Timestamp) -> Result<EnergyCap, Error>;
    
    /// Query current consumption
    fn query(&self, cap: &EnergyCap) -> EnergyStatus;
    
    /// Get carbon intensity of available compute
    fn carbon_intensity(&self) -> CarbonMap;
    
    /// Schedule for minimum carbon
    fn schedule_green(&self, task: Task) -> Result<Schedule, Error>;
    
    /// Generate sustainability attestation
    fn attest(&self, computation: ComputationId) -> SustainabilityAttestation;
}

/// Energy capability
pub struct EnergyCap {
    /// Joules remaining in budget
    joules_remaining: AtomicU64,
    /// Carbon budget (grams CO2)
    carbon_budget: Option<u64>,
    /// Deadline for energy use
    deadline: Timestamp,
}

Intent Router

Manages multi-modal interaction:

/// Intent declaration
pub struct Intent {
    /// What the intent accomplishes
    action: ActionType,
    /// Parameters
    params: HashMap<String, Value>,
    /// Urgency level
    urgency: Urgency,
    /// Context requirements
    context: ContextRequirements,
}

/// Intent Router synthesizes appropriate modality
pub trait IntentRouter {
    /// Declare an intent (OS chooses modality)
    fn declare(&self, intent: Intent) -> Result<IntentHandle, Error>;
    
    /// Wait for user response
    fn await_response(&self, handle: IntentHandle) -> Result<Response, Error>;
    
    /// Register new modality handler
    fn register_modality(&self, modality: ModalityHandler) -> Result<(), Error>;
}

/// Modality-specific rendering
enum ModalityHandler {
    Cli(CliRenderer),
    Touch(TouchRenderer),
    Voice(VoiceRenderer),
    Gesture(GestureRenderer),
    Neural(NeuralRenderer),
    Api(ApiRenderer),
}

Storage Model

Content-Addressed Object Store

/// Content address (hash of content)
#[derive(Clone, Copy, Hash, Eq, PartialEq)]
pub struct ContentAddress(Hash);

impl ContentAddress {
    /// Compute address from content
    pub fn from_content(data: &[u8]) -> Self {
        ContentAddress(sha3_256(data))
    }
}

/// Object store interface
pub trait ObjectStore {
    /// Store content, returns address
    fn put(&self, data: &[u8]) -> Result<ContentAddress, Error>;
    
    /// Retrieve content by address
    fn get(&self, addr: ContentAddress) -> Result<Vec<u8>, Error>;
    
    /// Check if content exists
    fn exists(&self, addr: ContentAddress) -> bool;
    
    /// Delete content (if no references)
    fn delete(&self, addr: ContentAddress) -> Result<(), Error>;
}

Current executable status: services/anvaya-storage is the first checked-in storage service core. It is no-std, fixed-capacity, content-addressed, deduplicates by content id, checks explicit read/write/manage rights from anvaya-sdk, and covers put, get, list, namespace update, namespace lookup, a unit-tested SDK IpcMessage request/response header with exact operation/length/authority-rights/optional resource-lineage/version/response shape validation, a bounded service-core dispatcher for put/get/list/namespace and object-length requests over explicit content/name/output buffers, quota/capacity denial, output-bound denial, fail-before-mutation dispatcher coverage, and storage plus IPC error-to-RFC 0010 mapping in unit tests. The nucleus QEMU proof exercises put/get/list, namespace put/get, and missing-rights denial before printing ANVAYA STORAGE SERVICE CORE OK; it also archives the signed network-echo package through this store, writes the package bytes to live virtio-blk sector 2, reads them back, revalidates the content id, reinstalls the restored bytes, and launches the restored record before ANVAYA STORAGE BLOCK PACKAGE OK. It remains proof/service-core substrate: production cryptographic hash policy, snapshots, garbage collection, durable block-backed service persistence, and live userspace service integration are still RFC 0020/RFC 0028 and v0.3 implementation work.

Namespace Layer

/// Mutable pointer to immutable content
pub struct NamespaceEntry {
    /// Human-readable path
    path: Path,
    /// Current content address
    current: ContentAddress,
    /// Version history
    history: Vec<VersionEntry>,
    /// Access capability required
    required_cap: CapabilityType,
}

/// Namespace operations
pub trait Namespace {
    /// Resolve path to content address
    fn resolve(&self, path: &Path) -> Result<ContentAddress, Error>;
    
    /// Update path to point to new content
    fn update(&self, path: &Path, new_addr: ContentAddress) -> Result<(), Error>;
    
    /// List entries in directory
    fn list(&self, path: &Path) -> Result<Vec<NamespaceEntry>, Error>;
    
    /// Get version history
    fn history(&self, path: &Path) -> Result<Vec<VersionEntry>, Error>;
}

Distributed Sync

Content-addressed storage enables efficient distributed sync:

/// Sync protocol
pub trait DistributedSync {
    /// Announce available content
    fn announce(&self, addrs: &[ContentAddress]) -> Result<(), Error>;
    
    /// Request content from peers
    fn request(&self, addr: ContentAddress) -> Result<Vec<u8>, Error>;
    
    /// Sync namespace state (CRDT-based)
    fn sync_namespace(&self, peer: PeerId) -> Result<(), Error>;
}

Application Runtime

WASM Runtime

Applications run as WebAssembly modules:

/// WASM module configuration
pub struct WasmConfig {
    /// Module binary
    module: Vec<u8>,
    /// Granted capabilities
    capabilities: CapabilitySet,
    /// Memory limits
    memory_limit: usize,
    /// CPU time limit (per invocation)
    time_limit: Duration,
    /// Energy budget
    energy_budget: Option<u64>,
}

/// ANVAYA WASI extensions
pub trait AnvayaWasi {
    /// Standard WASI (filesystem, clock, random)
    fn wasi_standard(&self) -> WasiStandard;
    
    /// Capability operations
    fn wasi_capability(&self) -> WasiCapability;
    
    /// Intent-based UI
    fn wasi_intent(&self) -> WasiIntent;
    
    /// AI model invocation
    fn wasi_intelligence(&self) -> WasiIntelligence;
    
    /// Energy tracking
    fn wasi_energy(&self) -> WasiEnergy;
}

Current executable status: runtime/anvaya-wasm is the first checked-in WASM runtime core. It is no-std, validates the WASM magic/version plus bounded type/import/function/export/code sections, recognizes bounded WASI preview and Anvaya function import declarations, enforces fixed type/import/function/export, code-byte, stack, and fuel limits, invokes zero-argument i32 exports, executes i32.const, i32.add, i32.sub, imported-function call, and end, routes bounded imported i32 host calls through explicit host authority, and maps parser/runtime failures onto the RFC 0010 error vocabulary. It remains WASM-runtime groundwork: linear memory, capability-mediated WASI host-call layouts, live userspace service IPC, production package/runtime integration, and live loader/app launch are still v0.3 work. A bounded nucleus QEMU proof now executes all twelve proof-app packages through runtime/anvaya-runner, verifies their source recipes with ANVAYA WASM APP SOURCE CATALOG OK, and proves bounded installer-backed launches plus missing-grant launch failure, after the same boot path exercises the storage/network service cores; that is kernel-harness evidence rather than the production loader path.

Current WASI mediation status: runtime/anvaya-wasi is the first checked-in capability-mediated host-call core. It is no-std, validates bounded relative file paths, opens file descriptors only from explicit grants, authorizes file read/write, DNS, TCP connect/send/receive, clock, and Anvaya capability extension calls from explicit rights, validates guest pointer ranges for file/DNS/socket buffers, decodes guest TCP endpoint and Anvaya extension request records, writes bounded DNS results back into guest memory, and maps mediation or guest-fault failures onto the RFC 0010 error vocabulary. It remains WASI groundwork: WASI preview ABI coverage, broader linear-memory result layouts, live userspace storage/network IPC, runtime/anvaya-wasm import integration, intent/energy APIs, and production loader-launched app evidence are still v0.3 work. The current nucleus QEMU proof does exercise the bounded file/storage, DNS/TCP, clock, and Anvaya extension proof calls through explicit grants, and the runner now has focused tests that continue storage/DNS/TCP imports into the bounded storage and network service-core dispatchers after mediation.

Current example-app status: examples/anvaya-wasm-apps is the first checked-in WASM application catalog. It contains twelve tiny proof modules with declared file, DNS, TCP, stdio, clock, endpoint, and local-object capability profiles, a service profile for service-role endpoint-receive, and no-std source recipes that rebuild the checked-in WASM bytes byte-for-byte. read-config imports anvaya.file_read, write-log imports anvaya.file_write, dns-lookup imports anvaya.dns_resolve, tcp-fetch imports anvaya.tcp_connect, clock-now imports wasi_snapshot_preview1.clock_time_get, endpoint-send imports anvaya.cap_authorize, endpoint-receive imports anvaya.cap_authorize, storage-roundtrip imports anvaya.storage_roundtrip, and network-echo imports anvaya.dns_resolve plus anvaya.tcp_connect; stdio-write imports guest-memory wasi_snapshot_preview1.fd_write; and file-records imports guest-memory file result-record calls. Direct interpreter tests prove those imports deny by default. The catalog tests rebuild every source recipe to the checked-in bytes, authorize declared host-call profiles through runtime/anvaya-wasi and verify signed app manifests through runtime/anvaya-package. Bounded runner tests verify each signed package, check launch grants against the app profile, install WASI grants, and invoke the bounded WASM export through runtime/anvaya-runner; another test installs each package through runtime/anvaya-installer and runs the installed record through the same runner path. The nucleus QEMU proof also builds raw signed proof packages for all twelve catalog apps, requires ANVAYA WASM APP SOURCE CATALOG OK, and runs them through the bounded runner with explicit host grants, runs network-echo through the service-backed runner path with DNS/TCP imports dispatching through the bounded network service core, and runs storage-roundtrip through the service-backed runner path with storage put/get imports dispatching through the bounded storage service core, installs and launches network-echo from the bounded installer registry, runs that installed record through the service-backed network runner path, then denies a read-config launch with missing host and launch grants after the storage/network service-core checks pass in the same boot. It remains example-app groundwork: external toolchain-built WASI modules beyond the internal recipes, persistent installer/loader integration, broader guest WASI imports, and production loader-launched evidence in QEMU are still v0.3 work.

Native Applications

Rust applications can run natively with capability safety:

/// Native application entry point
#[anvaya::main]
async fn main(caps: InitialCapabilities) -> Result<(), Error> {
    // Capabilities are explicitly passed, not ambient
    let fs = caps.filesystem;
    let net = caps.network;
    let intel = caps.intelligence;
    
    // Use capabilities
    let data = fs.read("config.toml").await?;
    
    Ok(())
}

/// Capability requirements declared in manifest
#[anvaya::manifest]
mod manifest {
    capabilities: [
        filesystem::read("config.toml"),
        network::connect("api.example.com:443"),
        intelligence::invoke("text-embedding"),
    ]
}

Current executable status: runtime/anvaya-package is the first checked-in package/app manifest core. It is no-std, parses bounded AVPK app/service/ driver bundle headers and capability required/requested rights records, rejects reserved-field, version, malformed-rights, and rights-amplification failures, verifies the signed region through a caller-provided signature verifier, applies role/right/code-size/cap-count launch policy, and emits narrowed launch grants only when the required rights remain satisfied. It remains package/runtime groundwork: production installer behavior, trust-root and key-management policy, persistent install transactions, and live loader/app launch are still v0.3 work. The current nucleus proof consumes raw signed AVPK proof packages with a toy signature verifier and explicit launch policy, including one storage-block-backed package restore/launch check and one missing-grant denial check, after the same boot path proves the storage/network service cores.

Current installer status: runtime/anvaya-installer is the first checked-in package installer registry core. It is no-std, verifies signed packages once through runtime/anvaya-package, assigns stable content-derived package ids, can archive package bytes into services/anvaya-storage with explicit storage authority, stores installed package records in fixed slots with policy-narrowed launch grants, rejects duplicate packages before consuming slots, reclaims slots on uninstall, and maps package/storage/installer failures onto RFC 0010 errors. The current nucleus QEMU proof consumes one installed package record from this registry and now also restores a storage-archived package from live virtio-blk sector 2, reinstalls it, and launches the restored installed record. It remains installer groundwork: trust-root/key rotation, package naming/versioning, dependency and upgrade transactions, live storage service integration, durable installer transactions, and loader-launched QEMU evidence are still v0.3 work.

Current runner status: runtime/anvaya-runner is the first checked-in signed WASM package runner core. It is no-std, verifies raw signed packages or consumes installed package records from runtime/anvaya-installer, requires package launch grants for declared file, DNS, TCP, stdio, clock, and Anvaya extension host profiles, installs authorized grants into runtime/anvaya-wasi, instantiates the bounded WASM payload, invokes a zero-argument i32 export, mediates one imported wasi_snapshot_preview1.clock_time_get proof call through explicit host authority, one imported anvaya.cap_authorize proof call through installed capability-extension grants, and narrow imported anvaya.dns_resolve and anvaya.tcp_connect proof calls through installed network grants, plus anvaya.file_read, anvaya.file_write, and anvaya.storage_roundtrip proof calls through installed file and capability-extension grants, including guest-memory fd_write and file result-record imports. It also offers a service-backed proof entrypoint that routes anvaya.storage_roundtrip through the bounded storage dispatcher and anvaya.dns_resolve/anvaya.tcp_connect through the bounded network dispatcher after WASI grant mediation for both raw signed packages and already installed package records. Focused runner tests prove those service-backed seams. It maps package/WASI/WASM failures onto RFC 0010 errors. The nucleus QEMU proof now packages and runs all twelve catalog apps through the existing bounded runner path, verifies their source recipes before ANVAYA WASM APP SOURCE CATALOG OK, runs network-echo and storage-roundtrip through the service-backed runner path before ANVAYA WASM SERVICE RUNNER OK, installs and runs network-echo from the bounded registry, runs the installed network-echo record through service-backed network dispatch before ANVAYA WASM APP INSTALL SERVICE RUNNER OK, derives application manifest rights from installed storage-roundtrip and network-echo, dispatches storage-roundtrip as process 0xa804 before ANVAYA WASM APP STORAGE PACKAGE LOADER OK, dispatches network-echo as process 0xa803 before ANVAYA WASM APP PACKAGE LOADER OK, feeds installed storage-roundtrip and network-echo launch grants into three-record startup init/service/application manifests, dispatches application process 0xa806 under ASID 0xa106 and CSpace 0xc506, and requires ANVAYA STARTUP APP MANIFEST LOADER OK, then proves those startup-dispatched apps can send a service IPC request to service 0xb701 with transfer_rights=0x2, parent_cspace=0xc506, wait_token=0x806, and ANVAYA STARTUP APP SERVICE IPC SEND OK, then has the same service receive/reply, complete the app wait with wait_state=completed, wait_data=0x2, and pending_waits=0, and resume the app before ANVAYA STARTUP APP SERVICE IPC REPLY OK and ANVAYA STARTUP APP RESUME OK, then prove the resumed app performs a service-style RFC 0010 ipc.call through mapped request/reply buffers, returns a receiver-local endpoint handle with transfer_rights=0x2, reaches cumulative audit=4, and requires ANVAYA STARTUP APP SERVICE IPC FULL CALL OK, then resumes the app again and drops the returned receiver-local endpoint through RFC 0010 cap.drop with dropped=1, error=stale, syscall=0x103, and ANVAYA STARTUP APP SERVICE IPC CALL DROP OK, then attempts to reuse that dropped handle through ipc.receive and proves error=bad-handle, audit=5, failures=1, and ANVAYA STARTUP APP SERVICE IPC CALL DROP DENIAL OK, then queues a fresh service request and clears it through RFC 0010 ipc.cancel with reason=0xca17, cleared=1, cumulative audit=7, and ANVAYA STARTUP APP SERVICE IPC CANCEL OK, then proves the app exits through the scheduler/launch-table-bound task_exit path with status=9 for storage-roundtrip and status=10 for network-echo, launch_state=exited, scheduler_state=exited, current_idle=1, and ANVAYA STARTUP APP EXIT OK, installs and runs service-role endpoint-receive, derives process-manifest service rights from its launch grants, admits/declares/starts it through the manifest/init-service path before ANVAYA WASM SERVICE PACKAGE LOADER OK, and proves missing host/launch grants deny execution after direct storage/network service-core checks; the installed storage-roundtrip storage-service path also proves a reply wait timeout before ANVAYA WASM STORAGE SERVICE WAIT TIMEOUT OK, and the installed network-echo network-service path proves a reply wait timeout before ANVAYA WASM NETWORK SERVICE WAIT TIMEOUT OK. It remains runner groundwork: broader guest WASI imports from linear memory, live userspace storage/network IPC, persistent installer integration, and production loader-launched app evidence in QEMU are still v0.3 work.

Security Architecture

Threat Model

ANVAYA assumes adversaries that may include:

• Malicious applications
• Compromised AI agents
• Superintelligent AI systems
• Quantum-capable attackers
• Nation-state actors

Defense Layers

Constitutional Enforcement

/// Constitutional constraint enforcement
pub struct Constitution {
    /// Immutable rules (hardware-enforced)
    immutable: ImmutableRules,
    /// Constitutional rules (amendment-protected)  
    constitutional: ConstitutionalRules,
    /// Statutory rules (policy-level)
    statutory: StatutoryRules,
}

impl Constitution {
    /// Check if operation is permitted
    pub fn check(&self, operation: &Operation) -> ConstitutionalResult {
        // Immutable rules cannot be overridden
        if self.immutable.forbids(operation) {
            return ConstitutionalResult::Forbidden;
        }
        
        // Constitutional rules may require approval
        if let Some(requirement) = self.constitutional.requirement(operation) {
            return ConstitutionalResult::RequiresApproval(requirement);
        }
        
        // Statutory rules are policy
        self.statutory.evaluate(operation)
    }
}

Hardware Escape

The experimental v0.6.1 QEMU profile has a resident M-mode monitor. It installs PMP before entering the complete S-mode nucleus, protects the firmware policy, CLINT, and a persistent pflash audit anchor, and retains the machine timer. Its three-boot gate demonstrates that direct protected-region stores, repeated or forged protected effects, armed-escape re-arm/timer/reset override, S-mode interrupt masking, and rollback of only the S-mode disk fail closed. This is an experimental privilege-boundary proof, not physical escape wiring or measured boot; see PROTECTED_MONITOR.md for the exact non-claims.

/// Hardware escape levels
pub enum EscapeLevel {
    /// Software-triggered (authenticated)
    Soft,
    /// Hardware button (firmware-handled)
    Hard,
    /// Physical isolation (power/network cut)
    Physical,
}

/// Escape operations
pub trait HardwareEscape {
    /// Pause all agents
    fn pause_all_agents(&self) -> Result<(), Error>;
    
    /// Terminate all agents and enter safe mode
    fn safe_mode(&self) -> Result<(), Error>;
    
    /// Full system halt and memory wipe
    fn emergency_halt(&self) -> !;
    
    /// Firmware recovery mode
    fn recovery_mode(&self) -> !;
}

Hardware Requirements

Minimum (Wearable Class)

Recommended (Mobile/Desktop Class)

Full Featured (Server Class)

RISC-V Extensions

Scaling Model

Device Classes

Current executable status: drivers/anvaya-virtio is the first checked-in driver core. It is no-std and validates virtio-MMIO register snapshots for block and network device IDs, requires explicit DeviceFrame + MAP authority, checks the MMIO register window size, models and materializes bounded virtqueue descriptor/available/used state with explicit DMA frame rights, supports bounded chained descriptor submission for block requests, plans baseline feature negotiation, and fails closed on malformed, inactive, unsupported, wrong-class, bad-queue, missing-authority, missing-required-feature, short-ring, invalid-chain, or out-of-range DMA paths. The nucleus QEMU proof now enables real virtio-blk and virtio-net MMIO devices, reads their live magic/version/device/vendor registers, classifies both transports, and asserts ANVAYA VIRTIO MMIO PROBE OK after missing-map-rights and wrong-class checks; it reads the live virtio-blk feature register, writes the baseline accepted/required feature set and status, and asserts ANVAYA VIRTIO FEATURE NEGOTIATION OK; it configures the live virtio-net TX queue and DMA-submits a deterministic ARP/Ethernet frame before ANVAYA VIRTIO NET TX OK, then submits a bounded DNS-over-UDP/IPv4 Ethernet frame before ANVAYA VIRTIO NET DNS TX OK; it configures the live virtio-net RX queue with a writable DMA packet buffer, triggers QEMU's ARP reply through TX queue 1, and validates the received reply from 10.0.2.2 to 10.0.2.15 before ANVAYA VIRTIO NET RX OK; it submits a live virtio-blk sector-0 read and verifies used-ring completion, status byte, and zero-filled sector checksum before ANVAYA VIRTIO BLK READ OK; it reads sector 1 before rewriting it and validates either fresh or exact persisted proof bytes before ANVAYA VIRTIO BLK PREWRITE READ OK; it writes a deterministic sector-1 pattern and reads it back with exact-pattern validation before ANVAYA VIRTIO BLK WRITE READBACK OK; the dedicated two-boot QEMU proof reuses one raw virtio-blk image and verifies the deterministic sector-1 checksum and exact byte pattern survive a restart; it writes and reads a storage-archived signed package through sector 2 before ANVAYA STORAGE BLOCK PACKAGE OK; it programs the live virtio-blk queue select/size/align/PFN/status registers and asserts ANVAYA VIRTIO QUEUE MMIO OK; it writes a no-op live queue notify and asserts ANVAYA VIRTIO QUEUE NOTIFY MMIO OK; it materializes descriptor/available/used ring bytes and asserts ANVAYA VIRTIO QUEUE MEMORY OK; then it builds a bounded queue and asserts ANVAYA VIRTIO QUEUE CORE OK after DMA-authority checks. It remains driver groundwork: DTB-driven discovery, block persistence integrated with production storage/package services, interrupt-driven scheduling, full TCP/IP packet handling, and userspace device-manager integration are still v0.3 work.

┌────────────────────────────────────────────────────────────────────────┐
│ WEARABLE          │ MOBILE           │ DESKTOP         │ SERVER        │
├────────────────────────────────────────────────────────────────────────┤
│ µW - mW           │ 100mW - W        │ W - 100W        │ 100W - MW     │
│ KB - MB RAM       │ GB RAM           │ GB - TB RAM     │ TB+ RAM       │
│ 1-2 cores         │ 4-8 cores        │ 8-32 cores      │ 64-256+ cores │
├────────────────────────────────────────────────────────────────────────┤
│ Nucleus only      │ Nucleus +        │ Nucleus +       │ Nucleus +     │
│                   │ Core services    │ Full services   │ Full + dist.  │
│                   │                  │ + UI            │ orchestration │
├────────────────────────────────────────────────────────────────────────┤
│ Sensing,          │ Local inference, │ Full inference, │ Training,     │
│ offload           │ UI, apps         │ development     │ coordination  │
└────────────────────────────────────────────────────────────────────────┘

Device Mesh

Devices form a capability-connected mesh:

/// Device mesh operations
pub trait DeviceMesh {
    /// Discover nearby devices
    fn discover(&self) -> Vec<DeviceInfo>;
    
    /// Pair with device (exchange capabilities)
    fn pair(&self, device: DeviceId) -> Result<PairingCap, Error>;
    
    /// Delegate capability to remote device
    fn delegate_remote(
        &self,
        cap: &impl Capability,
        target: DeviceId,
        restrictions: Restrictions,
    ) -> Result<RemoteCapRef, Error>;
    
    /// Invoke capability on remote device
    fn invoke_remote<T>(
        &self,
        cap: RemoteCapRef,
        operation: Operation,
    ) -> Result<T, Error>;
}

Appendix: Reference Implementation Notes

Build System

# QEMU first-light scaffold (default platform)
cargo build --release -p anvaya-nucleus \
  --target riscv64gc-unknown-none-elf \
  --features kernel-bin,qemu-virt

# Deterministic FML13V01 regular-file Image/DTB/U-Boot bundle
./scripts/build-fml13v01-artifact.sh

# Run the QEMU target
./scripts/run-qemu.sh

Testing

# Platform feature/build matrix
./scripts/check-platform-profiles.sh

# Standalone artifact reproducibility and support-claim checks
./scripts/check-fml13v01-artifact.sh
./scripts/check-hardware-support.py

# Virtual removable-media safety and physical-log contract tests
./scripts/check-fml13v01-media.sh
python3 ./scripts/test-v0-5-5-hardware-log.py
python3 ./scripts/test-v0-5-5-release.py

# QEMU boot smoke checks
./scripts/check-qemu-boot.sh

# Resident M-mode monitor plus three-boot hostile-S proof
./scripts/check-protected-monitor.sh

This document is a living specification. See rfcs for proposed changes.