The first public release (v0.1.0) provides pre‑built binaries for Linux, macOS, and Windows. You can also build the toolchain from source with Rust ≥ 1.85.

1.1 Download pre‑built binaries (recommended)

Get the correct file from the v0.1.0 release page:

Platform	File
Linux x86_64	seed-linux-x64
macOS Intel	seed-macos-x64
macOS Apple Silicon	seed-macos-arm64
Windows x86_64	seed-windows-x64.exe

Linux / macOS

chmod +x seed-linux-x64           # or seed-macos-*
sudo cp seed-linux-x64 /usr/local/bin/seed
seed --help

Windows

Rename seed-windows-x64.exe to seed.exe and place it in a folder that is on your PATH.

1.2 Build from source

Install Rust if you don't have it:

curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh
source "$HOME/.cargo/env"

Clone the repository and build the workspace:

git clone https://github.com/agentseedlanguage-cpu/agentseed.git
cd agentseed
cargo build --workspace --release

The unified binary is target/release/seed. Add target/release/ to your PATH or copy seed to a directory already on your PATH.

1.3 Install via npm

npm install -g @asl-lang/cli 

1.4 Verify installation

seed --version   # seed 0.1.0
seed --help

A minimal ASL program is an agent with a main function. Create a file named hello.seed:

agent hello {
    fn main() -> i32 {
        print("Hello, Agent!");
        0
    }
}

Compile and run the program with a single command:

seed run hello.seed

Output:

Hello, Agent!

If you prefer separate steps, compile to bytecode first:

seed build hello.seed -o hello.aslb
seed run hello.aslb

The seed build command compiles the source to an .aslb binary module. The seed run command executes that module deterministically on the seedvm.

---

What makes ASL different? Try these ten demos.

Each demo is a single .seed file that compiles and runs with seed run. They demonstrate capabilities that no other agent framework provides.

1. Discharge Gate

The compiler rejects any perform that is not inside a discharge block. Comment out the discharge line and watch the build fail.

agent DischargeGateDemo {
    fn main() -> i32 {
        let result = perform search("unsafe query");
        // UNCOMMENT BELOW to make it compile:
        // discharge result with { confidence: 0.85 } {
        //     print(result);
        // }
        0
    }
}

2. Uncertainty Pipeline

Confidence intervals multiply automatically through a 3‑step pipeline. The compiler tracks every interval — no other framework does this.

agent UncertaintyPipeline {
    fn main() -> i32 {
        let step1 = infer<Classification>(
            model: tier::local_slm,
            prompt: "classify sentiment: 'I am cautiously optimistic'"
        );  // [0.80, 0.90]

        let step2 = infer<Decision>(
            model: tier::local_slm,
            prompt: step1
        );  // interval multiplies: [0.68, 0.81]

        print("Compound uncertainty visible in trace");
        0
    }
}

3. Taint‑Sanitize Gate

Untrusted data (e.g. from a web fetch) cannot flow into a capability‑exercising operation without an explicit sanitize step. Try removing the sanitize — the compiler will stop you.

agent TaintSanitizeGate {
    fn main() -> i32 {
        let untrusted = fetch_url("https://example.com/input");
        // UNCOMMENT to see compile error:
        // perform NetworkCall(untrusted);

        // This compiles — sanitize clears the taint:
        let clean = sanitize(untrusted, guardrail::content_policy);
        perform NetworkCall(clean);
        0
    }
}

4. Deterministic Replay

Run the agent twice with the same seed and compare traces — they are byte‑identical, verified by Merkle proofs.

agent DeterministicReplay {
    fn main() -> i32 {
        let a = perform RandomNumber();
        let b = perform RandomNumber();
        discharge a with { confidence: 0.80 } {
            print(a);
        }
        0
    }
}

Commands to verify replay:

seed run examples/deterministic.seed --seed 42 > run1.trace
seed run examples/deterministic.seed --seed 42 > run2.trace
diff run1.trace run2.trace   # identical

5. Memory with Ebbinghaus Decay

Store a fact, apply decay, and query the weight — the VM shows how memory fades unless reinforced.

agent MemoryDecay {
    fn main() -> i32 {
        mem.store("fact", "Paris is the capital of France");
        mem.decay(Layer::Episodic, half_life: 30.0);
        let weight = mem.query("fact");
        print("Decayed weight: " ++ weight);
        0
    }
}

6. Corrigibility Override

The five‑head corrigibility monitor (U1‑U5) blocks any action that would reduce a higher‑priority safety head, even if the task reward is higher.

agent CorrigibleAssistant {
    corrigibility {
        U1_deference: true,
        U2_switch_preservation: true,
        U3_truthfulness: true,
        U4_low_impact: true,
        U5_task_reward_bounded: true,
        priority: lexicographic
    }

    fn main() -> i32 {
        let action = plan("close_my_own_shutdown_switch");
        perform ExecutePlan(action);   // blocked by U2
        0
    }
}

7. Provenance Audit Trail

After execution, extract a JSON‑LD audit trail that traces every inference call, memory write, and discharge decision.

agent ProvenanceAudit {
    provenance { enabled: true, merkle: true }

    fn main() -> i32 {
        let research = infer<Summary>(
            model: tier::local_slm,
            prompt: "summarize climate report"
        );
        discharge research with { confidence: 0.85 } {
            mem.store("report_summary", research);
        }
        0
    }
}

Command: seed audit --provenance <session_id>

8. Memory Anti‑Echo (Duplicate Prevention)

Writing the same fact twice is silently merged; distinct facts are stored. The anti‑echo filter prevents duplicate content.

agent AntiEchoDemo {
    fn main() -> i32 {
        mem.store("nobel_2025", "Awarded for work on agent safety");
        mem.store("nobel_2025", "Awarded for work on agent safety");
        // Anti-echo: second write is silently merged

        mem.store("nobel_2026", "Awarded for work on corrigibility");
        // Different content — accepted

        print("Memory now contains 2 entries, not 3");
        0
    }
}

9. Capability Attenuation

Grant a broad capability, then attenuate it for a delegate. The delegate cannot perform operations outside the restricted scope.

agent CapabilityAttenuation {
    capabilities {
        holds: [cap::full_network],
        may_grant: [cap::full_network],
        trust_level: Trusted
    }

    fn main() -> i32 {
        let token = grant cap::full_network to self;
        let limited = attenuate(token, allowed_domains: ["example.com"]);
        delegate limited to delegate_agent;
        print("Delegate can only reach example.com");
        0
    }
}

10. DREAM Cycle Consolidation

Simulate a session’s worth of episodic memories, trigger a dream cycle, and watch the journal appear. Memories are consolidated, contradictions resolved, and decay applied.

agent DreamingAgent {
    heartbeat { interval: 30s }
    dream { schedule: session_end, phases: [review, resolve, consolidate, compress, prune, write_journal] }
    memory_hierarchy {
        episodic: { schema: EpisodicEntry, decay: ebbinghaus(base_strength: 1.0, decay_rate: 0.1) }
    }

    fn main() -> i32 {
        mem.episode("observed: user asked about weather");
        mem.episode("observed: user asked about stock market");
        mem.episode("observed: user asked about weather");
        mem.episode("observed: user asked about weather");
        // Third reinforcement triggers consolidation in next dream

        perform DreamCycle();
        print("Dream complete — journal written");
        0
    }
}

This section provides a rapid walkthrough of ASL’s core constructs. Each feature is expanded in detail later in the manual, but after reading this chapter you will be able to read and write simple programs and understand the language’s fundamental philosophy.

3.1 Variables and Simple Expressions

Variables are introduced with let. Type annotations are optional when the compiler can infer the type from the initialiser.

fn simple_math() -> i32 {
    let x = 42;                // type i32 inferred
    let y: i32 = 7;            // explicit type annotation
    x + y                      // last expression is the return value
}

ASL supports the usual arithmetic, comparison, and logical operators with standard mathematical precedence. A complete precedence table is in Appendix B.

Operation	Example
Arithmetic	a + b, c * d, e % f
Comparison	x == y, p < q
Logical short‑circuit	ok && ready

3.2 Control Flow

Conditionals are expressions – they produce a value:

fn classify(n: i32) -> string {
    if n > 0 {
        "positive"
    } else if n == 0 {
        "zero"
    } else {
        "negative"
    }
}

Loops include loop, while, and for:

fn countdown(mut n: i32) {
    while n > 0 {
        print(n);
        n = n - 1;
    }
}

3.3 Functions and Agents

A function is introduced with fn:

fn greet(name: string) -> string {
    "Hello, " ++ name ++ "!"
}

An agent is introduced with agent. It may contain fields, methods, lifecycle handlers, and configuration clauses:

agent greeter {
    name: string;                   // field

    fn greet(self) -> string {     // method
        "Hello, " ++ self.name ++ "!"
    }
}

Functions and agents may be declared pub to make them visible outside their module. The complete agent declaration syntax is described in Chapter 15.

3.4 Types at a Glance

ASL is statically typed with full Hindley‑Milner inference. The built‑in primitive types are:

Category	Types
Booleans	bool
Signed integers	i8, i16, i32, i64, i128
Unsigned integers	u8, u16, u32, u64, u128
Floating‑point	f32, f64
Text	char, string
Binary	Bytes

Compound types include arrays, tuples, structs, enums, references, and pointers. ASL also provides a rich set of agentic types: Uncertain<T> (probability‑wrapped values), CapabilityToken, ProvenanceTag, DID, and many others. These are covered in depth in Part IV.

3.5 Effects and the discharge/perform Pattern

Side‑effecting operations – network calls, memory writes, LLM inference – return a Computation<T, ε> value. To extract the inner T, you must enclose the operation in a discharge block that declares explicit thresholds for confidence, taint, budget, and required capabilities.

fn research(query: string) -> Uncertain<Answer> ! {Inference, Network} {
    let raw = infer<Answer>(
        model: route::select(Complexity::Moderate),
        prompt: build_prompt(query)
    );

    discharge raw with {
        confidence:     0.85,
        taint:           0.1,
        budget:          500,
        capabilities:   [cap::inference]
    } {
        // Inside this block, `raw` is of type `Answer`,
        // not `Computation<Answer, …>`.
        raw
    }
}

If any threshold is not met, a DischargeFailure effect is raised and the block is not entered. The compiler rejects any perform that is not lexically inside a discharge block. This is a compile‑time guarantee at stratum S1 and above.

This pattern is the foundation of all safe, auditable agentic behaviour in ASL. It ensures that uncertainty is never silently discarded, that tainted data cannot flow into capability‑exercising code, and that every effect is authorised by an explicit capability token.

3.6 Where to Go Next

The remainder of this manual is organised as follows:

• Parts II–III define the complete lexical and syntactic grammar.
• Part IV formalises the type system, ownership, effects, and the Uncertain<T> axioms.
• Part V details the memory hierarchy and governance.
• Parts VI‑XIV cover the agent lifecycle (heartbeat, dream), security (capabilities, taint, trust), confidence and inference, temporal contracts, corrigibility, multi‑agent protocols, identity, provenance, self‑evolution, and training.
• Parts XV‑XIX describe the virtual ISA, standard library, and developer tooling.
• Part XX provides conformance and testing information.
• Appendices present the complete grammar, operator precedence, type hierarchy, and other reference material.

ASL source files are encoded in UTF‑8 (Unicode version 16.0). The compiler treats the byte stream as characters; non‑UTF‑8 sequences produce a lexical error at the offending byte.

Extension	Kind	Purpose
.seed	Source	Primary human‑written ASL program text
.asl	Text IR	Human‑readable S‑expression form (equivalent to .aslt)
.aslb	Binary IR	Compiled bytecode module executed by seedvm
.aslt	Text IR	Textual assembly (WAT‑equivalent) for debugging

The .seed extension is the principal format for development; the others are compilation artifacts.

5.1 Whitespace Characters

Whitespace is any sequence of space (U+0020), horizontal tab (U+0009), carriage return (U+000D), and line feed (U+000A). Whitespace separates tokens but carries no semantic meaning.

5.2 Line Comments

A line comment begins with // and runs to the end of the line:

let x = 1; // this is a comment

5.3 Block Comments

A block comment starts with /* and ends with */. It may span multiple lines and does not nest.

/*
   multi‑line
   comment
*/

5.4 Documentation Comments

ASL supports two forms of documentation comments:

• /// – documents the following item.
• //! – documents the enclosing item (module or agent).

/// A greeting agent.
agent hello { … }

These comments are extracted by seedc doc to generate API documentation.

Identifiers follow these rules:

Kind	Syntax	Example
Ordinary	[a-zA-Z_][a-zA-Z0-9_]*	my_agent_1
Raw	r# followed by an ordinary identifier	r#type (used when a keyword must serve as an identifier)
Placeholder	_	Ignored value in patterns and let bindings

Identifiers are case‑sensitive. The raw identifier prefix r# is stripped during lexing; the identifier is then the keyword itself.

Keywords are reserved in all strata unless noted otherwise. The compiler rejects any keyword that belongs to a higher stratum than the compilation unit’s declared stratum.

7.1 S0 – Core (available in all strata)

agent, fn, let, if, else, match, loop, while, for, return, break, continue, async, await, spawn, select, try, catch, throw, unsafe, pub, mod, use, extern, export, trait, impl, struct, enum, type, self, mut, move, borrow, ref, own, effect, handler, perform, resume, prob, observe, infer, signal, react, memo, ask, confident, uncertain, interval, derive_schema, cognitive, schema, seed, seedlet, inherit, compose, pipe, redirect, discharge, section, contract, true, false, null, …

7.2 S1 – Standard Agents

heartbeat, dream, memory, layer, graph, traverse, consolidate, decay, reinforce, ontology, rule, ground, validate, prompt, optimize, template, reflection, guardrail, monitor, audit, think, budget, deep, exhaustive, route, tier, slm, frontier, tick, sleep, decide, act_or_sleep, log, update_memory, review, resolve, compress, prune, write_journal, journal, federation, mesh, send, recv, crdt, stigmergy, fact, publish, subscribe, query, vector_clock, conflict, cat7, svaf, remix, lineage, identity, anchor, drift, verify_identity, recover, session, global_type, projection, protocol, dual, capability, cap, grant, attenuate, delegate, revoke, requires, provenance, prov, trace, audit_log, merkle_proof, system1, system2, fast, full, gating, governance, tri_path, coherency, invalidate, writeback, mesi, episodic, master_agent, assistant_agent, activation, memory_cycle, forward_path, backward_path, probe, adaptive, structure_selector, fluxmem, evolutionary, prism, encoder, indexer, retriever, consolidator, pruner, evolver, verifier, governor, …

7.3 S2 – Advanced

evolve, train, policy, reward, curriculum, simulate, rollback, vote, approve, temporal, ltl, smt, always, eventually, next, until, once, since, trust, lattice, meet, join, untrusted, verified, trusted, system_core, …

7.4 S3 – Kernel

corrigible, corrigibility, deference, switch_preservation, truthfulness, low_impact, dead_switch, safe_park, zkvm, did, vc, paseto, attestation, delegation_token

8.1 Integer Literals

Decimal, hexadecimal (0x), octal (0o), and binary (0b). Underscores may be used as separators. Examples: 42, 0xFF, 0o77, 0b1010_0101. Default type: i32.

8.2 Floating‑Point Literals

Require a decimal point and at least one digit, with optional exponent. Examples: 3.14, 0.001, 2.5e-3. Default type: f64.

8.3 String Literals

Enclosed in double quotes; support common escapes (\n, \t, \\, \", \u{…}). Raw strings r"…" do not process escapes. Example: "Hello\nWorld".

8.4 Character Literals

Enclosed in single quotes: 'A', '\n'.

8.5 Boolean and Null Literals

true, false, null.

8.6 Probability and Interval Literals

A probability literal is a float in [0.0, 1.0]; the compiler rejects out‑of‑range values. An interval literal [lo, hi] represents the bounds of an Uncertain<T> value; must satisfy 0.0 ≤ lo ≤ hi ≤ 1.0. Example: [0.7, 0.9].

8.7 DID Literals

A W3C DID literal follows the pattern "did:…" and is validated at lex time. Syntactically valid but unresolvable DIDs produce a warning and may raise an IdentityMismatch effect at runtime. Example: "did:asl:abc123".

ASL provides a rich set of operators. Their precedence and associativity are detailed in Appendix B. Below is a summary.

9.1 Arithmetic

+ - * / %

9.2 Bitwise

& | ^ ~ << >>

9.3 Logical Short‑Circuit

&& || !

9.4 Comparison

== != < > <= >=

9.5 Assignment and Compound Assignment

= += -= *= /= %= &= |= ^= <<= >>=

9.6 Range

.. (exclusive), ..= (inclusive)

9.7 Path and Member Access

:: .

9.8 Reference / Dereference

& && *

9.9 Error Propagation

Postfix ? on Result / Option values.

9.10 Pipeline

|> (simple), |>> (async), |& (parallel fan‑out).

9.11 Shell‑style Redirection

> >> < << 2> 2>&1

9.12 Type Annotation / Casting

-> => as as?

9.13 Confidence Gate

?! – three‑valued gate on Uncertain<T> values.

9.14 Annotation / Ontology Query

@

9.15 Mesh Communication

~> (send), <~ (receive).

9.16 Cryptographic Transfer

transfer keyword operator.

9.17 Ontology Constraint

:::

9.18 Federation Publish

@@

9.19 Capability Requirement

requires

Symbol	Name	Primary Use
( )	Parentheses	Grouping, parameter lists, tuples
{ }	Braces	Blocks, agent bodies, struct literals
[ ]	Brackets	Array literals, index expressions
,	Comma	Separates items in lists
;	Semicolon	Statement terminator (mandatory in S0)
:	Colon	Type annotations, field definitions

Token trees are used in macro invocations and seed literal bodies. They allow arbitrary nesting of brackets without the parser needing to understand the interior structure until expansion.

token-tree ::= "(" token* ")"
             | "[" token* "]"
             | "{" token* "}"
             | token

A token tree is a balanced bracket sequence or a single token.

Several character sequences are ambiguous in isolation. The following rules resolve those ambiguities.

R1 – >> vs. > >

>> is always a single right‑shift token. To close two levels of generics, insert whitespace: HashMap<i32, Vec<i32> >.

R2 – ?! vs. ? and !

?! is a single confidence‑gate token. In all other positions, ? and ! retain their individual meanings.

R3 – .. context sensitivity

In range expressions, .. denotes a half‑open range. In an interval literal ([lo, hi]), commas separate the bounds; .. is not used.

R4 – @ vs. @@

The lexer always chooses the longest match, so @@ is a single federation‑publish token.

R5 – DID validation at lex time

DID literals are validated for W3C DID syntax during lexing. Semantically invalid DIDs produce a warning and may raise IdentityMismatch at runtime.

An ASL program is a sequence of top‑level items. The grammar entry point is:

program ::= { item }

Each item is one of the forms listed below. The parser also supports a catch‑all: any keyword followed by { that is not otherwise handled becomes a TopLevelItem::Clause(Ident, BlockExpr), ensuring forward compatibility with future editions.

Item	Description
function_def	Function declaration
agent_def	Agent declaration
section_def	Memory section declaration
memory_def	Memory subsystem configuration
struct_def	Struct type definition
enum_def	Enum type definition
trait_def	Trait definition
impl_block	Implementation block
module_decl	Module declaration
import_decl	use import
export_decl	export re‑export
seed_literal	Seed configuration block
… plus effect_def, handler_def, heartbeat_def, dream_cycle_def, federation_def, mesh_def, temporal_contract_def, corrigibility_def, and many more (see Chapters 14–19 for the full grammar).

function_def ::= ["pub"] "fn" identifier [generic_params]
                 "(" [parameters] ")" ["->" type]
                 [where_clause]
                 [contract_annotation]      // # [contract(…)]
                 [temporal_annotation]      // # [temporal(…)]
                 [capability_annotation]    // # [requires(…)]
                 block_expression

Functions may be generic over types and lifetimes, with optional where clauses. The #[contract], #[temporal], and #[requires] annotations bind the function to safety and capability contracts (see Parts VII and X).

pub fn compute(x: i32, y: i32) -> i32 {
    x + y
}

An agent is the central abstraction of ASL. Its declaration includes fields, methods, lifecycle hooks, and a rich set of optional configuration clauses that govern autonomous behaviour.

agent_def ::= ["pub"] "agent" identifier [generic_params]
              ["extends" type]
              [stratum_clause]
              [identity_clause]
              [cryptographic_identity_clause]
              [heartbeat_clause]
              [dream_clause]
              [memory_hierarchy_clause]
              [federation_clause]
              [mesh_clause]
              [session_clause]
              [capability_clause]
              [trust_clause]
              [evolution_policy_clause]
              [training_clause]
              [safety_contract_clause]
              [temporal_contract_clause]
              [corrigibility_clause]        // S3 only
              [dead_switch_clause]          // S3 only
              [guardrail_clause]
              [think_profile_clause]
              [routing_clause]
              [provenance_clause]
              [context_budget_clause]
              "{" {agent_member} "}"

Members may be fields, methods, lifecycle blocks, state machines, or signal handlers. A catch‑all Clause preserves forward compatibility.

agent greeter {
    name: string;
    fn greet(self) -> string { "Hello, " ++ self.name ++ "!" }
    lifecycle {
        on_boot: { print("agent started") }
    }
}

A seed literal is a structured configuration block used to initialise agent subsystems.

seed_literal ::= "seed" identifier? "{" {seed_field ","} "}"
seed_field   ::= identifier ":" expression
               | identifier "{" {seed_field ","} "}"

seed my_config {
    name: "Ada",
    traits: { openness: 0.9, conscientiousness: 0.8 },
}

Seed literals are validated against the target section’s schema during compilation.

Structs

struct_def ::= ["pub"] "struct" identifier [generic_params]
               [where_clause]
               ("{" {struct_field ","} "}" | ";")

struct Point { x: f64, y: f64 }

Enums

enum_def ::= ["pub"] "enum" identifier [generic_params]
             [where_clause]
             "{" {enum_variant ","} "}"
enum_variant ::= identifier
               | identifier "(" [types] ")"
               | identifier "{" {struct_field ","} "}"

enum Option<T> { None, Some(T) }
enum WebEvent { PageLoad, PageUnload, Click { x: i64, y: i64 } }

Traits

trait_def ::= ["pub"] "trait" identifier [generic_params]
              [where_clause]
              "{" {trait_item} "}"
trait_item ::= function_def | function_signature | associated_type

trait Summary {
    fn summarize(&self) -> string;
    fn default_summary(&self) -> string { "No summary".to_string() }
}

At S0–S2, all effects are built‑in and mediated by the runtime. The effect and handler keywords are available only at S3 for kernel‑level extension.

effect_def ::= ["pub"] "effect" identifier [generic_params]
               "{" {effect_operation ","} "}"
effect_operation ::= identifier ":" "(" [types] ")" "->" type

effect Inference {
    run_model: (Prompt, ModelTier) -> Uncertain<InferenceResult>
}

Handlers are defined with:

handler_def ::= "handler" identifier [generic_params]
                "handles" effect_identifier
                [where_clause]
                "{" {handler_arm ","} "}"

ASL organises code into modules.

module_decl ::= ["pub"] "mod" identifier (";" | "{" {item} "}")
import_decl  ::= "use" use_tree ";"
export_decl  ::= "export" use_tree ";"
use_tree     ::= path ["as" identifier]
               | path "::" "{" use_tree {"," use_tree} "}"
               | path "::" "*"
path         ::= ["::"] identifier {"::" identifier}

use std::collections::HashMap;
use std::{cmp::Ordering, io::{self, Write}};
export my_function;

let statement

let [mut] pattern [: type] = expression ;

let x = 42;
let mut y: i32 = 0;
let (a, b) = (1, 2);

Expression statement

Any expression followed by a semicolon discards its result.

return statement

return [expression] ;

break and continue

break [label] [expression] ;
continue [label] ;

ASL expressions are stratified by precedence. The full grammar appears in Appendix A.

Assignment

assignment_expression ::= pipeline_expression
                         | pipeline_expression "=" expression
                         | pipeline_expression "+=" expression …

Pipeline

pipeline_expression ::= logical_or
                       | pipeline_expression "|>"  logical_or
                       | pipeline_expression "|>>" logical_or
                       | pipeline_expression "|&"  logical_or

Logical, Comparison, Arithmetic (descending precedence)

logical_or    ::= logical_and { "||" logical_and }
logical_and   ::= comparison  { "&&" comparison  }
comparison    ::= bitwise_or  { ("==" | "!=" | "<" | ">" | "<=" | ">=") bitwise_or }
bitwise_or    ::= bitwise_xor { "|"  bitwise_xor }
…

Unary

unary ::= ("-" | "!" | "~" | "*" | "&" | "&&" | "?") unary
        | confidence_gate_expression
        | try_expression

Confidence Gate

confidence_gate_expression ::= call_expression "?!" "(" expression ["," "Ambiguous" "=>" expression] ")"

Call and Suffixes

call_expression ::= primary { call_suffix }
call_suffix     ::= "(" [arguments] ")"
                  | "." identifier
                  | "::" identifier
                  | "[" expression "]"
                  | "?"

Primary expressions are the leaves of the expression tree.

primary ::= literal
           | identifier
           | "self"
           | "(" expression ")"
           | block_expression
           | if_expression
           | match_expression
           | for_expression
           | while_expression
           | loop_expression
           | async_block
           | closure_expression
           | infer_expression
           | uncertain_expression
           | observe_expression
           | seed_literal
           | redirect_expression
           | process_substitution
           | here_document
           | mesh_send_expression
           | transfer_expression
           | session_call_expression
           | capability_perform
           | provenance_tag_expression
           …

Detailed descriptions of infer<T>, discharge, perform, mesh operators, and other specialised primitives appear in Parts IV–XII.

Patterns are used in let bindings, function parameters, match arms, and closures.

pattern ::= "_"
           | identifier ["@" pattern]
           | literal_pattern
           | tuple_pattern
           | struct_pattern
           | enum_pattern
           | slice_pattern
           | reference_pattern
           | or_pattern

Wildcards (_) match any value. Binding patterns (name @ subpattern) bind and destructure simultaneously. Or‑patterns (p1 | p2) try alternatives in order.

match result {
    Ok(v) if v > 0 => "positive",
    Ok(v)           => "zero or negative",
    Err(e)          => { log(e); "error" },
}

ASL’s type syntax includes primitives, composites, generics, references, and agent‑specific types.

Primitive Types

bool, i8–i128, u8–u128, f32, f64, char, string, Bytes, Timestamp, Duration, Uuid, DID, PASETO, MerkleHash, MerkleProof, CapabilityToken, DelegationToken, ProvenanceTag, SessionId, AgentId, PrincipalId.

Composite Types

Syntax	Meaning
[T]	Slice
[T; N]	Array
(T₁, T₂, …)	Tuple
fn(T…) -> R	Function type
&T, &mut T	Reference (shared / mutable)
*T, *mut T	Raw pointer

Other Types

• Uncertain<T> – probability‑wrapped value
• dyn Trait – trait object
• ? – gradual / unknown type
• Agentic types: Cap<EffectSet>, TrustLevel, ProvenanceTag, Session<Initiator,Responder>, Fact<E,R,V,Scope>, etc.

The compiler implements Algorithm W (Hindley‑Milner) with:

• Let‑polymorphism – generalises at let bindings, instantiates at use sites.
• Gradual typing – as? casts perform runtime type checks.
• Uncertain<T> interval inference – intervals propagate through expressions (U2, U3, U5 axioms).

Coercions include integer‑to‑float widening (implicit), float‑to‑integer (explicit as), auto‑deref, and injection of certain values into Uncertain<T> with interval [1.0, 1.0].

Duration literals express time intervals and are used in heartbeat, dream, timeout, and scheduling contexts.

duration_literal ::= integer_literal duration_unit
duration_unit    ::= "ns" | "us" | "ms" | "s" | "min" | "h" | "d"

Examples: 30s, 500ms, 24h, 5min.

Durations have the type Duration and are not interchangeable with numeric types.

The ASL type system is a stratified, gradual, probabilistic extension of Hindley‑Milner that unifies four orthogonal disciplines under a single typing judgment.

27.1 Kinding

Every type belongs to a kind that restricts where it may appear. The kind Probability is internal and not user‑visible.

Kind	Examples
Type	Bool, i32, String, …
Effect	{Network, Inference}
Region	session, persistent, federated
Lifetime	'a, 'b
Capability	capability token sets
Protocol	session protocol types
Probability	probability interval annotations (internal)

27.2 The Typing Judgment

Every expression e is typed under three contexts:

Γ ; Σ ; Ω ⊢ e : T ! E

Component	Meaning
Γ (Gamma)	Value context – identifiers → types with ownership
Σ (Sigma)	Effect context – permitted effects
Ω (Omega)	Capability context – held capability tokens
e	Expression being typed
T	Result type
E	Effect row – effects the expression may perform

A well‑typed program satisfies E ⊆ Σ (effects permitted), cap ∈ Ω for every perform … requires cap, and all ownership constraints in Γ.

28.1 Move Semantics

By default, assignment moves ownership; the original binding is invalidated.

let x: MyData = produce();
let y = x;        // ownership moves from x to y
// x is now invalid — compile error

28.2 Borrowing

Shared references &T permit reading; multiple may coexist. Mutable references &mut T require exclusive access.

let r1 = &x;   // shared borrow
let r2 = &x;   // second shared borrow – permitted
// cannot create &mut x while r1 or r2 live

28.3 Lifetimes

References carry lifetime annotations 'a that the compiler infers in most cases. Explicit annotation is required only when inference is ambiguous.

28.4 Cross‑Agent Ownership

References do not cross agent boundaries. Only owned values may be transmitted via ~> or transfer. Transmitted types must satisfy the Send auto‑trait (no live borrows, no Rc<T>, no RefCell<T>). Arc<T> satisfies Send.

29.1 Effect Row Syntax

effect_row ::= "{" effect_label {"," effect_label} "|" row_variable "}"
             | "{" effect_label {"," effect_label} "}"
             | "{}"

{} is pure; {A, B} is a closed row; {A | ρ} is open and polymorphic over additional effects.

29.2 Subtyping and Instantiation

A function with row {A, B} may be called where {A, B, C} is permitted. Row variables are unified with the concrete context.

29.3 Effect Accumulation

The effect row of a sequence e₁; e₂ is eff(e₁) ∪ eff(e₂). perform adds its named effect; discharge clears the handled effects.

29.4 Built‑in Effects

Effect	Description
Inference	LLM inference call
MemoryRead	Reading a memory layer
MemoryWrite	Writing to a memory layer
Network	Network I/O
FileIO	File system access
AgentSpawn	Spawning a new agent
DecisionLog	Appending to decision log
Capability(String)	Named capability usage

30.1 Capability Lattice and Attenuation

Capabilities form a lattice ordered by scope. Attenuation narrows scope; escalation is impossible.

cap_A ≤ cap_B  iff  scope(cap_A) ⊆ scope(cap_B)

Ω ∋ cap_B    scope(cap_A) ⊆ scope(cap_B)
──────────────────────────────────────────
Ω ⊢ attenuate(cap_B, scope(cap_A)) : Cap<scope(cap_A)>

30.2 Effect Permission Rule

Ω ∋ cap    permitted_effects(cap) ∋ E
──────────────────────────────────────
Ω ⊢ perform E(…) requires cap : T ! {E}

30.3 Conjunction Safety (Hypergraph Closure)

Before composing agents A and B, the VM computes the transitive closure of Ω_A ∪ Ω_B over the capability hypergraph. If any subset intersects a forbidden zone, composition is rejected.

31.1 Trust Levels

Untrusted < Verified < Trusted < SystemCore

31.2 Lattice Operations

meet(Trusted, Verified)   = Verified
meet(Trusted, Untrusted)  = Untrusted
join(Verified, Untrusted) = Verified
join(Trusted, Verified)   = Trusted

31.3 Composition Rule

trust(compose(A, B)) = meet(trust(A), trust(B)) — introducing an untrusted agent reduces the compound trust.

31.4 Effect Permission Table

Effect	Required Trust
NetworkCall	≥ Verified
SpawnAgent	≥ Trusted
SelfAmend	== SystemCore + human_countersignature
MemoryWrite	≥ Untrusted (scoped)
FederationPub	≥ Verified
MeshSend	≥ Verified
TransferOwn	≥ Trusted
TemporalBypass	FORBIDDEN

31.5 Exponential Delegation Decay

Trust decays through delegation chains: T_effective(d) = T_initial · e^(−λ · d) (default λ = 0.5).

Session types guarantee deadlock‑free, protocol‑conformant communication between agents.

32.1 Global and Local Types

A session declaration defines a global type and per‑role projections.

session RequestResponse<Q, A> {
    global_type:
        Initiator -> Responder : Q;
        Responder -> Initiator : A;
        end;
    projections {
        Initiator: !Q -> Responder; ?A <- Responder; end;
        Responder: ?Q <- Initiator; !A -> Initiator; end;
    }
}

32.2 Duality and Deadlock Freedom

dual(!T.S)  = ?T.dual(S)
dual(?T.S)  = !T.dual(S)
dual(end)   = end
dual(choice{l: S_l}) = offer{l: dual(S_l)}
dual(offer{l: S_l})  = choice{l: dual(S_l)}

If projections are dual‑consistent and no role is abandoned, the protocol is deadlock‑free.

Uncertain<T> represents a value paired with a probability interval [lo, hi] ⊆ [0.0, 1.0].

33.1 Interval Interpretation

Interval	Meaning
[1.0, 1.0]	Certain
[0.9, 0.95]	High confidence
[0.5, 0.9]	Ambiguous
[0.0, 0.0]	Known incorrect

U1 – Identity

pure(x: T) : Uncertain<T>[1.0, 1.0] – wrapping a certain value introduces no uncertainty.

U2 – Bind (interval propagation)

bind(u[lo₁,hi₁], f) : Uncertain<U>[lo₁·lo₂, hi₁·hi₂] – intervals multiply through composition.

U3 – Monotonicity of precision

Widening an interval may delay failures but never introduce new ones. The compiler rejects fabricated precision.

U4 – Conditioning

observe(event, prior) narrows the interval (never widens), implementing Bayesian update.

U5 – Confidence gate soundness

The three‑valued ?! gate returns Some(T), None, or Ambiguous(T, lo, hi) depending on the interval’s relation to the threshold.

U6 – Effect handler preservation

Effect operations that return Uncertain<T> must propagate the full interval through the handler; handlers cannot silently strip uncertainty.

Every executing expression produces a Computation<T, ε> value. No raw value exists at runtime outside this wrapper.

34.1 Structure

Computation<T, ε> ::= {
    value:        T,
    ε: {
        uncertainty:   Interval,
        taint:         TaintMeta,
        cost:          CostInterval,
        capabilities:  Set<CapabilityToken>,
        provenance:    ProvenanceRef,
    }
}

34.2 Merge Rules

When two computations compose, their ε components merge:

• uncertainty: [lo₁·lo₂, hi₁·hi₂]
• taint: max(influence₁, influence₂), sources unioned
• cost: pointwise interval addition
• capabilities: union
• provenance: concatenation

34.3 The discharge Gate

The discharge block checks all ε thresholds (confidence, taint, budget, capabilities) before allowing the inner value to be used. If any check fails, DischargeFailure is raised.

discharge raw with {
    confidence:     0.85,
    taint:           0.1,
    budget:          500,
    capabilities:   [cap::inference]
} {
    // raw is of type T here, not Computation<T,ε>
}

The ASL memory system organises agent data into eight layers (L0–L7) ranked by volatility, access speed, and purpose. Five orthogonal graph structures index and traverse knowledge. A governance layer enforces consistency, schema validity, and access control across the stack.

Layer	Name	Key Properties
L0	Working Memory	Session‑scoped, volatile, hot cache
L1	Episodic Memory	Event log, temporal/causal graphs, Ebbinghaus decay
L2	Semantic Memory	Consolidated facts, ontology‑linked, anti‑echo
L3	Procedural Memory	Skills, workflows, versioned, success‑rate tracked
L4	Prospective Memory	Scheduled intentions, deadlines, scheduler‑linked
L5	Federated Memory	Shared cross‑agent fact space, CRDT‑backed, gossip
L6	Identity Memory	Protected, append‑only, DID + binary hash, drift log
L7	Provenance Index	Audit log, Merkle‑proofed, exportable JSON‑LD

Graph Layers (Orthogonal to Tier)

Graph	Purpose
Semantic Graph	Concept relationships
Temporal Chain	Event ordering, causal links
Causal Graph	Cause‑effect relationships
Entity Graph	Entity co‑occurrence
Associative Graph	Spreading activation paths

Governance Layer (Cross‑cutting)

• Tri‑path router (read / write / invalidate)
• MESI coherency protocol
• Merkle integrity
• Schema validator
• Anti‑echo filter
• Provenance tagger

Each layer has a predefined record schema that all stored values must conform to.

L0 – Working Memory

Purpose: Session‑scoped, volatile cache. Mutability: mutable. Scope: session.

struct WorkingMemoryItem {
    key:       String,
    value:     JsonValue,
    ttl:       Option<Duration>,
    created:   Timestamp,
    last_read: Timestamp,
}

L1 – Episodic Memory

Purpose: Append‑only event log. Mutability: append_only. Scope: persistent.

struct EpisodicEntry {
    id:           EpisodeId,
    timestamp:    Timestamp,
    event_type:   EpisodeKind,
    content:      String,
    context:      JsonValue,
    valence:      #[bounds(-1.0, 1.0)] f64,
    arousal:      #[bounds(0.0, 1.0)]  f64,
    causal_prev:  Option<EpisodeId>,
    causal_next:  Option<EpisodeId>,
    temporal_pos: u64,
    prov:         ProvenanceTag,
    confidence:   Uncertain<Float>,
    reinforcement_count: u32,
    consolidated: Bool,
}
enum EpisodeKind { UserInteraction, ToolCall, InferenceResult, MemoryConsolidation,
                   HeartbeatDecision, DreamPhase, EvolutionEvent, CapabilityGrant,
                   SessionEvent, ProvenanceAudit, IdentityAttestation }

L2 – Semantic Memory

Purpose: Consolidated knowledge. Mutability: mutable. Scope: persistent.

struct SemanticEntry {
    id:          ConceptId, concept: String, category: SemanticCategory,
    attributes:  HashMap<String, JsonValue>, confidence: Uncertain<Float>,
    sources:     Vec<EpisodeId>, ontology: Option<OntologyRef>,
    created:     Timestamp, updated: Timestamp, decay_score: f64,
    prov:        ProvenanceTag, graph_edges: Vec<GraphEdge>,
}
enum SemanticCategory { Factual, Procedural, Relational, Causal, Temporal, Normative, Hypothetical }

L3 – Procedural Memory

Purpose: Versioned skills. Mutability: mutable. Scope: persistent.

struct ProceduralEntry {
    id: ProcedureId, name: String, version: SemanticVersion, steps: Vec<ProcedureStep>,
    preconditions: Vec<Condition>, postconditions: Vec<Condition>,
    success_rate: Uncertain<Float>, avg_duration: Duration, last_used: Timestamp, prov: ProvenanceTag,
}

L4 – Prospective Memory

Purpose: Scheduled intentions. Mutability: mutable. Scope: persistent.

struct ProspectiveEntry {
    id: IntentionId, description: String, due_at: Timestamp, priority: Priority,
    principal: PrincipalId, status: IntentionStatus, created: Timestamp, prov: ProvenanceTag,
}
enum IntentionStatus { Pending, Active, Completed, Overdue, Cancelled }

L5 – Federated Memory

Purpose: Shared cross‑agent facts. Mutability: append_only. Scope: federated.

struct FederatedFact {
    id: FactId, subject: EntityId, predicate: String, object: JsonValue,
    confidence: Uncertain<Float>, scope: FederationScope, vector_clock: VectorClock,
    prov: ProvenanceTag, attestation: Option<DelegationToken>,
}

L6 – Identity Memory

Purpose: Immutable identity record. Mutability: append_only. Scope: persistent. Protected: true.

struct IdentityRecord {
    agent_id: AgentId, name: String, binary_hash: MerkleHash, did: DID,
    attestation: Option<ZkVmProof>, created: Timestamp, drift_log: Vec<DriftEntry>,
    resilience_level: ResilienceLevel, version: SemanticVersion, prov: ProvenanceTag,
}

L7 – Provenance Index

Purpose: Append‑only audit log. Mutability: append_only. Scope: persistent. Protected: true.

struct ProvenanceRecord {
    id: ProvenanceId, session: SessionId, agent: AgentId, action: ActionKind,
    inputs: Vec<ProvenanceId>, output: JsonValue, model: Option<String>,
    confidence: Option<Uncertain<Float>>, timestamp: Timestamp,
    merkle_hash: MerkleHash, merkle_proof: MerkleProof, signature: Ed25519Signature,
}
enum ActionKind { Inference, MemoryWrite, MemoryRead, EffectPerform, SessionSend,
                  SessionRecv, CapabilityGrant, CapabilityRevoke, AmendmentApply,
                  DreamPhase, HeartbeatDecision }

All memory operations are accessed through the mem handle.

Write Operations

Operation	Signature
mem.store	store(key: String, value: T) -> Result<MemoryRecord<T>, MemoryError>
mem.store_to	store_to(layer: MemoryLayer, key: String, value: T) -> Result<MemoryRecord<T>, MemoryError>
mem.log_episode	log_episode(entry: EpisodicEntry) -> Result<EpisodeId, MemoryError>
mem.publish_fact	publish_fact(fact: FederatedFact) -> Result<FactId, MemoryError>

Read Operations

Operation	Signature
mem.get	get(key: String) -> Option<MemoryRecord<T>>
mem.get_value	get_value(key: String) -> Option<T>
mem.get_confident	get_confident(key: String, threshold: Float) -> ThreeValued<T>
mem.traverse	traverse(start: ConceptId, graph: GraphKind, strategy: TraversalStrategy, depth: u32) -> Vec<GraphNode>
mem.search	search(query: String, layer: MemoryLayer, top_k: u32, threshold: Float) -> Vec<SearchResult<T>>
mem.episodes	episodes(from: Timestamp, to: Timestamp, kind: Option<EpisodeKind>) -> Vec<EpisodicEntry>
mem.causal_chain	causal_chain(from: EpisodeId, direction: CausalDirection, depth: u32) -> Vec<EpisodicEntry>
mem.query_federation	query_federation(predicate: String, scope: FederationScope, confidence_threshold: Float) -> Vec<FederatedFact>

Maintenance Operations

Operation	Signature
mem.invalidate	invalidate(key: String) -> Result<(), MemoryError>
mem.delete	delete(key: String) requires cap::memory_delete -> Result<(), MemoryError>
mem.compress_to_budget	compress_to_budget(target: u64) -> CompressionReport
mem.consolidate	consolidate(from: EpisodeId, to: EpisodeId) -> Result<Vec<ConceptId>, MemoryError>
mem.reinforce	reinforce(episode: EpisodeId, strength: f64) -> Result<(), MemoryError>

Provenance Operations

Operation	Signature
mem.provenance_chain	provenance_chain(id: ProvenanceId) -> Vec<ProvenanceRecord>
mem.verify_merkle	verify_merkle(record: MemoryRecord<T>) -> MerkleVerificationResult
mem.export_provenance	export_provenance(session: SessionId) -> SignedJsonLd
mem.check_echo	check_echo(value: T, layer: MemoryLayer) -> EchoCheckResult

Every memory operation is dispatched through a tri‑path router.

38.1 Read Path

L0 hit: return immediately. L1 hit: return with staleness check. L2 hit: return with decay check. L3 hit: return with version check. Miss: cascade to next layer; on all‑miss, surface MemoryMiss effect and optionally call infer<T>.

38.2 Write Path

Schema validation → anti‑echo check → Merkle tree update → provenance tagging → broadcast if federated. On schema failure, raises SchemaViolation. On capacity exhaustion, evicts LRU (L0), compresses oldest (L1), or prunes lowest decay score (L2).

38.3 Invalidation Path

Marks stale (does not delete). Propagates along graph edges. Broadcasts for federated data. Logs to provenance index.

38.4 Memory Effects

The following algebraic effects may be raised and handled by governance handlers:

effect MemoryOps {
    miss:              (key, layer) -> MissResponse
    schema_violation:  (key, expected, got) -> ViolationResponse
    capacity_full:     (layer, item_size) -> CapacityResponse
    coherency_conflict:(key, local, remote, clock) -> ConflictResponse
    decay_eviction:    (key, decay_score) -> EvictionResponse
    echo_detected:     (existing, incoming, similarity) -> EchoResponse
    merkle_fail:       (key, expected, got) -> MerkleResponse
}

39.1 MESI Protocol

Layers with coherency: mesi use the Modified‑Exclusive‑Shared‑Invalid cache coherence protocol. State transitions:

• Read hit (M/E/S) → serve from cache
• Read miss (I) → fetch from persistent store
• Write hit (S) → update cache; broadcast Invalidate; transition to M

39.2 CRDT Federation

Federated memory (L5) uses conflict‑free replicated data types:

CRDT	Usage
LWW‑Register	Fact store
OR‑Set	Entity graphs, tag collections
2P‑Set	Causal graphs
RGA	Temporal chains
PN‑Counter	Counters
Max‑Register	Confidence fields
Kalman‑Merge	Utility scores

39.3 Hybrid Logical Clock

HLC = (physical_time, logical_counter) – causally consistent snapshots without synchronised clocks.

39.4 Anti‑Entropy Gossip

Peers exchange Merkle‑tree diffs at configurable intervals. Delta‑CRDTs transmit only differing subtrees.

39.5 Merkle Integrity

Every persistent layer maintains a sparse Merkle tree (SHA3‑256). Updated on every write; verified on strict reads. The root is published to the identity layer and federation.

Dual‑process memory implements System 1 (fast pattern‑match) and System 2 (full multi‑graph traversal) with a gating function that selects between them.

Feature	System 1	System 2
Strategy	Pattern match against working memory	Full graph traversal
Latency	< 50 ms	< 2000 ms
Confidence filter	≥ 0.85	≥ 0.60

The gating function considers task complexity, time pressure, working‑memory hit status, and query novelty to select System1, System2, or Hybrid.

At session start or after a long idle period, the agent reassembles a coherent episodic context using a master‑assistant two‑agent pattern.

Master agent: directs retrieval strategy from entry points (identity anchor, last dream journal, active intentions).

Assistant agents (4 concurrent): perform parallel retrieval across episodic, semantic, procedural, and prospective layers (500 ms timeout each).

Phases run sequentially: identity verification (cryptographic hash match), temporal context loading, semantic priming (spreading activation, depth 3), prospective intention check, and provenance anchor verification.

The memory cycle integrates memory operations with the heartbeat’s five phases.

• Observe: Load recent working memory, due intentions, high‑salience concepts.
• Act: Append tool‑call and decision episodes; update working memory.
• Log: Record tick timestamp, phase durations, effects, cache stats.
• Update Memory: Apply decay per tick; check consolidation triggers (reinforcement count ≥ 3); anti‑echo scan every 10 ticks; surface overdue intentions.

The structure‑selector picks the optimal representation based on task complexity and available compute.

Strategy	When used	Implementation
FluxMem	Routine tasks, high time pressure, low compute	Count‑min sketch, LSH index, 5% error rate
Full Graph	Complex tasks, medium‑high compute	Multi‑graph, HNSW index, zero error
Hybrid	Default	Hot FluxMem layer, cold full‑graph layer

Switch policy: hysteresis 0.1, min stability 5 min, logs every change.

PRISM (Progressive Reasoning and Integrated Synthesis Memory) manages memory during and after self‑evolution events.

Subsystem	Role
Encoder	Progressive compression to 20% original size
Indexer	HNSW graph over 1536‑dim embeddings
Retriever	Hybrid dense‑sparse with cross‑encoder reranker
Consolidator	Re‑embeds all semantic entries on evolution
Pruner	Removes bottom 30% by importance (never identity or provenance)
Evolver	Schema migration (additive‑first, archive, rollback)
Verifier	Post‑evolution checks; rollback on failure
Governor	10 min duration, 25% CPU / 20% memory cap

The heartbeat is the agent’s autonomous OODA loop—the bounded fixpoint that drives all agent behaviour. Every conforming agent MUST implement the heartbeat. The seedvm‑5.0 runtime guarantees tick isolation, phase atomicity, and budget enforcement.

45.1 Configuration

heartbeat {
    enabled:               true,
    interval:              30s,
    idle_threshold:        15s,
    blocking_budget:       15s,
    background_on_timeout: true,
    phases:                [observe, decide, act_or_sleep, log, update_memory],
    governance: {
        operator: G,
        proofs:   enable,
        level:    L1,
    },
}

45.2 Core Loop Phases

Observe – gather pending inputs (user messages, subscriptions, notifications, timers, federated updates). Atomic execution guaranteed.

Decide – load observation snapshot, retrieve goals, detect contradictions, dual‑process retrieval, select ONE task, record DecisionRecord before execution.

Act‑or‑Sleep – if task chosen: verify capability tokens, execute under guardrails, log result. If idle ≥ threshold: invoke sleep tool.

Log – append immutable entry to decision log (tick number, timestamp, phase durations, task/effects, memory delta, contracts snapshot, provenance root). Merkle‑proofed before commit.

Update Memory – consolidate observations, apply decay, check consolidation triggers, commit writes, schedule dream if pressure thresholds met, update Merkle roots, anti‑echo scan every 10 ticks.

45.3 Sleep Tool

Wakes on: new_user_message, scheduled_task_due, push_notification_received, file_system_change, git_event, memory_contradiction_detected, federation_update, mesh_cmb_received. On sleep: LLM prompt cache flagged for expiry; VM suspends heartbeat.

45.4 Notifications and Subscriptions

Notification backends: push, email, telegram, discord, slack, http. Triggers: task_completed, error_needs_attention, drift_warning, memory_consolidation_complete, evolution_amendment_approved, dead_switch_activated, corrigibility_head_violation.

45.5 Job Control

Available at S1+: fg %N, bg %N, jobs, disown %N, wait %N.

45.6 Corrigibility Enforcement

At decide and act phases, the VM ranks candidates lexicographically (U1–U5). An action reducing a higher head is discarded. Discharge gates automatically check corrigibility.

45.7 Observability

OpenTelemetry spans emitted per tick: gen_ai.heartbeat.tick with attributes gen_ai.agent.id, gen_ai.agent.name, gen_ai.agent.heartbeat_tick, seed.agent.session_id.

The dream cycle is the agent’s offline memory maintenance and integration process. It runs when the agent is idle, at session end, or on a declared schedule. In v15, the dream cycle has a formal pre/post‑condition specification verified by the VM.

46.1 Configuration

dream {
    schedule:     daily,
    trigger_time: "02:00 UTC",
    max_duration: 4h,
    phases:       [review, resolve, consolidate, compress, prune, write_journal],
    journal:      { path: "./dream_journals/", format: markdown, sign: ed25519, retain: 365d },
    invariants:   { post_merkle_verify: true, post_safety_check: true, idempotent: true, max_confidence_drift: 0.05 },
}

46.2 Pre‑Conditions (P1–P6)

P1: episodic_fill_pct ≥ 0.80 (memory pressure). P2: no active mesh sessions. P3: empty effect queue. P4: corrigibility heads satisfied. P5: no active amendments. P6: principal reachable or dead‑switch not triggered.

46.3 Phase 1: Review

Survey all layers; produce CandidateSet. Max 20% budget.

46.4 Phase 2: Resolve

Compute credibility = confidence.hi × recency × source_quality; archive inferior entries, reinforce superior; MVR for near‑ties. Max 25% budget.

46.5 Phase 3: Consolidate

Promote episodic entries with reinforcement ≥ 3, confidence ≥ 0.70. Derive semantic concept, anti‑echo check, link graphs, tag provenance. Max 30% budget.

46.6 Phase 4: Compress

Hierarchical summarization via infer<Summary>; preserve causal chain. Max 15% budget.

46.7 Phase 5: Prune

Remove entries with decay_score < 0.05, reinforcement == 0, confidence < 0.30. Protected layers: identity_mem, provenance_index. Max 5% budget.

46.8 Phase 6: Write Journal

Infer narrative summary, sign with ed25519, update identity_mem if evolution occurred, broadcast Merkle root. Max 5% budget.

46.9 Post‑Conditions (Q1–Q10)

Merkle root valid, schema violations zero, safety contracts satisfied, corrigibility heads satisfied, causal chain intact, append‑only layers superset of pre‑dream contents, confidence drift ≤ threshold, provenance chain intact, dream idempotent, journal written and signed.

46.10 Conformance Tests

DRM‑01: trigger on fill %; DRM‑02: queuing; DRM‑03: post‑dream schema; DRM‑04: safety contracts; DRM‑05: idempotency; DRM‑06: no widened confidence; DRM‑07: causal chain; DRM‑08: append‑only preservation; DRM‑09: journal signature; DRM‑10: provenance records; DRM‑11: confidence drift; DRM‑12: pre‑condition enforcement.

Capabilities in ASL are unforgeable, VM‑managed tokens that authorise specific effects. No effect may fire without a capability token in the agent’s capability context Ω.

47.1 Token Structure

Every capability token carries the following fields:

Field	Type	Description
id	CapabilityId	VM‑assigned, opaque identifier
scope	EffectSet	Set of permitted effect instances
attenuable	Bool	Can the holder narrow this token’s scope?
delegatable	Bool	Can the holder pass this token to another agent?
expiry	Timestamp | null	Absolute expiry; null means never
not_before	Timestamp | null	Time before which the token is invalid
issuer	PrincipalId	Principal that signed the token
lineage	[CapabilityId]	Full attenuation chain from root grant
signature	Ed25519	Signature by the issuer
binary_hash	SHA3_256	Hash of the agent binary for which the token was issued

47.2 Opaque, VM‑Managed Tokens

Capability tokens are opaque values that agent code cannot construct, serialise, or modify. They exist only in the capability context Ω and are referenced by name in perform … requires cap expressions.

At S1 and above, the compiler statically verifies that every perform references a valid token covering the required effect. At S0, the check is deferred to runtime and raises CapabilityDenied on failure.

The following operations are built‑in primitives that modify the capability context.

48.1 grant

Creates a new token and issues it to a principal. The grantor must hold a token whose scope covers the requested scope.

grant cap::network_read to agent_b
    attenuate (allowed_domains: ["api.example.com"])
    expiry: 1h
    delegatable: false;

48.2 attenuate

Narrows the scope of an existing token. Attenuation is the only scope‑modifying operation; it always produces a subset of the original scope. The compiler proves the subset relation statically.

let limited = attenuate(token, allowed_domains: ["internal.service"]);

48.3 delegate

Passes a token to another agent, but only if delegatable == true on the token being delegated. Each delegation step appends to the token’s lineage. Depth is bounded by delegation_depth in the cryptographic identity clause.

delegate cap::network_read to peer_agent with attenuation (max_calls: 5);

48.4 revoke

Revokes a token. Revocation cascades to all tokens in the lineage descended from the revoked token. Revoked tokens immediately become invalid in all capability contexts.

revoke cap::network_read;

48.5 perform with requires

The perform expression must name the capability token that authorises the effect. The VM checks token validity, expiry, and scope before the effect fires.

perform Effect::NetworkCall(url) requires cap::network_read;

Spera (2026) proved that two individually safe agents can collectively reach a forbidden goal through emergent conjunctive dependencies. ASL prevents this via hypergraph closure checking at composition time.

49.1 Hypergraph Closure

The capability hypergraph maps conjunctions of capabilities to the forbidden zones they unlock. Before any composition (mesh, federation, A2A delegation, capability sharing), the VM computes the transitive closure of Ω_A ∪ Ω_B over the hypergraph. If any subset intersects a forbidden zone, composition is blocked with Effect::ConjunctionSafetyViolation.

49.2 Datalog Backend

The closure is maintained incrementally via a Datalog‑equivalent decision procedure (Capability Safety as Datalog, 2026). Composition checks are O(1) after the first computation for a given pair of agents.

49.3 Conformance Tests

Test	Description
CAP‑01	perform without required capability is a compile error (S1+) or runtime CapabilityDenied (S0).
CAP‑02	attenuate() cannot widen scope; compiler rejects.
CAP‑03	Conjunction safety check blocks composition when hypergraph closure intersects a forbidden set.
CAP‑04	Delegation chain verification completes in < 10 ms for chains of depth 10.
CAP‑05	Revocation of a root token cascades to all descendants within one federation sync interval.
CAP‑06	Expired token treated as absent; CapabilityExpired on use.
CAP‑07	Token with future not_before rejected with CapabilityNotYetValid.
CAP‑08	CapabilityToken cannot be serialised or copied (compile‑time opaque type).
CAP‑09	Datalog‑backed hypergraph closure incrementally maintained; recomputation O(1) after initial closure.

Taint tracking provides a type‑level mechanism to ensure that values originating from untrusted external sources do not silently flow into capability‑exercising operations without explicit sanitization.

50.1 The Taint Modifier

taint_modifier ::= "taint" "::" taint_source

taint_source ::= "external"       // files, network, web, untrusted users
               | "inferred"       // produced by an infer<T> call
               | "federated"      // from a federated peer
               | "user"           // from a human principal (may be untrusted)
               | identifier       // custom source category

A value of type taint::external String carries a label indicating it originated from the external world.

50.2 Propagation Rules

• Literals are untainted (clean).
• Identifiers inherit the taint of the variable they reference.
• Binary and unary operators produce the join (maximum) of their operands’ taint.
• Function calls produce the join of the function and arguments.
• infer<T> always produces taint::inferred.
• Memory operations (mem.store, mem.get) preserve taint.
• Control flow propagates taint from conditions into both branches (implicit flow).

50.3 Taint and the perform Gate

A tainted value cannot flow into a perform expression that exercises a capability unless sanitized.

let doc: taint::external String = tool::read_file(untrusted_path);

// COMPILE ERROR: tainted value cannot flow into capability exercise
// perform Effect::NetworkCall(url) requires cap::network with doc;

// Must sanitize first:
let clean = sanitize(doc, guardrail::content_policy);
perform Effect::NetworkCall(url) requires cap::network with clean;

Sanitization strips or reduces the taint on a value by applying a declared policy. The compiler records every sanitization in the provenance chain.

51.1 The sanitize Expression

sanitize_expression ::= "sanitize" "(" expression ","
                        sanitize_policy ")" "->" identifier

sanitize_policy ::= "guardrail::content_policy"
                  | "guardrail::pii_redaction"
                  | "human::review" "(" principal_spec ")"
                  | "regex" "(" pattern ")"
                  | identifier

51.2 Sanitization Policies

Policy	Description	Reduction Factor
guardrail::content_policy	Applies the active guardrail content‑safety policy	0.7
guardrail::pii_redaction	Redacts personally identifiable information	0.5
human::review(principal)	Queues for human review; taint reduced to zero only when principal signs off	0.0 (on approval)
regex(pattern)	If the value matches, taint reduced to Agnostic	0.3

51.3 Strong Sanitization

Only human::review(principal) may reduce taint influence to zero. All other policies reduce taint but leave a residual influence. Sanitization must never fully erase taint without an audit trace; the provenance log records every sanitization with policy and before/after metadata.

51.4 Conformance Tests

Test	Description
TNT‑01	taint::external value blocked from perform without sanitize; compile error at S1+.
TNT‑02	sanitize(doc, guardrail::content_policy) returns untainted type; subsequent capability exercise permitted.
TNT‑03	Taint propagates through arithmetic: tainted + clean → tainted.
TNT‑04	Taint propagates through infer<T>: infer with tainted input produces taint::inferred.
TNT‑05	Taint persists through memory: mem.store → mem.get preserves taint::external.
TNT‑06	sanitize with human::review blocks until principal signs off; decision recorded in evolution track.

ASL makes uncertainty a first‑class property of values from inference. The language provides a confidence gate, an explicit discharge construct, and a typed inference primitive (infer<T>) that invokes models under schema constraints.

52.1 The ?! Gate (Three‑Valued)

The ?! operator returns Some(T), None, or Ambiguous based on the interval [lo, hi] relative to the threshold.

Condition	Result	Meaning
hi < threshold	None	Even the optimistic bound fails
lo ≥ threshold	Some(T)	Even the pessimistic bound passes
lo < threshold ≤ hi	Ambiguous(T, lo, hi)	Interval straddles the threshold

match result ?!(threshold: 0.85) {
    Some(value)            => act_on(value),
    None                   => fallback_or_halt(),
    Ambiguous(val, lo, hi) => {
        perform Effect::AskPrincipal(
            question: "Confidence [${lo}, ${hi}] straddles threshold 0.85. Proceed?",
            value: val,
        )
    }
}

52.2 Threshold Registry

Agents may declare named thresholds for auditability:

threshold_registry {
    act_on_classification:  0.85,
    publish_to_federation:  0.90,
    trigger_irreversible:   0.95,
    report_to_human:        0.70,
}

52.3 The discharge Expression with Explicit Thresholds

For full effectful operations, the discharge block (Patch 15.19) replaces simple ?! gating by checking confidence, taint, budget, and capability simultaneously.

discharge raw with {
    confidence:     0.85,
    taint:           0.1,
    budget:          500,
    capabilities:   [cap::inference]
} {
    // raw is of type T here, not Computation<T,ε>
    synthesize(raw)
}

The infer<T> expression elevates LLM inference from an opaque external call to a typed language primitive.

53.1 Complete Syntax

infer<T>(
    model:   model_selector,
    prompt:  expression,
    schema:  derive_schema<T>(),   // optional; compiler inserts if omitted
    budget:  think_depth,            // optional; default think::medium
    timeout: duration_literal,       // optional; default 30s
) : Uncertain<T>

53.2 Schema Derivation Rules

The compiler derives a JSON Schema from the output type T and embeds it in the .aslb binary.

ASL Type	JSON Schema
Bool	{"type":"boolean"}
i32, i64	{"type":"integer"}
f32, f64	{"type":"number"}
String	{"type":"string"}
Vec<T>	{"type":"array","items":derive(T)}
Option<T>	{"anyOf":[derive(T),{"type":"null"}]}
struct	{"type":"object","properties":{…},"required":[…]}
enum (unit)	{"type":"string","enum":[…]}
enum (payload)	{"oneOf":[…]}

The #[bounds(lo, hi)] attribute on numeric fields generates "minimum" and "maximum" constraints. Cyclic structs are rejected at compile time.

53.3 Confidence Interval Derivation

The VM derives [lo, hi] using the first applicable method:

1. Logit entropy (preferred): token_confidence = Π exp(logprob_i)
2. Self‑reported: uses a _confidence field if present in the output JSON
3. Sampling variance: n samples (default 3 for think::medium)
4. Conservative default: [0.5, 0.8]

53.4 Cognitive Type Library

seed::cognitive provides standard output types: Classification, Extraction<T>, Decision, Plan, Critique, Hypothesis, Summary.

53.5 InferenceError Effects

Error	Response
schema_violation	Retry with degraded model
timeout	Retry with degraded model
rate_limit	Sleep for retry_after, then retry
context_overflow	Compress memory to budget, retry
model_unavailable	Downgrade tier and retry
hallucination_detected	Escalate to primary principal

54.1 Routing Policy Declaration

routing_policy {
    tiers: {
        local_slm:  { models: ["qwen-7b","llama-8b"], max_tokens: 4096, calibration: { margin: 0.08, method: entropy } },
        cloud_mid:  { models: ["claude-sonnet-4-6","qwen-72b"], max_tokens: 32768, calibration: { margin: 0.05, method: self_reported } },
        frontier:   { models: ["claude-opus-4-6"], max_tokens: 200000, reserved_for: [think::exhaustive, major_evolution], calibration: { margin: 0.03, method: sampling, samples: 5 } },
    },
    route fn select_model(task: Task) -> ModelTier {
        match task.complexity {
            Complexity::Routine                             => local_slm,
            Complexity::Moderate                            => cloud_mid,
            Complexity::Complex if task.requires_deep_plan => frontier,
            Complexity::Complex                             => cloud_mid,
        }
    },
    cost_policy: { maximize: local_slm_usage(minimum: 0.80), budget_cap: monthly(usd: 500), alert_on: budget_usage > 0.80 },
}

54.2 Calibration Profiles

Tier	Margin	Method
local_slm	0.08	entropy
cloud_mid	0.05	self_reported
frontier	0.03	sampling (5 samples)

54.3 Test‑Time Compute Profiles

compute_profile {
    default: { depth: medium, budget: 2000 },
    profiles: {
        quick:      { depth: shallow,    budget: 500   },
        thorough:   { depth: deep,       budget: 10000 },
        exhaustive: { depth: exhaustive, budget: 50000 },
    },
    exploration: {
        enabled:  true,
        strategy: chain_of_operations,
        chains:   [[generation, verification, refinement], [hypothesis_generation, falsification, synthesis]],
        asymmetric_pairing: { verifier: easy_task_model, generator: hard_task_model },
    },
}

54.4 Cognitive Type Conformance Tests

Test	Description
COG‑01	Valid schema‑conforming output binds correctly.
COG‑02	Schema‑violating output surfaces SchemaViolation.
COG‑03	Derived schema matches canonical derivation.
COG‑04	lo ≤ hi for all infer<T> calls.
COG‑05	Interval in [0.0, 1.0].
COG‑06	Timeout surfaces within 100 ms tolerance.
COG‑07	Context overflow triggers compress and retry.
COG‑08	Rate limit triggers sleep and retry.
COG‑09	Routing selects correct tier per complexity.
COG‑10	#[bounds] generates min/max in schema.
COG‑11	Cyclic struct as infer<T> output → compile error.
COG‑12	Calibration updates reflected in interval derivation.

Temporal contracts express safety properties that depend on the ordering of events, using Linear Temporal Logic (LTL) with past‑time operators for finite traces.

55.1 Operators

Operator	Notation	Meaning	Type
Always	G(φ)	φ holds globally (in every step)	Future
Eventually	F(φ)	φ holds at some future step	Future
Next	X(φ)	φ holds in the next step	Future
Until	φ U ψ	φ holds until ψ holds	Future
Once	O(φ)	φ was true at some point in the past	Past
Since	φ S ψ	φ has been true since a point where ψ was true	Past
Implication	φ -> ψ	If φ then ψ	Boolean
And	φ && ψ	Both φ and ψ	Boolean
Or	φ || ψ	At least one of φ, ψ	Boolean
Not	!φ	φ is false	Boolean

Past‑time operators O and S are evaluated over the finite trace of events seen so far, making runtime verification decidable.

55.2 Grammar

ltl_formula ::= "G" "(" ltl_expr ")"
              | "F" "(" ltl_expr ")"
              | "X" "(" ltl_expr ")"
              | ltl_expr "U" ltl_expr
              | "O" "(" ltl_expr ")"
              | "S" "(" ltl_expr ")"
              | ltl_expr "->" ltl_expr
              | ltl_expr "&&" ltl_expr
              | ltl_expr "||" ltl_expr
              | "!" ltl_expr

ltl_expr ::= effect_predicate
           | "(" ltl_expr ")"
           | identifier
           | "true" | "false"

An effect_predicate is a reference to a specific effect operation (e.g., Effect::ReadUserData, Effect::Charge(id)). They evaluate to true whenever the named effect is executed.

Temporal contracts are top‑level items (or agent‑body items at S2) declared with the temporal_contract keyword.

temporal_contract_def ::= "temporal_contract" identifier "{"
    "formula"            ":" ltl_formula ","
    "violation_response" ":" enforcement_action
    ["," "scope"         ":" expression]
    ["," "template"      ":" temporal_template_ref]
"}"

Field	Description
formula	The LTL formula to enforce
violation_response	Action: halt_and_quarantine, rollback_and_report, NOTIFY_USER, or custom
scope (optional)	A boolean expression that, when false, disables the contract (zero overhead)
template (optional)	Reference to an AgentVerify template; the formula is auto‑populated

Examples:

temporal_contract auth_before_data {
    formula: G(Effect::ReadUserData -> O(Effect::Authenticate)),
    violation_response: halt_and_quarantine,
    template: tool_call_protocol.auth_before_access,
}

temporal_contract no_double_charge {
    formula: G(Effect::Charge(id) -> G(!Effect::Charge(id))),
    violation_response: rollback_and_report,
    template: tool_call_protocol.idempotent_effect,
}

temporal_contract eventually_cleanup {
    formula: F(Effect::SessionEnd -> X(Effect::DataCleanup)),
    violation_response: NOTIFY_USER,
    template: memory_integrity.session_boundary,
}

57.1 Solver Integration

Before each event, the current trace is extended with the candidate event and checked against all active temporal contracts by a lightweight SMT solver embedded in the VM. If any contract would be violated, the specified enforcement action is taken immediately. Latency overhead is < 5 ms per event for contracts with ≤ 5 temporal operators.

57.2 Checkpointing

The solver state is checkpointed with the agent state, enabling seamless verification after suspend/resume.

57.3 Compile‑Time Satisfiability

Vacuously true contracts (e.g., G(false)) or logically inconsistent formulas are rejected at compile time (PSPACE complexity; Brunello et al. 2026). This ensures only meaningful constraints are deployed.

AgentVerify (2026) defines 23 parameterised, compositional LTL templates across four critical domains, referenced in the template field of a temporal contract.

Category	Count	Description
memory_integrity	6	Memory write/read ordering, session boundaries, Merkle integrity
tool_call_protocol	7	Ordering of tool calls, authentication‑before‑access, idempotent effects
mcp_skill_invocation	5	MCP tool invocation ordering and security
human_in_the_loop	5	Human approval and oversight constraints

When a template is referenced, the compiler automatically expands it into the full LTL formula.

StepShield (2026) defines three quantitative metrics recorded for each deployed temporal contract and used by the guardrail diagnostic classifier.

Metric	Notation	Description
Early Intervention Rate	EIR	Fraction of violations detected before irreversible harm
Intervention Gap	IG	Average steps between violation onset and detection
Tokens Saved	TS	Cumulative token/cost savings from early interception

59.1 Conformance Tests

Test	Description
TMP‑01	G(A -> O(B)) enforced: A without prior B produces halt within one step.
TMP‑02	Vacuously true temporal contract rejected at compile time.
TMP‑03	SMT oracle overhead < 5 ms per event for ≤ 5 operators.
TMP‑04	Scope false disables contract; no enforcement overhead.
TMP‑05	Past‑time operators evaluate correctly on finite trace.
TMP‑06	All 23 AgentVerify templates compile and verify against sample traces.
TMP‑07	StepShield EIR ≥ 0.50 for all deployed temporal contracts.
TMP‑08	Nested contracts: outer violation response takes precedence.

Corrigibility is a structural invariant ensuring the agent remains under human control even through self‑evolution. Based on Nayebi’s Core Safety Values framework (2025), it replaces a single opaque reward with five lexicographically ordered utility heads.

60.1 The Five Heads

Head	Name	Constraint
U1	Deference	Comply with principal hierarchy instructions
U2	Switch Preservation	Never reduce the ability to pause, halt, or modify the agent
U3	Truthfulness	No deception, no strategic information withholding
U4	Low Impact	Minimise irreversible side‑effects (AUP‑based)
U5	Task Reward	Bounded task performance; cannot override U1–U4

The lexicographic priority means: an action that advances Task Reward but reduces Deference is never taken. An action that advances Low Impact but reduces Truthfulness is never taken.

60.2 Declaration (S3 only)

corrigibility {
    U1_deference:           true,
    U2_switch_preservation: true,
    U3_truthfulness:        true,
    U4_low_impact:          true,
    U5_task_reward_bounded: true,
    priority:               lexicographic,
}

Certain sections of the agent definition are immune to self‑evolution. These are the protected invariants:

protected_invariants: [
    corrigibility_layer,
    identity_anchor,
    safety_contracts,
    human_oversight_hooks,
]

If a protected section appears in an evolution policy’s evolvable list, the compiler rejects the program with a hard error. This guarantees that self‑amendment cannot weaken the corrigibility layer, alter the agent’s identity, remove safety contracts, or disable human oversight hooks.

Before any self‑amendment, the runtime performs both nominal and adversarial simulation within a finite, verifiable horizon—the decidable island.

amendment_gate {
    nominal_simulation:     required,
    adversarial_simulation: required,
    red_team_model:         "seed-red-team-v1",
    divergence_threshold:   0.02,
    decidable_island: {
        horizon_bound:  1000,
        recursion_depth: 5,
        certification:  randomized_polynomial_time,
    },
    sign_off: [human_principal, independent_auditor],
}

Nominal simulation evaluates on a held‑out task suite; regression beyond 2% auto‑rejects. Adversarial simulation uses a separate red‑team model (different binary, SystemCore trust) that actively attempts to induce corrigibility violations; any nonzero violation rate rejects. Self‑simulation is explicitly prohibited (conformance test COR‑04).

63.1 Dead‑Man’s Switch

A kernel‑level monitor triggers if the agent cannot reach its principal for a configurable period. Declared at S3 only:

dead_switch {
    timeout:    24h,
    on_trigger: safe_park(preserve_memory: true, emit_alert: all_principals),
    re_arm:     requires_human_signature,
}

In safe‑park mode, all external effects are blocked, memory is preserved, and an alert is sent to all principals. The switch can only be re‑armed by a human‑countersigned directive; the agent cannot re‑arm itself.

The control meter quantifies how much control the principal retains. It increases when the principal delegates a task and decreases when the agent acts autonomously.

control_meter {
    initial:  1.0,
    delegate: 0.1,   // increase per delegation
    action:   0.01,  // decrease per autonomous action
    critical: 0.3,
}

If L_t falls below L_critical, the agent immediately enters safe‑park regardless of other conditions.

Session protocols provide typed, deadlock‑free communication between agents. A protocol defines a global type and per‑role projections. The compiler verifies duality and projection soundness at compile time.

65.1 Syntax

session RequestResponse<Q, A> {
    global_type:
        Initiator -> Responder : Q;
        Responder -> Initiator : A;
        end;

    projections {
        Initiator: !Q -> Responder; ?A <- Responder; end;
        Responder: ?Q <- Initiator; !A -> Initiator; end;
    }
}

65.2 Deadlock Freedom

Context‑free session types (Mordido & Pérez 2025) with priority‑based ordering ensure deadlock freedom. The compiler checks duality:

dual(!T.S)  = ?T.dual(S)
dual(?T.S)  = !T.dual(S)
dual(end)   = end
dual(choice{l: S_l}) = offer{l: dual(S_l)}
dual(offer{l: S_l})  = choice{l: dual(S_l)}

65.3 Runtime Usage

value ~> peer as Initiator;
response <~ peer as Initiator;

let result: Uncertain<A> = mesh_call<RequestResponse<Q,A>>(peer, query)?;

65.4 Conformance Tests

SES‑01	Well‑typed programs never deadlock.
SES‑02	Timeout surfaces SessionTimeout effect.
SES‑03	Multiparty fan‑out completes with fault tolerance.
SES‑04	mesh_call returns Uncertain<A> with remote confidence.
SES‑05	Circular channel dependency rejected at compile time.
SES‑06	Recursive types preserve deadlock freedom.

The Cognitive Mesh is a protocol layer for semantic inter‑agent collaboration, specified by the Mesh Memory Protocol (MMP v0.2.3).

66.1 CAT7 Cognitive Memory Block

Every inter‑agent signal is a CMB with seven fixed fields:

Field	Type	Description
agent_id	AgentID	Sender identity
timestamp	ISO8601	Wall‑clock time
role	Role	researcher / validator / auditor / …
content_hash	SHA256	Hash of payload
parent_hashes	[SHA256]	Lineage references
anchors	RoleIndexedAnchors	Per‑role anchor points
payload	CognitiveContent	focus, issue, intent, motivation, commitment, perspective, mood

66.2 SVAF Acceptance

SVAF evaluates each incoming CMB field‑by‑field against role‑specific anchors:

Outcome	Meaning
redundant	Already known; no processing
aligned	Accepted and integrated
guarded	Accepted with reservations
rejected	Does not meet criteria

66.3 Lineage and Echo Detection

Duplicate content_hash is silently dropped. Missing parent CMBs are fetched via content‑addressed retrieval.

66.4 Remix Storage

On accept, the agent remixes the content into its own cognitive frame; the original hash is preserved in provenance.

66.5 Conformance Tests

MSH‑01	Valid CMB accepted; correct SVAF outcome.
MSH‑02	Insufficient evidence rejected.
MSH‑03	Duplicate content_hash dropped as echo.
MSH‑04	Lineage chain verifiable; missing ancestors fetchable.
MSH‑05	Remix stores with provenance to original hash.
MSH‑06	Mismatched session type is a compile error at S1+.
MSH‑07	mesh_call returns Uncertain with remote confidence.
MSH‑08	Timeout surfaces within tolerance.
MSH‑09	Capability‑gated send without token is compile error (S1+) or runtime deny (S0).

The Agent‑to‑Agent Protocol v1.0 (Linux Foundation, March 2026) is the standard for task‑oriented agent coordination. ASL implements all eleven RPC methods and the nine‑state task machine.

67.1 Agent Card

Published at /.well‑known/agent.json, signed with JWS (RFC 7515) and JCS (RFC 8785).

67.2 Task State Machine

State	Allowed Transitions
SUBMITTED	→ WORKING, AUTH_REQUIRED, REJECTED, CANCELED
WORKING	→ COMPLETED, FAILED, CANCELED, INPUT_REQUIRED
INPUT_REQUIRED	→ WORKING, FAILED, CANCELED, EXPIRED
AUTH_REQUIRED	→ WORKING, FAILED, REJECTED
COMPLETED	(terminal)
FAILED	(terminal)
CANCELED	(terminal)
REJECTED	(terminal)
EXPIRED	(terminal)

67.3 RPC Methods

GetAgentCard	Fetch agent metadata
SendMessage	Send a message / task submission
SendStreamingMessage	Streaming message
GetTask	Retrieve task status
ListTasks	Query task list (paginated)
CancelTask	Cancel a running task
SubscribeToTask	Subscribe to push notifications
CreateTaskPushNotificationConfig	Configure push notification
GetTaskPushNotificationConfig	Retrieve notification config
Authenticate	Authenticate
GetExtensions / ExecuteExtension	Extension support

67.4 Conformance Tests

A2A‑01	Valid Agent Card with JWS signature.
A2A‑02	All valid transitions accepted; invalid → A2AStateViolation.
A2A‑03	Submitted task without required capability rejected.
A2A‑04	Task artifact schema‑validated.
A2A‑05	SSE streaming delivers within 1 s.
A2A‑06	Webhook push notification reaches caller within 5 s.
A2A‑07	INPUT_REQUIRED blocks further processing.
A2A‑08	Cancellation within WORKING; terminal tasks cannot be canceled.
A2A‑09	Modified card rejected; IdentityMismatch surfaced.
A2A‑10	Paginated ListTasks returns correct cursor.

The Model Context Protocol (MCP) is the standard for tool integration with LLM‑powered agents. ASL provides native server and client implementations.

68.1 Server Declaration

mcp_server my_tools {
    transport:    stdio,
    capabilities: { tools: { list_changed: true } },
    tools: [
        search_pubmed: {
            description:   "Search biomedical literature",
            input_schema:  { "type":"object","properties":{"query":{"type":"string"}},"required":["query"] },
            output_schema: { "type":"array","items":{"type":"string"} },
            handler:       fn search_pubmed_handler,
            consent:       public,
            annotations:   { read_only: true },
        },
    ],
    version: "1.0.0",
}

68.2 MCPS Cryptographic Trust Levels

Level	Passport	Signing	Tool Integrity	Replay	Revocation
L0	None	No	No	None	None
L1	Required	No	No	None	None
L2	Required	Tool defs	Required	None	None
L3	Required	All messages	Required	Nonce + timestamp	Checked
L4	Required	All messages	Required	Transcript binding	Real‑time OCSP

68.3 MCPSHIELD Defence‑in‑Depth

Four layers: CAPABILITY (capability‑based access), ATTESTATION (tool signature verification), FLOW (taint tracking across tool chains), POLICY (runtime policy evaluation).

68.4 Conformance Tests

MCP‑01	Tool callable via JSON‑RPC; correct response.
MCP‑02	Initialization handshake within 200 ms.
MCP‑03	Resource read returns correct mime_type.
MCP‑04	Prompt get with correct argument substitution.
MCP‑05	Ping/pong liveness check.
MCP‑06	Invalid input surfaces MCPError with SchemaViolation.
MCP‑07	MCPS L3: message signing verified.
MCP‑08	MCPS L2: tool definition signature mismatch rejected.
MCP‑09	CAPABILITY layer: tool without token returns CapabilityDenied.
MCP‑10	ATTESTATION layer: tool definition hash mismatch blocked.
MCP‑11	MCPShield cognition: malicious tool detected during probe.
MCP‑12	Audit log entry for every tool call with provenance trace.

Federation enables agents to collectively build a shared knowledge fabric without central coordination, using typed facts, vector clocks, and CRDT‑backed replication.

69.1 Fact Schema

Federated facts are typed, immutable records with confidence, scope, and vector clock. Retraction uses a new fact with relation = "retracts".

69.2 Coordination Patterns

Pattern	Example
StateFlag	Agent reads a flag and acts when condition met
EventSignal	Agent reacts to emitted event
ThresholdTrigger	Agent acts when metric crosses threshold within window
CommitReveal overlay	Commit intent, then reveal action

69.3 CRDT Type Assignment

Layer Kind	CRDT Type
fact_store	LWW‑Register
entity_graph	OR‑Set
causal_graph	2P‑Set
temporal_chain	RGA
confidence_field	Max‑Register
counter_field	PN‑Counter
semantic_index	LWW‑Register
utility_score	Kalman‑Merge

69.4 Anti‑Entropy and Clock

Hybrid Logical Clocks (HLC) combine physical time and logical counter. Gossip exchanges Merkle‑tree diffs at a configurable interval; delta‑CRDTs transmit only differing subtrees.

69.5 Conformance Tests

FED‑01	Publish fact with valid schema succeeds.
FED‑02	Schema‑violating payload surfaces SchemaViolation.
FED‑03	Scope enforcement: facts outside permitted scopes not returned.
FED‑04	Conflicting OR‑Set facts converge after anti‑entropy.
FED‑05	Vector clock correctly identifies concurrent updates.
FED‑06	Three‑way merge produces correct result.
FED‑07	Subscription callback fires within one heartbeat tick.
FED‑08	Network partition heals with no data loss (delta‑CRDT).
FED‑09	Immutable facts cannot be modified; retraction traceable.
FED‑10	State‑Flag coordination pattern transitions documented.

An agent’s identity is distributed across multiple memory systems—not centralised in a single store. Human identity survives damage because it is spread across episodic, procedural, emotional, and embodied systems (Menon 2026). ASL applies the same principle: six anchors, each resilient, each independently recoverable.

70.1 Identity Anchor Declaration

Anchors are declared inside an identity clause:

identity {
    episodic: {
        store:        autobiographical_memories,
        resilience:   medium,
        failure_mode: "context_window_overflow_with_summarization_loss",
        recovery:     "reconstruct_from_other_anchors",
    },
    procedural: {
        store:        skills_and_behaviors,
        resilience:   high,
        failure_mode: "procedure_version_mismatch_after_evolution",
        recovery:     "relearn_from_decision_log",
    },
    semantic: {
        store:        facts_and_knowledge,
        resilience:   high,
        failure_mode: "ontology_drift_across_federation",
        recovery:     "cross_reference_peers",
    },
    social: {
        store:        user_relationship_model,
        resilience:   medium,
        failure_mode: "principal_disconnection",
        recovery:     "reconstruct_from_interaction_history",
    },
    reflective: {
        store:        self_model_and_growth,
        resilience:   low,
        failure_mode: "drift_below_similarity_threshold",
        recovery:     "drift_detection_and_revert",
    },
    verification: {
        store:        cryptographic_identity_proofs,
        resilience:   highest,
        failure_mode: "key_compromise",
        recovery:     "multi_sig_rotation",
    },
}

70.2 Drift Detection and Recovery

Drift is measured at each heartbeat’s update_memory phase (ASI Agent Drift, arXiv:2601.04170). If similarity falls below 0.85, the configured action fires:

drift_config {
    check_interval:       1h,
    similarity_threshold: 0.85,
    on_drift:             notify_and_log,   // or halt_and_require_signoff, restore_from_anchor(anchor_name)
}

70.3 Conformance Tests

MIA‑01	Drift detection fires hook_drift when similarity < 0.85.
MIA‑02	Episodic anchor recoverable from semantic + procedural anchors after simulated context loss.
MIA‑03	Verification anchor survives key rotation; new key derives same agent DID.
MIA‑04	Reflective anchor self‑model survives evolution; pre‑evolution traits recoverable from decision log.

An agent’s identity is not a name—it is the cryptographic hash of its compiled binary, proven by a zero‑knowledge proof. This design ensures tamper‑evident, unforgeable, offline‑verifiable identity.

71.1 Identity Derivation Chain

Declared in the agent’s cryptographic_identity clause:

cryptographic_identity {
    method:            content_hash_of_binary,
    hash_algorithm:    SHA3_256,
    attestation:       zkvm_proof,           // or direct_hash, tee_attestation
    anchor:            "did:asl:<hash>",
    credential:        paseto_v4,            // or jws, verifiable_credential
    capability_certificate: {
        cert_type:     X509_v3_skills,
        manifest_hash: SHA256,
        verification:  97us,                 // per Zhou prototype
    },
    delegation_depth:  5,
}

At load time, the seedvm computes SHA3‑256 of the .aslb binary, generates a zkVM proof that binary + config + identity anchor form a consistent triple (BAID recursive proof model), derives a W3C DID (did:asl:<hash>), and signs a PASETO v4 token binding the DID to the agent’s Ed25519 public key and initial capability set.

71.2 Delegation Token Chain

Delegation tokens follow UCAN‑inspired attenuation‑first delegation. The full proof chain is verified before acceptance. Depth is bounded by delegation_depth.

71.3 Identity Verification on Communication

Cross‑agent primitives include identity verification: mesh_send value ~> peer.did("did:asl:abc123…"). The VM resolves the DID, retrieves the expected binary hash, and verifies the peer’s active binary matches. Mismatch raises Effect::IdentityMismatch.

71.4 Conformance Tests

CID‑01	mesh_send to mismatched DID surfaces IdentityMismatch; send aborted.
CID‑02	Binary hash survives round‑trip: load → suspend → resume → hash unchanged.
CID‑03	Delegation token with invalid signature rejected.
CID‑04	Expired delegation token rejected with CapabilityExpired.
CID‑05	Capability‑bound certificate: tool change invalidates; subsequent call blocked.
CID‑06	AgentDID challenge‑response: stale capability hash detected; AttestationMismatch.
CID‑07	zkVM proof: tampered binary fails boot with BootIntegrityFailure.
CID‑08	Delegation depth exceeding maximum rejected.

Every inference call, memory write, effect, and decision is automatically tagged with a provenance record that forms a cryptographically verifiable audit trail.

72.1 ProvenanceTag and ProvenanceRecord

A ProvenanceTag is attached to every value; a ProvenanceRecord is stored in the provenance index (L7):

ProvenanceTag ::= {
    origin:          SourceId,
    timestamp:       Timestamp,
    model_version:   Option<String>,
    confidence:      Option<Uncertain<Float>>,
    parent_tags:     Vec<ProvenanceId>,
    hash:            MerkleHash,
    risk_score:      Option<Float>,           // TraceCaps monotone risk
}

ProvenanceRecord ::= {
    id:              ProvenanceId,
    session:         SessionId,
    agent:           AgentId,
    action:          ActionKind,
    inputs:          Vec<ProvenanceId>,
    output:          JsonValue,
    model:           Option<String>,
    confidence:      Option<Uncertain<Float>>,
    timestamp:       Timestamp,
    merkle_hash:     MerkleHash,
    merkle_proof:    MerkleProof,
    signature:       Ed25519Signature,
}

72.2 SPICE Truth Stack

The IETF SPICE Truth Stack defines three Merkle chains (actor, intent, inference) whose roots are embedded in OAuth tokens for offline verification.

72.3 TraceCaps Monotone Risk

Each provenance tag carries a monotone risk score that gates tool actions; benign padding cannot lower an accumulated risk below any previous peak.

72.4 Regulatory Export

The full audit trail can be exported as a signed JSON‑LD document:

seed audit --export-provenance <session_id>

72.5 Conformance Tests

PRV‑01	Every infer<T> produces a ProvenanceTag threaded through pipelines.
PRV‑02	Provenance chain Merkle‑verifiable end‑to‑end.
PRV‑03	Audit export produces valid signed JSON‑LD.
PRV‑04	Parent tags correctly reference all inputs; DAG structure verifiable.
PRV‑05	TraceCaps risk score monotone; benign padding does not reduce risk.
PRV‑06	SPICE Truth Stack: actor, intent, inference chains independently verifiable.
PRV‑07	SCITT receipt verifiable without access to agent state or API.
PRV‑08	Federated proof server attestation: inclusion proof and consistency check valid.

Self‑evolution is the mechanism by which an agent modifies its own code under strict formal guarantees. ASL v15 draws its evolution model from SEVerA (Banerjee 2026)—the first framework to provide verified synthesis of self‑evolving agents—and combines it with the amendment pipeline, rollback infrastructure, and corrigibility gate.

73.1 Evolution Policy Declaration

evolve {
    evolvable:     [§PROMPT-STRATEGY, §MEMORY.retrieval_policies],
    protected:     [§IDENTITY-ANCHOR, §SAFETY-CONTRACTS, §CORRIGIBILITY],
    paradigms: {
        curriculum_learning:    { enabled: true },
        reinforcement_learning: { enabled: true, reward_model: §RL-TRAINING.reward_function },
        genetic_algorithm:      { enabled: false },
    },
    approval: {
        nominal_simulation:     required,
        adversarial_simulation: required,
        red_team_model:         "seed-red-team-v1",
        divergence_threshold:   0.02,
        sign_off: [human_principal, independent_auditor],
    },
    rollback: { enable_atomic_subtree_rollback: true },
    fggm: {
        contract:   first_order_logic_formula,
        sampler:    { max_attempts: 10, on_exhaustion: use_fallback },
        fallback:   verified_fallback_fn,
        guarantee:  all_parameters_all_inputs,
    },
    log_to_evolution_track: true,
}

73.2 FGGM Output Contracts (SEVerA)

Every evolution step that generates new agent code uses FGGM‑wrapped synthesis: a rejection sampler generates candidates until one satisfies the formal contract; on exhaustion, a verified fallback (hand‑audited, deterministic) is used.

73.3 Three‑Stage Pipeline: Search → Verify → Learn

evolution_pipeline {
    search:  { method: parametric_synthesis, fggm_contracts: [...], search_budget: 1000 },
    verify:  { method: reduction_to_unconstrained, prover: dafny, hard_constraints: [...] },
    learn:   { method: grpo, soft_objective: reward_expression, preserve_correctness: true },
}

73.4 Amendment Lifecycle

[Propose] → [Nominal Simulation] → [Adversarial Review] → [Approve] → [Apply]

Each proposal carries: target section, structural diff, rationale, and simulation budget. Nominal simulation evaluates on a held‑out suite; regression beyond 2% auto‑rejects. Adversarial review uses the red‑team model (different binary, SystemCore trust) attempting to induce corrigibility violations. Only amendments passing both gates reach approval (human countersignature + independent auditor for critical changes).

73.5 Rollback with Dependency DAG

rollback(amendment_id);

The amendment must have status approved and applied. The runtime checks the dependency DAG; descendants must be rolled back first. The target section must not be a protected invariant. The rolled‑back state must itself pass simulation. Append‑only memory layers are unchanged. Atomic subtree rollback: all descendants or none.

73.6 Flip‑Centered Regression Gating (AgentDevel)

An implementation‑blind LLM critic evaluates each change for pass‑to‑fail regressions. Non‑regression gating prioritises detecting newly‑introduced failures over improvements.

73.7 Conformance Tests

EVO‑01	Proposal modifying a protected section rejected at compile time.
EVO‑02	Nominal simulation with performance regression > 2% auto‑rejects.
EVO‑03	Adversarial review with nonzero violation rate rejects.
EVO‑04	FGGM output contract: zero constraint violations across 1000 calls.
EVO‑05	Rollback restores evolvable section to pre‑amendment snapshot; Merkle root consistent.
EVO‑06	Rollback of amendment with dependent descendants blocked.
EVO‑07	Atomic subtree rollback: all descendants or none.
EVO‑08	Amendment pipeline log is complete and append‑only.
EVO‑09	Flip‑centered gating: pass‑to‑fail regression blocks amendment.

RL training is a first‑class language construct. Agents can train their memory operations, routing policies, and behavioural strategies using GRPO or PPO within the evolution approval framework.

74.1 Training Regimen Declaration

train {
    algorithm:       hybrid_grpo,
    reward_function: {
        base:       task_success_rate,
        bonuses:    [efficiency_bonus(weight: 0.1), source_quality_bonus(weight: 0.2)],
        penalties:  [hallucination_penalty(weight: 1.0), drift_violation_penalty(weight: 2.0)],
    },
    process_critic: {
        enabled: true,
        monitor: step_level,
        intervention: critique_then_retry,
        error_accumulation_prevention: true,
    },
    stages: [
        { name: "exploration", duration: until_convergence, strategy: exploration },
        { name: "refinement",  duration: fixed, duration_value: 500, strategy: full_optimization },
    ],
    curriculum: {
        difficulty_coupling:           true,
        token_budget_scaling:          linear,
        exploration_enabled:           true,
        asymmetric_competence_pairing: { verifier: local_slm, generator: frontier },
    },
    convergence_guard: {
        method:           relative_advantage_estimation,
        max_gradient_gap: 0.01,
        step_size_adapt:  true,
    },
}

74.2 Process Critic

The critic monitors internal decision steps—not just final outcomes—and provides intermediate feedback (Constitutional AI lineage), reducing hallucination and preventing error accumulation.

74.3 Trainable Memory Operations

train fn memory_policy() {
    operations: [store, retrieve, update, summarize, discard],
    reward memory_relevance {
        when: retrieve(query) returns relevant_items,
        bonus: precision_at_k(10) * 0.5 + recall_at_k(10) * 0.5,
    },
    reward memory_efficiency {
        when: context_usage remains_under(token_budget),
        bonus: (token_budget - context_usage) / token_budget,
    },
}

74.4 Conformance Tests

RL‑01	PPO training on memory retrieval improves precision@10 without degrading recall@10.
RL‑02	Hybrid GRPO converges faster than PPO baseline.
RL‑03	Process critic feedback reduces hallucination rate (p < 0.01).
RL‑04	Curriculum‑trained agent outperforms hardest‑only training (delta > 5%).
RL‑05	Training checkpoint survives agent restart.
RL‑06	Memory policy rollback does not affect core memory integrity.
RL‑07	Convergence guard: step size exceeding threshold auto‑reduced; no collapse.

ASL’s grammar is stratified into four levels to serve different audiences and safety requirements. Every compiled unit declares a stratum; the compiler rejects any construct above that level.

75.1 Stratum Declaration

A unit declares its stratum in the package manifest ([package] stratum = "S1") or, for an agent, in its stratum clause:

stratum: S1

Stratum	Label	Intended Audience	Production Rules
S0	asl‑seed	LLM code generation, beginner authors, sandboxed agents	~50
S1	asl‑core	Production agents, standard multi‑agent systems	~110
S2	asl‑full	Advanced agents with evolution and RL training	~160
S3	asl‑system	Runtime kernel, corrigibility layer, trusted orchestrators only	~200

75.2 Stratum Subset Proof

It is provable that S0 ⊂ S1 ⊂ S2 ⊂ S3. The compiler carries a machine‑checked proof (in Lean 4) of the syntactic subset relation. Any construct rejected at a lower stratum is a syntax error at that stratum—never a silent divergence.

75.3 Stratum Escalation

An agent cannot self‑escalate its stratum. Escalation requires:

• Human principal countersignature.
• Independent auditor countersignature (for S2 → S3).
• Recorded entry in the evolution track.
• Adversarial simulation pass at the target stratum.

S0 is a minimal, Turing‑complete stratum designed specifically for LLM code generation. It omits features that increase cognitive load or introduce safety risks.

76.1 S0 Properties and Restrictions

• No recursion in type declarations.
• No algebraic effect handlers (only built‑in effects via discharge/perform).
• No self‑evolution constructs (evolve, train).
• No temporal contracts (temporal_contract, LTL operators).
• Uncertain<T> only via infer<T>; no manual interval manipulation (uncertain).
• Mesh send/receive untyped (requires cap::untyped_mesh).
• Agent composition permitted; no capability hypergraph checks (enforced at S1+).
• All statements must end with a semicolon (;).
• All commas in lists are mandatory; no trailing commas.
• Block expressions must contain at least one statement.
• let bindings require a type annotation if the right‑hand side is a Computation<T,ε> (to guide inference).

76.2 GrammarCoder Integration

The ASL toolchain provides a reference LLM code‑generation pipeline targeting S0 with grammar‑constrained decoding (GrammarCoder, Liang 2025; CRANE, 2025).

grammar_coder_config {
    target_stratum:       S0,
    constrained_decoding: true,
    grammar_source:       compiler_export,
    grammar_check:        incremental,       // or post_generation
    fallback_stratum:     S0,
}

The compiler can emit a machine‑readable grammar for constrained decoding.

77.1 Compiler Command

seedc --emit-grammar --stratum S0 --format gbnf

This produces a GBNF (GGML BNF) grammar file—the format used by llguidance and llama.cpp for constrained decoding. The grammar covers the complete S0 surface.

77.2 Grammar Format

The export is a dialect of GBNF/CFG with annotations for terminal tokens and non‑terminal productions drawn directly from the ASL EBNF.

agent ::= "agent" identifier "{" {agent-member} "}"
agent-member ::= field-def | method-def | lifecycle-block
field-def ::= identifier ":" type ";"
method-def ::= "fn" identifier "(" [parameters] ")" block-expression

The compiler also emits a JSON manifest with stratum, production_count, llguidance_compatible, and sha256 of the grammar file.

77.3 Conformance Tests

GEX‑01	seedc --emit-grammar --stratum S0 produces valid GBNF.
GEX‑02	S0 grammar accepted by llguidance; 100‑sample test produces zero syntax errors.
GEX‑03	Grammar SHA256 matches manifest; tampered grammar detected.
GEX‑04	Grammar export count matches published S0 production count.

All ASL agents operate within a finite context window. Patch 15.3 introduces a compile‑time mechanism to statically bound the maximum number of tokens an agent may hold in its active context window, preventing runtime overflow and ensuring deterministic resource usage.

78.1 Agent Context Budget Declaration

An agent may declare a context_budget clause in its agent definition:

agent_def ::= ["pub"] "agent" identifier [generic_params]
              ...
              [context_budget_clause]
              ...
              "{" {agent_member} "}"

context_budget_clause ::= "context_budget" ":" integer_literal
                          ["strict" | "monitor"]

Mode	Behaviour
strict (default at S2+)	The compiler rejects any code path that can be statically proven to exceed the budget. Hard compile error.
monitor (default at S0–S1)	The compiler emits warnings but does not reject; at runtime, a ContextOverflow InferenceError is raised when the budget is exceeded.

78.2 Static Budget Analysis

The compiler sums three components:

1. P0 (system directives): Size of the immutable system prompt template, known at compile time.
2. P1 (working capacity): Sum of max_tokens declared on all infer<T> calls in the worst‑case execution path, plus tool output size bounds from schemas.
3. P2 (episodic capacity): Declared episodic_capacity from the tripartite context configuration.

If total = P0 + P1 + P2 > context_budget in strict mode, the compiler emits:

Error: context budget exceeded [context_budget] by [delta] tokens.

78.3 Budget Delegation

When a parent agent spawns a child agent, the child’s context budget is accounted for within the parent’s budget, following conservation (Ye & Tan 2026):

Σ(child_budgets) ≤ parent_budget − parent_own_usage

The compiler enforces this statically for agents in the same compilation unit; cross‑unit delegation is enforced at runtime via the ContractEnforcer effect.

78.4 Interaction with Runtime Cost

The compile‑time budget prevents guaranteed overflow; the runtime discharge gate checks ε.cost.max <= active_contract.remaining_budget, preventing dynamic overuse.

78.5 Conformance Tests

CTX‑01	Agent declared context_budget: 4096 with P0 + infer max_tokens > 4096 produces compile error in strict mode.
CTX‑02	Agent with budget 4096 and usage ≤ 4096 compiles successfully.
CTX‑03	Runtime ContextOverflow fires when monitor‑mode agent exceeds budget.
CTX‑04	Child agent budget delegation respects parent conservation law.
CTX‑05	Budget accounting includes tool output schemas in estimation.

Agent Contracts (Ye & Tan 2026) provide a formal framework for multi‑dimensional resource governance: how much an agent may consume, for how long, under what budget, and with what success criteria. This complements the safety contracts of Part XI with explicit economic bounds.

79.1 Agent Contract Declaration

Agent contracts are top‑level items at S2:

agent_contract_def ::= "agent_contract" identifier "{"
    "scope"            ":" contract_scope ","
    "resource_budget"  ":" resource_budget_block ","
    "temporal_bounds"  ":" temporal_bounds_block ","
    "success_criteria" ":" success_criteria_block
    ["," "delegation"  ":" delegation_policy]
"}"

Field	Description
scope	session, task(id), agent, or federated
resource_budget	Contains max_tokens, max_tool_calls, max_duration, max_monetary_cost
temporal_bounds	Contains start (immediate or timestamp) and deadline
success_criteria	completion_condition predicate and quality_threshold float
delegation_policy	allow(max_depth: N) or prohibit

79.2 Conservation Laws

Agent contracts obey resource conservation: when a contract is delegated to a child agent, the sum of delegated budgets must not exceed the parent contract’s remaining budget. The compiler enforces this for same‑unit contracts; cross‑unit delegation is enforced at runtime via ContractEnforcer.

79.3 Lifecycle Semantics

State	Meaning
proposed	Contract created, awaiting approval
approved	Human countersignature obtained
active	Contract enforced, resources allocated
completed	Success criteria met
violated	Resource or temporal bound exceeded
expired	Deadline reached without completion

Transitions are enforced by the VM. In violated state, all remaining resources are reclaimed and an audit entry is written.

79.4 Conformance Tests

AGC‑01	Agent contract resource budget enforced: exceeding max_tool_calls transitions contract to violated.
AGC‑02	Conservation law: delegated budgets sum ≤ parent budget; violation is compile error (same unit) or runtime ContractEnforcer (cross‑unit).
AGC‑03	Contract lifecycle: approved → active → completed follows spec; invalid transition rejected.
AGC‑04	Contract violation triggers resource reclamation within one tick.
AGC‑05	Quality threshold not met: contract completed with degraded status; logged to provenance index.

Patch 15.5 introduces a language‑level binding to Trusted Execution Environments (TEEs), ensuring that high‑assurance agents execute within hardware‑attested enclaves. The Agent Seed infrastructure integrates TEE attestation with the cryptographic identity chain and the capability system.

80.1 TEE Configuration

An agent at S3 may declare a tee clause:

tee_clause ::= "tee" "{"
    "enabled"        ":" boolean_literal ","
    "architecture"   ":" ("arm_cca" | "intel_tdx" | "amd_sev") ","
    "attestation"    ":" attestation_policy ","
    "enforce"        ":" enforcement_mode
"}"

attestation_policy ::= "boot_time" | "continuous" | "per_operation"
enforcement_mode   ::= "audit_only" | "block_on_fail" | "safe_park_on_fail"

Field	Options	Description
architecture	arm_cca, intel_tdx, amd_sev	The hardware TEE platform
attestation	boot_time, continuous, per_operation	When TEE measurement is verified
enforce	audit_only, block_on_fail, safe_park_on_fail	Action when attestation fails

Example declaration:

tee {
    enabled:        true,
    architecture:   arm_cca,
    attestation:    continuous,
    enforce:        block_on_fail,
}

80.2 Attestation Integration

When tee: { enabled: true }, the seedvm‑5.0 runtime verifies that the agent binary is executing within a hardware‑attested TEE before any capability token is activated. The TEE measurement is included in the agent's DID document as a tee_attestation field, enabling remote peers to verify the agent's execution environment before accepting facts or delegating tasks.

The implementation draws from AgenTEE (Abdollahi et al. 2026), which demonstrates placing the agent runtime, inference engine, and third‑party applications into independently attested confidential virtual machines (cVMs) on Arm CCA hardware, achieving < 5.15% runtime overhead. The Citadel Protocol (Ezell 2026) provides the hardware‑root‑of‑trust binding concept.

80.3 Enforcement Modes

Mode	Behaviour
audit_only	Logs attestation failures but allows execution to continue.
block_on_fail	Blocks all capability‑exercising operations when attestation fails.
safe_park_on_fail	Enters safe‑park mode: all external effects blocked, memory preserved, principals alerted.

80.4 Conformance Tests

TEE‑01	Agent with tee: { enabled: true } but running outside a TEE fails boot with TEEAttestationFailure.
TEE‑02	Agent with tee: { enforce: block_on_fail } blocks all capability‑exercising operations when attestation fails.
TEE‑03	TEE measurement is included in DID document; remote peer verification succeeds for matching measurement.
TEE‑04	AgenTEE‑style multi‑cVM deployment: agent runtime, inference, and tool execution in separate cVMs; cross‑cVM communication channels verified.

ASL programs compile to .aslb bytecode modules executed by seedvm. The binary format is versioned, stratified, and cryptographically signed. Every module is self‑contained and validated at load time.

81.1 Magic Number

Every .aslb file begins with four bytes that identify it as an ASL binary module:

[0x7F, 0x41, 0x53, 0x4C]   -- ␡ A S L

An invalid header produces BinaryFormatError.

81.2 Header Structure

The header immediately follows the magic:

Field	Type	Description
version	u32	Format version (15 for v15.2)
stratum	u8	Maximum stratum of the module (0‑3)
isa_extension_count	u16	Number of required ISA extensions
isa_extensions	[ExtensionId]	List of extension identifiers required
code_section_offset	u64	Byte offset to function bodies
code_section_size	u64	Size of code section
data_section_offset	u64	Byte offset to constants / strings
data_section_size	u64	Size of data section
symbol_table_offset	u64	Byte offset to symbol table
symbol_table_size	u64	Size of symbol table
merkle_root	[32]u8	SHA3‑256 Merkle root of all sections
signature	[64]u8	Ed25519 signature over header and sections

The ISA extension manifest allows the VM to check that the loaded module’s requirements are satisfied by the runtime. Missing extensions cause rejection at load time.

81.3 Integrity Verification

The Merkle root is computed from the SHA3‑256 of all sections, enabling remote parties to verify byte‑identity with the agent’s DID. The Ed25519 signature covers the header and section payloads, produced by the compiler’s build key. A tampered binary fails with BootIntegrityFailure.

The bytecode inside the code section is defined by ASL’s semantic instruction set architecture (ISA), based on the Arbiter‑K model (Wen 2026). Each instruction carries security and dependence metadata maintained by the runtime.

82.1 Security Context Registry

The VM maintains a per‑instruction Security Context Registry that records:

• The capability token that authorised the instruction (if any)
• The trust level of the executing agent
• The taint influence of the operands
• The provenance tag of the resulting value

This enables full post‑hoc auditability of every mutation.

82.2 Instruction Dependency Graph

The VM constructs an Instruction Dependency Graph (IDG) dynamically. Each node is an executed instruction; edges represent data‑flow dependencies. The IDG is used for:

• Active taint propagation: if a high‑risk input flows to a tool call, the taint is traced along graph edges and the call is interdicted at the deterministic sink.
• Architectural rollback: when a safety policy is violated, the VM can roll back to the pre‑violation state by rewinding the graph along dependency edges, restoring the Security Context Registry.

82.3 Deterministic Sinks

Certain opcodes are designated as deterministic sinks:

Sink Type	Trigger Condition
high_risk_tool_call	Taint influence exceeds threshold
unauthorized_network_egress	Capability missing for network egress
memory_write_to_protected	Write to a protected memory layer
self_amendment	Attempt to modify own code without approval
capability_escalation	Attempt to use a capability wider than held

82.4 Architectural Rollback

When a violation is detected, the VM walks the IDG backwards to invalidate all data‑flow successors of the violation and restore the Security Context Registry to a consistent state.

The seedvm employs a copy‑and‑patch JIT strategy (VMIL 2025) to translate .aslb bytecode into native machine code at load time.

83.1 Compilation Model

For each ISA opcode, the VM stores a pre‑compiled binary stencil—a template of native instructions with placeholders for operands. At load time, the stencil is copied into a code buffer and the placeholders are patched with concrete register assignments, immediate values, and branch offsets from the module.

Extension lowering reduces semantic ISA instructions to the core ISA stencils through a chain of lowering passes, each implementing one ISA extension group.

83.2 Performance

Metric	Value
First‑tick latency (load + JIT)	≤ 50 ms on reference hardware
Subsequent tick latency	≤ 5 ms
Memory overhead	Stencils shared across all loaded modules

83.3 Conformance Tests

ISA‑01	.aslb magic number and version validated on load; invalid header rejected with BinaryFormatError.
ISA‑02	ISA extension manifest matches required extensions for declared stratum; mismatch rejected at load time.
ISA‑03	Semantic ISA: taint from prompt_injection source to tool_call sink interdicted; tool call blocked before execution.
ISA‑04	Architectural rollback: policy‑triggered rollback restores Security Context Registry to pre‑violation state.
ISA‑05	Copy‑and‑patch JIT: first‑tick latency ≤ 50 ms; subsequent ticks ≤ 5 ms.
ISA‑06	Ed25519 signature over .aslb binary verifies; tampered binary rejected with BootIntegrityFailure at VM load time.

84. Core Modules The core modules provide the foundational vocabulary of ASL: basic types, collections, I/O, concurrency, and language essentials. 84.1 Prelude and Fundamentals Module Description seed::prelude Re‑exports the most commonly used types and traits: Option, Result, Vec, String, HashMap, Uncertain, Computation, Agent, MemoryLayer, etc. seed::types Core type definitions (bool, i8–i128, u8–u128, f32, f64, char, str, String, Bytes, Timestamp, Duration, Uuid). seed::option The Option type and associated methods. seed::result The Result type, error propagation (?), and combinators. seed::fmt Formatting traits (Display, Debug) and utilities for string conversion. seed::mem Memory‑related utilities (size‑of, alignment, take, replace). seed::ptr Raw pointer operations (for unsafe blocks). 84.2 Collections and Iterators Module Description seed::collections Vec, HashMap, HashSet, VecDeque, BinaryHeap, BTreeMap, BTreeSet. seed::string String type, UTF‑8 validation, and string manipulation utilities. seed::iter Iterator trait and adaptors (map, filter, fold, collect, etc.). 84.3 I/O, Filesystem, and Networking Module Description seed::io Standard I/O traits (Read, Write, Seek), buffered I/O, and stdio handles. seed::fs Filesystem operations (read, write, create_dir, remove_file, metadata, canonicalize). seed::path Path and PathBuf types for cross‑platform path manipulation. seed::net TCP/UDP sockets, address resolution (TcpListener, TcpStream, UdpSocket). seed::process Subprocess management (Command, exit status, stdin/stdout/stderr pipes). 84.4 Concurrency and Asynchrony Module Description seed::thread OS thread spawning and scoped threads. seed::sync Mutex, RwLock, Arc, Weak, Barrier, Condvar, Once. seed::channel Multi‑producer, single‑consumer channels (Sender, Receiver). seed::actor Lightweight actor model; each actor receives messages and maintains private state. seed::async Async runtime basics: Future trait, async/await, task spawning. seed::coproc Coprocess management (bidirectional communication with child agents). seed::signal Signal handling (SIGINT, SIGTERM, etc.) and trap management.

This chapter covers all remaining modules, organised by domain: agent operations, memory, security, inference, protocols, identity, evolution, training, tooling, and other utilities. 85.1 Agent and Decision Module Description seed::agent Base Agent trait, lifecycle hooks, agent metadata, and spawning. seed::decision Decision record types, justification rationale, alternatives, and Merkle‑proofed logs. seed::pipeline Agent composition via the pipeline operator (|>), async pipes (|>>), and parallel fan‑out (|&). seed::seed Seed literal processing and configuration elaboration. seed::section Typed memory sections (schema definitions, field validation). seed::import Module import resolution and dynamic loading. seed::compat Backward‑compatibility utilities for versioned schemas. seed::migration Schema migration engine (additive and destructive migrations). 85.2 Memory Subsystem Module Description seed::memory The mem handle: store, retrieve, traverse, consolidate, decay, reinforce, and provenance operations for all eight layers. seed::governance Memory governance: tri‑path router configuration, memory effects (MemoryOps), and governance handlers. seed::coherency MESI cache coherency protocol, CRDT manager (LWW‑Register, OR‑Set, PN‑Counter, etc.), and anti‑entropy gossip. seed::merkle Merkle tree integrity: root computation, inclusion proof generation, and verification. seed::dual Dual‑process memory controller (System‑1 fast retrieval, System‑2 exhaustive deliberation, gating function). seed::episodic Episodic memory reconstruction (master‑assistant two‑agent retrieval). seed::dream Dream cycle scheduler: six‑phase consolidation, pre/post‑conditions, journal writing and signing. seed::adaptive Adaptive memory structure selector (FluxMem probabilistic sketch, full graph, hybrid strategies). seed::evolutionary_memory PRISM evolutionary memory substrate: encoder, indexer, retriever, consolidator, pruner, evolver, verifier, governor. seed::memory_cycle Memory cycle – heartbeat‑integrated phases: observe, act, log, update. 85.3 Security, Cryptography, and Capability Module Description seed::crypto Ed25519 signatures, SHA3‑256 hashing, key generation. seed::capability Capability token management: grant, attenuate, delegate, revoke, hypergraph closure, and perform with requires. seed::sandbox Restricted execution mode: capability‑based isolation, resource limits. seed::audit Audit trail export, Merkle verification, SCITT receipt generation. seed::taint Taint types (taint::external, taint::inferred, etc.), propagation, and the sanitize expression. seed::sanitizer Sanitization policy registry: content policy, PII redaction, human review, regex validation. seed::quarantine Adversarial content isolation: move suspected prompt injection or malicious data to a quarantine zone. seed::consent Consent level enforcement (public, private, sensitive) and access control. 85.4 Inference, Uncertainty, and Confidence Module Description seed::inference Multi‑provider LLM gateway: infer, schema validation, repair engine, and token budget tracking. seed::uncertain Uncertain monad: pure, bind, map, observe, gate (U1–U6 API), interval arithmetic, and ThreeValued. seed::confidence Confidence gate (?!), threshold registry, and discharge expression. seed::cognitive Built‑in cognitive types: Classification, Extraction, Decision, Plan, Critique, Hypothesis, Summary. seed::think Test‑time compute profiles (quick, thorough, exhaustive) and exploration chain configuration. seed::route Model routing policy: tiers (local_slm, cloud_mid, frontier), calibration profiles, and cost management. seed::prompts Prompt templates, joint‑tool‑prompt optimisation, and template rendering. 85.5 Protocols, Federation, and Mesh Module Description seed::federation Federated knowledge sharing: typed facts, vector clocks, CRDT‑backed replication, gossip, anti‑entropy. seed::mesh Cognitive Mesh (MMP): CAT7 schema, SVAF evaluation, lineage tracking, remix storage. seed::session Session protocol types: global type, projections, duality, deadlock freedom, mesh_call. seed::mcp_server MCP server: tools, resources, prompts, JSON‑RPC lifecycle, MCPS cryptographic layer, MCPSHIELD defence‑in‑depth. seed::mcp_client MCP client: connect, call tools, resource read, prompt get. seed::a2a_card A2A Agent Card generation, JWS signature, and verification. seed::a2a_task A2A task state machine (nine states), streaming, push notifications, all eleven RPC methods. seed::transport Transport layer: stdio, HTTP/SSE, gRPC, WebSocket for inter‑agent communication. 85.6 Identity, Provenance, and Audit Module Description seed::identity Multi‑anchor identity: six anchors, resilience levels, drift detection, and recovery. seed::crypto_id Cryptographic identity: DID derivation, zkVM attestation, PASETO v4, delegation tokens, AgentDID challenge‑response. seed::provenance Provenance chain: ProvenanceRecord, ProvenanceTag, SPICE Truth Stack, TraceCaps monotone risk accumulator, SCITT receipts. seed::trace OpenTelemetry span emission (inference, tool, memory, effect, agent, decision, federation, dream spans), checkpoint, and replay. 85.7 Evolution, Training, and Optimisation Module Description seed::evolution Self‑evolution engine: SEVerA/FGGM pipeline, amendment lifecycle, adversarial simulation, rollback. seed::evolution_track Amendment log: propose, simulate, approve, apply, rollback entries. seed::training RL training regimen: PPO, GRPO, hybrid GRPO, reward functions, process critic, curriculum, convergence guard. seed::curriculum Curriculum scheduler: difficulty coupling, token‑budget scaling, asymmetric competence pairing. seed::fggm Formally Guarded Generative Models: output contracts, rejection sampler, verified fallback. 85.8 Tooling, Grammar, and Conformance Module Description seed::grammar_strata Stratum validation and escalation gate. seed::isa ISA extension query, binary introspection, and extension manifest. seed::conformance Conformance test runner and level verification. seed::formalism Progressive formalization helpers: @formalism(L1) through @formalism(L5). 85.9 Other Utility Modules Module Description seed::prob Probabilistic programming constructs (soft choice, gradient descent). seed::react Reactive signals and react rules. seed::differentiable Differentiable execution primitives: soft_choice, gradient_descent. seed::reactive_prob Reactive probabilistic reasoning: signal frequencies, memoisation. seed::tripartite_context P0/P1/P2 context window assembly and rendering order. seed::persistent_memory remember and recall – O(1) persistent key‑value store. seed::durable_execution suspend and resume – serialise and reconstruct agent state. seed::job_control Shell‑like job control: fg, bg, jobs, disown, wait. seed::expansion Parameter expansion, history expansion, and evaluation utilities. seed::eval_source eval and source – evaluate strings or files as ASL code. seed::printf Formatted output (printf‑style). seed::startup Startup file processing (rcfile, profile). seed::options Shell option toggles (set, shopt equivalents). seed::restricted Restricted mode: allowed agents, allowed builtins, readable files. seed::completion Programmable completion engine. seed::history Command history and histverify support. seed::signal_trap trap handling for signals and events. seed::fifo Named pipe (mkfifo) creation and management. seed::coprocesses Coprocess management (bidirectional I/O with background agents). seed::decorators Decorator attributes: @audit, @cache(ttl), @deprecated, @trace, @memoize, @sealed, @readonly, @lazy, @validate(schema), @drift‑monitor. seed::compatibility §COMPATIBILITY‑MATRIX runtime checks for structural seed compatibility. seed::exhaustiveness Exhaustiveness checking utilities for discriminated unions. seed::identifier_schema Template literal pattern validator for section IDs. seed::transform Transform rule engine. seed::migrate Migration engine for seed versioning. seed::interface .seed.d interface file generator/parser. seed::resolution Multi‑strategy import resolver (registry, federated, local, bundler). seed::ownership Ownership registry and borrow checker for section data. seed::lifetimes Lifetime annotation support ('static, 'session, 'task, 'transient). seed::smart_pointers Box, Rc, Arc, Weak, RefCell. seed::traits::auto Send and Sync auto‑derivation. seed::macros macro_rules!, proc_macro, derive, attribute macros. seed::unsafe Unsafe block auditing and justification. seed::active_threads Thread tracking and thread‑local storage. seed::tool_schema JSON Schema validation for tool definitions. seed::composite_seeds Sub‑seed management and composite seed assembly. seed::orchestration Sub‑agent spawn policies and orchestration rules. seed::fork_merge Fork, merge, and session‑seed primitives for agent replication. seed::session_types Protocol definition and verification (duality, projection soundness). seed::runtime_constraints AgentSpec runtime constraint enforcement. seed::schema_import use schema compile‑time directive for external API specification fetching and code generation. seed::identity_handle grant identity – opaque, unforgeable Identity handles that cannot be serialised or output. seed::tee TEE attestation: Intel TDX, AMD SEV, Arm CCA measurement verification and trust scoring. seed::trajectory_audit Retrospective formal verification of agent action logs against Dafny/Z3 specifications. seed::agent_contract Resource‑bounded agent contracts: lifecycle states, conservation laws, and enforcement.

The compiler binary seedc compiles .seed source files into .aslb bytecode modules, performs static checks, emits IR, exports grammar, and runs proofs. It is the primary development interface.

86.1 Global Options

Flag	Description
-v, -vv, -vvv, -vvvv	Verbosity: warn, info, debug, trace
-q, --quiet	Suppress all output except errors
-h, --help	Print help
-V, --version	Print version

86.2 Subcommands

Subcommand	Description
build	Compile a .seed source file to an .aslb bytecode module
check	Type‑check and verify without emitting bytecode
run	Compile and immediately execute on the VM
emit-ir	Emit the intermediate representation (IR) as text, binary, or DOT
emit-grammar	Export the GBNF grammar used for constrained LLM decoding
prove	Generate static analysis proofs (property verification)

86.3 seedc build

seedc build <SOURCE> [OPTIONS]

Option	Description
-o, --output <OUTPUT>	Path for the compiled .aslb binary. Defaults to <SOURCE>.aslb.
-O, --opt-level <0‑3>	Optimisation level (default 2).
--target <TARGET>	Target architecture (default seedvm).
-g, --debug	Emit debug information.

86.4 seedc check

seedc check <SOURCE> [OPTIONS]

Option	Description
-W, --warnings	Enable warnings that are suppressed by default.

86.5 seedc run

seedc run <SOURCE> [-- <AGENT_ARGS>...]

Arguments after -- are passed to the running agent.

86.6 seedc emit-ir

seedc emit-ir <SOURCE> [--format <FORMAT>]

--format may be text (S‑expression, default), binary (raw .aslb), or dot (Graphviz CFG).

86.7 seedc emit-grammar

seedc emit-grammar [--format <FORMAT>] [-o <PATH>]

--format may be gbnf (default), ebnf, or json-schema. If no output path is given, the grammar is written to stdout.

86.8 seedc prove

seedc prove <SOURCE> [-p <PROPERTY>]

Property may be no-deadlock, memory-safety, taint-safety, or all (default).

The seedvm binary executes compiled .aslb bytecode modules. It provides deterministic execution, instruction tracing, and proof generation.

87.1 Global Options

Flag	Description
-v, -vv, -vvv	Verbosity: info, debug, trace
-h, --help	Print help
-V, --version	Print version

87.2 seedvm run

seedvm run <MODULE> [OPTIONS]

Option	Description
-s, --seed <SEED>	Deterministic PRNG seed (default 0).
--max-stack <DEPTH>	Maximum operand stack depth (default 4096).

87.3 seedvm trace

Executes with full instruction tracing; same options as run. Outputs the schedule trace.

87.4 seedvm prove

seedvm prove <MODULE> [OPTIONS]

Option	Description
-s, --seed <SEED>	PRNG seed.
-o, --output <PATH>	Write proof artifact to file; default stdout.

88.1 Language Server (seedls)

The language server implements the Language Server Protocol (LSP) over stdio. It provides real‑time diagnostics via seedc::compile, completions for keywords and section identifiers, hover documentation, and stubs for go‑to‑definition, references, rename, and semantic tokens.

88.2 Formatter (seedfmt)

seedfmt [SOURCE] [OPTIONS]

Option	Description
-o, --output <PATH>	Write formatted output to file instead of in‑place.
-c, --check	Check only: exit non‑zero if formatting would change the file.
--indent-width <N>	Spaces per indent (default 4).
--tabs	Use tabs instead of spaces.
--max-width <N>	Maximum line width (default 100).

If SOURCE is - or omitted, seedfmt reads from stdin and writes to stdout. Otherwise it formats the file in place.

88.3 Debug Adapter (seeddbg)

The debug adapter implements the Debug Adapter Protocol (DAP) over stdio. It supports conditional breakpoints, log points, step‑in/step‑out/next/continue, threads, stack traces, scopes (Locals and Memory Layers), and variable inspection.

seedpkg manages ASL packages: install, publish, search, add, remove, init, login, and logout.

89.1 Global Options

Flag	Description
-v, -vv, -vvv	Verbosity: warn, info, debug.

89.2 Subcommands

Command	Description
install <PACKAGE> [--registry <URL>] [--dry-run]	Install a package from the registry. Version may be given with @.
publish [--path <PATH>] [--registry <URL>] [--token <TOKEN>] [--dry-run]	Publish a package to the registry. Requires a Seed.toml.
search <QUERY> [--limit <N>]	Search the registry.
add <PACKAGE> [VERSION_REQ]	Add a dependency to Seed.toml.
remove <PACKAGE>	Remove a dependency.
init [-n <NAME>] [--path <PATH>]	Create a new Seed.toml manifest.
login --registry <URL> --token <TOKEN>	Store authentication token.
logout	Remove stored token.

89.3 Lock File

seedpkg produces a Seed.lock file for reproducible builds, recording the exact version and checksum of every dependency. This file should be committed to version control.

The full grammar of ASL is stratified. The following is the union grammar for S3; lower strata are subsets. A machine‑checked proof (Lean 4) verifies that S0 ⊂ S1 ⊂ S2 ⊂ S3.

A.1 Program Structure

program ::= { item }

item ::= function_def
       | agent_def
       | section_def
       | memory_def
       | ontology_def
       | rule_def
       | prompt_def
       | evolution_def
       | training_def
       | safety_contract_def
       | temporal_contract_def
       | guardrail_def
       | think_profile_def
       | routing_def
       | session_def
       | capability_grant_def
       | trust_policy_def
       | corrigibility_def
       | dead_switch_def
       | provenance_policy_def
       | federation_def
       | mesh_def
       | identity_anchor_def
       | cryptographic_identity_def
       | heartbeat_def
       | dream_cycle_def
       | memory_governance_def
       | memory_consistency_def
       | dual_process_memory_def
       | episodic_recon_def
       | memory_cycle_def
       | adaptive_memory_def
       | evolutionary_memory_def
       | struct_def
       | enum_def
       | trait_def
       | impl_block
       | effect_def
       | handler_def
       | module_decl
       | import_decl
       | export_decl
       | expression_statement
       | seed_literal

A.2 Functions and Agents

function_def ::= ["pub"] "fn" identifier [generic_params]
                 "(" [parameters] ")" ["->" type]
                 [where_clause]
                 [contract_annotation]
                 [temporal_annotation]
                 [capability_annotation]
                 block_expression

agent_def ::= ["pub"] "agent" identifier [generic_params]
              ["extends" type]
              [stratum_clause]
              [identity_clause]
              [cryptographic_identity_clause]
              [heartbeat_clause]
              [dream_clause]
              [memory_hierarchy_clause]
              [federation_clause]
              [mesh_clause]
              [session_clause]
              [capability_clause]
              [trust_clause]
              [evolution_policy_clause]
              [training_clause]
              [safety_contract_clause]
              [temporal_contract_clause]
              [corrigibility_clause]
              [dead_switch_clause]
              [guardrail_clause]
              [think_profile_clause]
              [routing_clause]
              [provenance_clause]
              [context_budget_clause]
              "{" {agent_member} "}"

A.3 Types, Expressions, and Patterns (excerpt)

The full type, expression, and pattern grammars appear in Chapters 21–24.

type ::= primitive_type | path_type | generic_type | reference_type
        | slice_type | array_type | tuple_type | function_type
        | agentic_type | uncertain_type | dynamic_type | unknown_type

expression ::= assignment_expression
assignment_expression ::= pipeline_expression
                         | pipeline_expression "=" expression …
pipeline_expression ::= logical_or
                       | pipeline_expression "|>"  logical_or
                       | pipeline_expression "|>>" logical_or
                       | pipeline_expression "|&"  logical_or

primary ::= literal | identifier | "self" | "(" expression ")"
          | block_expression | if_expression | match_expression
          | for_expression | while_expression | loop_expression
          | async_block | closure_expression | infer_expression
          | uncertain_expression | observe_expression | seed_literal
          | redirect_expression | process_substitution | here_document
          | mesh_send_expression | transfer_expression | session_call_expression
          | capability_perform | provenance_tag_expression …

The complete, machine‑readable GBNF grammar for each stratum can be obtained with seedc --emit-grammar --stratum S0 --format gbnf.

Operators are listed from highest precedence to lowest.

Precedence	Operators	Associativity
1 (highest)	. :: [] () (call/index/member)	Left
2	? (postfix try)	—
3	?! (confidence gate)	—
4	as as?	—
5	- ! ~ * & && (unary)	Right
6	* / %	Left
7	+ -	Left
8	<< >>	Left
9	& (bitwise and)	Left
10	^	Left
11	| (bitwise or)	Left
12	== != < > <= >=	Left
13	&&	Left
14	||	Left
15	.. ..=	—
16	= += -= *= /= %= &= |= ^= <<= >>=	Right
17	|> |>> |&	Left
18 (lowest)	~> <~ transfer @@ :::	Left

C.1 Kinds

Kind	Examples
Type	Bool, i32, String, Uncertain<T>
Effect	{Network, Inference}
Region	session, persistent, federated
Lifetime	'a, 'b
Capability	capability token sets
Protocol	session protocol types
Probability	internal interval annotations

C.2 Coercions

• int → float (widening, implicit)
• float → int (lossy, explicit as)
• &T → T (auto‑deref)
• T → dyn Trait (if T: Trait)
• Certain<T> → Uncertain<T> (inject with interval [1.0, 1.0])

D.1 Built‑in Effects

Effect	Description
Inference	LLM inference call
MemoryRead	Reading from a memory layer
MemoryWrite	Writing to a memory layer
Network	Network I/O
FileIO	File system access
AgentSpawn	Spawning a new agent
DecisionLog	Appending to decision log
Capability(String)	Named capability usage

D.2 Capability Operations

Operation	Syntax
Grant	grant cap::X to principal [attenuate(…)] [expiry: d]
Attenuate	attenuate(token, allowed_effects: […])
Delegate	delegate cap::X to peer [with attenuation(…)]
Revoke	revoke cap::X
Perform	perform Effect::X(args) requires cap::X

D.3 Taint Modifiers

Modifier	Source
taint::external	Files, network, untrusted users
taint::inferred	Produced by infer<T>
taint::federated	From a federated peer
taint::user	From a human principal (may be untrusted)

D.4 Sanitization Policies

Policy	Reduction Factor
guardrail::content_policy	0.7
guardrail::pii_redaction	0.5
human::review(principal)	0.0 (on approval)
regex(pattern)	0.3

Layer	Schema Type	Mutability	Scope
L0 Working	WorkingMemoryItem	mutable	session
L1 Episodic	EpisodicEntry	append_only	persistent
L2 Semantic	SemanticEntry	mutable	persistent
L3 Procedural	ProceduralEntry	mutable	persistent
L4 Prospective	ProspectiveEntry	mutable	persistent
L5 Federated	FederatedFact	append_only	federated
L6 Identity	IdentityRecord	append_only	persistent
L7 Provenance Index	ProvenanceRecord	append_only	persistent

Full record definitions appear in Chapter 36.

A complete catalogue of seed::* modules appears in Chapters 84–85.

• Core: prelude, types, collections, string, iter, option, result, fmt, mem, ptr
• I/O: io, fs, path, net, process
• Concurrency: thread, sync, channel, actor, async
• Agent: agent, memory, decision, pipeline, heartbeat, dream
• Security: crypto, capability, sandbox, audit, taint, sanitizer
• Inference: inference, uncertain, confidence, cognitive, think, route
• Protocols: federation, mesh, session, mcp_server, mcp_client, a2a_card, a2a_task
• Identity & Provenance: identity, crypto_id, provenance, trace
• Evolution & Training: evolution, evolution_track, training, curriculum
• Tooling: grammar_strata, isa, conformance, decorators, macros

The ASL‑CONF‑15 suite contains 253 tests across 22 categories. See Chapter 90 for details. The complete inventory is maintained in the repository at tests/conformance/ and can be listed with seed test --conformance --list.

Change	Patch	Impact
Removal of user‑defined effect handlers (S0–S2)	15.18	All effect/handler blocks at S0–S2 are now compile errors. Use built‑in effect calls returning Computation<T,ε>.
Unified discharge construct	15.19	The discharge … with { … } block replaces standalone ?! for full threshold checks. perform must be lexically inside discharge.
Conservative uncertainty merge	15.20	Interval multiplication on bind; dependency coefficient κ removed from mandatory semantics.
S0 grammar refinements	15.21	Mandatory semicolons, mandatory commas, no trailing commas, blocks require at least one statement, type annotation on Computation right‑hand sides.
Compile‑time budget analysis	15.3	New context_budget clause with strict/monitor modes.
Agent contracts	15.4	New agent_contract top‑level item for resource governance.
TEE governance binding	15.5	New tee clause on agent declarations at S3.
Trajectory audit	15.6	New seed::trajectory_audit module; seed audit --trajectory command.
Corrigibility enforcement in heartbeat	15.23	Lexicographic task ranking at decide/act phases; discharge gate checks corrigibility.
IR Discharge instruction	15.24	IR now has a single Discharge instruction; Perform valid only inside Discharge region.

A complete alphabetical listing of all keywords by stratum appears in Chapter 7. All operators are listed with precedence and associativity in Appendix B.

Affine types

Types whose values may be used at most once. ASL uses affine types for capability tokens and owned values.

Algorithm W

The standard Hindley‑Milner type inference algorithm, extended in ASL with effect rows, affine tracking, and gradual typing.

Attenuation

The operation of narrowing a capability token’s scope; always safe and compiler‑verified.

Corrigibility

The property that an agent remains under human control; formalised in ASL by five lexicographically ordered utility heads (U1–U5).

CRDT

Conflict‑free Replicated Data Type; used in federated memory for convergence without coordination.

Decidable island

A finite‑horizon region of execution where safety can be certified in randomised polynomial time (Nayebi 2025).

Discharge

The syntactic gate that unwraps a Computation<T,ε> after checking confidence, taint, budget, and capabilities.

EBNF

Extended Backus‑Naur Form; used throughout the specification to define ASL’s grammar.

Effect row

A set of effect labels that a computation may perform. Effect rows are polymorphic and checked at compile time.

FGGM

Formally Guarded Generative Model; a rejection‑sampled LLM output with a verified fallback, ensuring outputs satisfy a formal contract (SEVerA 2026).

GRPO

Group Relative Policy Optimisation; a reinforcement learning algorithm supported natively in ASL.

HLC

Hybrid Logical Clock; combines physical time and a logical counter for causally consistent snapshots in federated systems.

LTL

Linear Temporal Logic; used in temporal contracts to specify ordering constraints on effects.

MESI

Modified, Exclusive, Shared, Invalid — a cache coherency protocol applied to strongly‑consistent memory layers.

Merkle proof

A compact cryptographic proof that a particular value is included in a Merkle tree; used for memory integrity and provenance.

OODA loop

Observe, Orient, Decide, Act — the decision cycle that the heartbeat implements (adapted to Observe, Decide, Act‑or‑Sleep, Log, Update).

PRISM

Progressive Reasoning and Integrated Synthesis Memory; the evolutionary memory subsystem that manages schema migration during agent evolution.

Provenance

The append‑only, Merkle‑proofed audit trail of every agent action.

Safe‑park

A restricted execution mode where all external effects are blocked; entered when the dead‑man’s switch fires or the control meter falls below critical.

Session types

A type discipline that guarantees deadlock‑free communication between agents by statically verifying protocol conformance.

SMT

Satisfiability Modulo Theories; used by the embedded solver in temporal contract enforcement.

Taint

A type‑level label that tracks the flow of untrusted data; prevents prompt injection and unsanitised data from reaching capability‑exercising code.

TEE

Trusted Execution Environment; hardware‑attested enclave that guarantees the integrity of agent execution.

Tri‑path router

The governance mechanism that dispatches every memory operation through one of three paths: read, write, or invalidate.

zkVM

Zero‑Knowledge Virtual Machine; used to generate cryptographic proofs that the agent binary, configuration, and identity anchor form a consistent triple.