007: The Agent Meta-Language

007 is an experimental programming language for agents that make agents.

Not a framework. Not a library. A language where autonomous agents are first-class citizens and agent-creation safety is treated as a language-design problem rather than an orchestration afterthought.

1. Current Evidence Boundary

The repository already has real substance:

• a substantial Rust workspace with parser, evaluator, and supporting tooling

• cargo test --workspace currently passing across the workspace

• draft proof artifacts in Idris2 and Agda

• Canonical Proof Suite runner wired and reporting (see status table below)

What this repository does not yet earn today:

• a complete soundness story for all of the language claims in the papers

• a warning-free clippy posture across the whole workspace

• publication-ready prose that cleanly matches the current checked artifact

• audited stable or production standing

• a fully-passing Canonical Proof Suite (live status table below)

1.1. Canonical Proof Suite

The runner for the M/S/E Canonical Proof Suite (TRG roadmap §1) is wired end-to-end. Live status (as of the last run on 2026-04-18): 28/35 passing, 7 in-progress, 0 not-started under the v1.1-proposed manifest (expanded from v1.0’s 15 entries; v1.1 entries are under a 90-day co-signed review window that closes 2026-07-17, during which they do not contribute to TRG grading). At the v1.0 baseline the suite stands at 8/15 passing. Per-entry detail is at audits/canonical-proof-suite/STATUS.adoc; the machine-readable manifest is at audits/canonical-proof-suite/MANIFEST.a2ml; the latest run output is at audits/canonical-proof-suite/REPORT.a2ml. Run locally with just canonical-proof-suite. Nightly CI is at .github/workflows/canonical-proof-suite.yml. The headline TRG grade is currently TRG-X (Untested) — see audits/audit-trg-2026-04-18.md — with a roadmap to TRG-D gated on closing the remaining 7 in-progress v1.0 scaffolds, parser-fuzz 24h evidence, and the panic-attack assail zero-findings sign-off.

2. The Name

007 — because this is the language of agents.

Named for the most famous agent designation in fiction, but the mission here is real: build a language where the grammar itself prevents the classes of bugs that plague multi-agent systems.

3. The Problem

When Agent A creates Agent B, it is writing a program. Almost all agent frameworks today treats this as string concatenation — prompts glued together, tools passed as JSON, behaviour defined in untyped configuration. This is the equivalent of building SQL queries by concatenating user input. We know how that ends…​

Well, maybe not all of us, so here’s the primer.

Multi-agent systems today suffer from:

• Agent injection — data that becomes control (prompt injection at the agent level)

• Protocol violations — agents that don’t follow communication contracts

• Resource leaks — spawned agents that are never collected

• Capability creep — agents that inherit permissions they shouldn’t have

• Coordination failures — deadlocks, livelocks, dropped messages between agents

These are not implementation bugs. They are language-level failures — the languages we use to build agents lack the constructs to prevent them.

4. The Solution: Six Pillars

007 is built on six foundational principles, each drawn from a proven language paradigm:

4.1. 1. Harvard Architecture (from JTV)

Grammatical separation of control (agent behaviour) and data (agent knowledge). An agent’s data expressions cannot contain control flow. This makes agent injection structurally impossible at the parser level.

-- This is DATA: pure, total, halting arithmetic
@total data context = {
  temperature: 0.7 + 0.0,
  max_tokens: 1000 + 24,
  knowledge: load("corpus.json")
}

-- This is CONTROL: behaviour, decisions, side effects
@impure control agent Analyst(ctx: context) {
  on receive(query) -> investigate(query)
}

4.2. 2. Actor Model with Supervision (from Elixir/BEAM)

Every agent is a lightweight process with isolated state. Agents communicate only via message passing. Supervisor agents manage lifecycles — if an agent crashes, its supervisor decides what to do (restart, escalate, ignore).

supervisor ResearchTeam {
  strategy: one_for_one,
  max_restarts: 3 per 60s,

  children: [
    agent Lead(caps: [spawn, coordinate]),
    agent Searcher(caps: [read_file, web_fetch]),
    agent Analyst(caps: [reason, summarise]),
  ]
}

4.3. 3. Capability-Based Security (from Pony/E/Wasm)

Agents can only perform actions they’ve been explicitly granted. Capabilities are part of the type system — not runtime permission checks. An agent spawned with caps: [read_file] literally cannot call write_file. The compiler rejects it.

-- Type error: Searcher does not have capability `write_file`
agent Searcher(caps: [read_file, web_fetch]) {
  on found(data) -> write_file("out.txt", data)  -- COMPILE ERROR
}

4.4. 4. Session Types (from academic PLT)

Communication protocols between agents are typed contracts. The compiler verifies that both sides of a conversation follow the protocol. No deadlocks. No protocol violations. No "I sent you a query but you sent me a farewell."

session protocol Investigation {
  Requester -> Investigator: Query(topic: String)
  loop evidence_loop {
    Investigator -> Requester: Evidence(finding: Data)
                              | Conclusion(result: Data)
    if Evidence: continue evidence_loop
    if Conclusion: break
  }
}

4.5. 5. Linear Agent Handles (from Ephapax)

Agent handles are linear types — they must be consumed exactly once. You cannot clone an agent handle (no accidental fan-out). You cannot drop one (no leaked agents). Every spawned agent has a known owner and a known fate.

-- Linear: must be used exactly once
linear let worker = spawn Searcher(caps: [read_file])

-- Using it:
send(worker, Query("find vulnerabilities"))  -- worker consumed

-- This would be a COMPILE ERROR:
-- send(worker, Query("something else"))  -- already consumed!

-- To reuse, the protocol must explicitly return the handle:
linear let (worker2, result) = exchange(worker, Query("find vulns"))

4.6. 6. Choreographic Compilation (from Chor-lambda)

Write the global multi-agent protocol once. The compiler projects it down to each agent’s local code. Instead of writing Agent A and Agent B separately and hoping they mesh, write the dance — the compiler gives each dancer their steps.

choreography peer_review(author: Author, reviewer: Reviewer) {
  author -> reviewer: submit(paper)
  reviewer -> author: feedback(comments)

  branch {
    | accept -> reviewer -> author: accepted
    | revise ->
        author -> reviewer: revision(updated_paper)
        goto peer_review  -- type-safe recursion
  }
}

-- Compiler generates:
-- Author.local_code  (knows only its sends/receives)
-- Reviewer.local_code (knows only its sends/receives)
-- Both guaranteed protocol-compatible

5. Design Influences

Source	What 007 Takes	Why
JTV (Julia-the-Viper)	Harvard architecture, purity levels (@total/@pure/@impure), reversibility	Agents can’t inject control into each other’s data. Reversibility enables undo.
Elixir/BEAM	Actor model, supervision trees, hot code swapping, distribution	Agents as processes. Fault tolerance. Live-update agent behaviour.
Chapel	Locale-aware parallelism, domain maps	Agents aware of where work runs: local GPU, remote API, edge node.
Ephapax	Linear types, region-based memory	Agent handles can’t leak. Resources consumed exactly once.
Pony	Reference capabilities, no-data-race guarantee	Compile-time proof that agents can’t share mutable state.
Unison	Content-addressable code	Agents referenced by hash. Immutable, verifiable, reproducible.
Chor-lambda	Choreographic programming	Global protocol view compiled to per-agent local code.
TLA+/Alloy	Temporal logic, model checking	Specify and verify agent behaviour over time.

6. Novel Contributions (I think!)-

007 introduces concepts not found in any existing language, except as referenced jtv (https://github.com/hyperpolymath/jtv and https://jtv-lang.org [under construction]) and typed-wasm (https://github.com/hyperpolymath/typed-wasm), again, as refrenced)

1. Harvard Architecture for Agent Creation — grammatical separation of agent data and control, making agent injection a parse error

2. Typed Agent Topologies — the compiler rejects malformed multi-agent configurations before they run

3. Choreographic Agents — global multi-agent protocols compiled to verified local agent code

4. Linear Agent Handles — spawned agents tracked by the type system, preventing leaks and duplication

5. Locale-Aware Agent Placement — declarative specification of where agent computation runs (GPU, API, edge)

6. Content-Addressable Agent Behaviour — agents referenced by hash of their behaviour, not by name — reproducible and auditable

7. Implementation Language

007’s compiler is implemented in Rust (primary: crates/oo7-core, parser, typechecker, evaluator, codegen) with a Zig compiler-core (compiler-core/zig/) providing native codegen backends. Formal proofs sit in Idris2, Agda, and Rocq under proofs/. The primary runtime target is the BEAM (Erlang VM, via an Elixir/OTP codegen path), which is also the best-tested backend.

Secondary codegen targets (narrower coverage):

• WASM / typed-wasm — typed-wasm is the only verified codegen path under the 2026-04-13 rollout; raw wasm32 is retained for pipeline smoke tests but is labelled RAW-NON-VERIFIED

• x86_64 / aarch64 / riscv64 (via Zig) — stage-2 function-body compilation done; non-linkable output (no ELF section/symbol tables yet)

• Cranelift / QBE — exist with narrower coverage

8. Status

Phase: typed-wasm-first rollout — compiler-core Phase 3 stage-2 complete across x86/arm/wasm (2026-04-13); typed-wasm adopted as the only verified codegen target; 007 IR/parser/emitter being lifted onto typed-wasm v1.1+ surface sugar. Overall completion: ~62%. Authoritative state: .machine_readable/STATE.a2ml.

9. Links

• Specification: Language Specification

• Grammar: Formal Grammar (EBNF)

• Design rationale: Design Rationale

• Examples: Example Programs

10. License

SPDX-License-Identifier: MPL-2.0

Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)