agenticraft-foundation 0.1.1

Formally verified mathematical foundations for multi-agent AI coordination.

The core verification engine behind AgentiCraft — an enterprise-grade platform for building production-ready AI agents and multi-agent systems.

13 CSP operators · Multiparty Session Types · Hypergraph Topology · Multi-Protocol Routing · CTL Model Checking · Probabilistic Verification · 1300+ tests · Minimal dependencies

Install

With uv (recommended):

uv add agenticraft-foundation

Or with pip:

pip install agenticraft-foundation

Quick Start

from agenticraft_foundation import (
    Event, Prefix, Stop, Parallel,
    Interrupt, Timeout, Guard, TIMEOUT_EVENT,
    build_lts, traces, detect_deadlock, is_deadlock_free,
)

# Define agent events
process_data = Event("process_data")
handle_priority = Event("handle_priority")
return_result = Event("return_result")

# Build an interruptible agent task
task = Prefix(process_data, Prefix(return_result, Stop()))
handler = Prefix(handle_priority, Stop())
agent = Interrupt(primary=task, handler=handler)

# Agent can do its task OR be interrupted by priority request
assert process_data in agent.initials()
assert handle_priority in agent.initials()

# Add a timeout with fallback
fallback = Prefix(Event("return_cached"), Stop())
bounded = Timeout(process=agent, duration=30.0, fallback=fallback)

# Analyze the process
lts = build_lts(bounded)
print(f"States: {len(lts.states)}")
print(f"Deadlock-free: {is_deadlock_free(bounded)}")

deadlocks = detect_deadlock(bounded)
print(f"Deadlock states: {len(deadlocks.deadlock_states)}")

t = list(traces(lts, max_length=5))
print(f"Traces: {len(t)}")

See the RAG pipeline verification for an end-to-end example combining CSP, deadlock detection, topology analysis, and temporal logic across 4 agents. More examples in the docs.

Verify an AgentiCraft app manifest

The one-call adoption surface. Pass an app.yaml dict (or any object exposing model_dump(by_alias=True)); get a structured report.

import yaml
from agenticraft_foundation import verify

with open("app.yaml") as f:
    manifest = yaml.safe_load(f)

report = verify(manifest)
print(report.summary())

if not report.passed:
    for check in report.errors:
        print(f"ERROR: {check.name} — {check.message}")
    raise SystemExit(1)

Five checks run on every manifest:

topology.connected severity is driven by topology.coordination_mode declared in the manifest:

• a2a → disconnected = error (real partition bug)
• hybrid → disconnected = warning (mixed orchestrator + direct)
• orchestrated (default) → disconnected = info (external orchestrator drives each agent independently)

The report passes iff every error-severity check passes. Pass strict=True to promote warnings to errors for enterprise gating:

report = verify(manifest, strict=True)  # warnings now block

Serialize the report for CI logs or API responses with report.to_dict() — every field, including per-check duration_ms and structured details, round-trips through JSON.

CLI

The [cli] extra adds PyYAML and a module-level entry point:

pip install agenticraft-foundation[cli]
python -m agenticraft_foundation app.yaml          # human-readable summary
python -m agenticraft_foundation app.yaml --strict # treat warnings as errors
python -m agenticraft_foundation app.yaml --json   # machine-readable for CI

Exit codes: 0 (passed), 1 (verification failed), 2 (input error).

The function accepts plain dicts so the foundation has zero dependency on the wider AgentiCraft platform — callers decide whether to parse app.yaml via pydantic, raw YAML, or anything else. AgentiCraft's craft push invokes verify() on every marketplace publish.

Architecture

graph TB
    subgraph algebra["algebra"]
        csp["CSP Operators<br/><i>13 process primitives</i>"]
        sem["Semantics<br/><i>LTS, traces, deadlock</i>"]
        eq["Equivalence<br/><i>bisimulation, failures</i>"]
        ref["Refinement<br/><i>trace, failures, FD</i>"]
        pat["Patterns<br/><i>coordination templates</i>"]
        csp --> sem
        sem --> eq
        sem --> ref
        csp --> pat
    end

    subgraph mpst["mpst"]
        gt["Global Types<br/><i>protocol specification</i>"]
        lt["Local Types<br/><i>projected per-role</i>"]
        proj["Projector<br/><i>global to local</i>"]
        mon["Session Monitor<br/><i>runtime checking</i>"]
        gt --> proj --> lt --> mon
    end

    subgraph topology["topology"]
        lap["Laplacian Analysis<br/><i>spectral decomposition</i>"]
        conn["Connectivity<br/><i>vertex/edge, bridges</i>"]
        hyper["Hypergraph<br/><i>group coordination</i>"]
        lap --- conn
        lap --- hyper
    end

    subgraph protocols["protocols"]
        pg["Protocol Graph<br/><i>G = (V, E, P, &Phi;, &Gamma;)</i>"]
        route["Routing<br/><i>Dijkstra, BFS, resilient</i>"]
        semr["Semantic Routing<br/><i>capability embeddings</i>"]
        compat["Compatibility<br/><i>translation costs</i>"]
        wf["Workflows<br/><i>W = (T, &prec;, &rho;)</i>"]
        tx["Transformers<br/><i>composable T: M&rarr;M'</i>"]
        pg --> route
        pg --> semr
        compat --> route
        compat --> tx
        pg --> wf
    end

    subgraph verification["verification"]
        inv["Invariant Checker<br/><i>runtime assertions</i>"]
        cex["Counterexamples<br/><i>structured explanations</i>"]
        ctl["Temporal Logic<br/><i>CTL model checking</i>"]
        prob["Probabilistic<br/><i>DTMC reachability</i>"]
        inv --- cex
        ctl --- prob
    end

    subgraph specs["specifications"]
        formal["Consensus Properties<br/><i>agreement, validity</i>"]
        wcon["Weighted Consensus<br/><i>quality-weighted quorum</i>"]
        mas["MAS Mappings<br/><i>BDI, Contract Net</i>"]
        formal --- wcon
        formal --- mas
    end

    subgraph complexity["complexity"]
        bounds["Complexity Bounds<br/><i>30+ theoretical limits</i>"]
        faults["Fault Models<br/><i>classical + LLM-specific</i>"]
        bounds --- faults
    end

    pat -.->|"coordination<br/>patterns"| gt
    ref -.->|"property<br/>checking"| formal
    ref -.->|"counterexample<br/>generation"| cex
    sem -.->|"LTS model<br/>checking"| ctl
    lap -.->|"topology<br/>metrics"| pg
    hyper -.->|"group<br/>structure"| wf

    style algebra fill:#0d94881a,stroke:#0D9488
    style mpst fill:#0d94881a,stroke:#0D9488
    style topology fill:#0d94881a,stroke:#0D9488
    style protocols fill:#0d94881a,stroke:#0D9488
    style verification fill:#0d94881a,stroke:#0D9488
    style specs fill:#0d94881a,stroke:#0D9488
    style complexity fill:#0d94881a,stroke:#0D9488

Operators

All 13 CSP operators implement the full Process contract: kind, alphabet(), initials(), after(event).

Core Primitives (8)

Agent-Specific Extensions (5)

See the full operator reference for recursion, verification pipeline, and detailed semantics.

Modules

See the docs for: Protocol Graph Model | Verification Pipeline | Spectral Topology | Fault Models & Complexity | Consensus & MAS Mappings | Full API Reference

Development

# Install dev dependencies
uv sync --group dev

# Run tests
uv run pytest tests/ -v

# Run with coverage
uv run pytest tests/ --cov=agenticraft_foundation --cov-report=html

# Lint
uv run ruff check src/ tests/

# Format
uv run ruff format src/ tests/

# Type check
uv run mypy src/

Dev Container

Open in VS Code with the Dev Containers extension for a ready-to-go environment -- Python 3.12, uv, Ruff, and mypy pre-configured with format-on-save.

# Or build manually with Docker
docker build -t agenticraft-foundation .devcontainer/

Why Formal Methods for Agents?

Multi-agent systems fail in production because coordination bugs are invisible until runtime. Formal verification catches them at design time:

• Deadlock detection -- Find states where no agent can make progress
• Trace analysis -- Verify all possible execution sequences
• Refinement checking -- Prove implementation matches specification
• Counterexample generation -- Structured explanations of why verification fails
• Temporal logic -- CTL model checking: "always", "eventually", "until" over LTS
• Probabilistic verification -- DTMC reachability, steady-state, expected steps for stochastic agents
• Protocol verification -- Ensure multi-agent communication is well-formed
• Spectral analysis -- Quantify topology resilience via algebraic connectivity
• Workflow validation -- Verify protocol executability before deployment
• Fault tolerance -- Model LLM-specific failure modes alongside classical faults

References

• Hoare, C.A.R. (1985). Communicating Sequential Processes. Prentice Hall.
• Roscoe, A.W. (1998). The Theory and Practice of Concurrency. Prentice Hall.
• Clarke, E.M., Emerson, E.A. (1981). Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic. Workshop on Logics of Programs.
• Baier, C., Katoen, J.-P. (2008). Principles of Model Checking. MIT Press.
• Honda, K., Yoshida, N., Carbone, M. (2016). Multiparty Asynchronous Session Types. JACM.

See the full references in the documentation.

Citation

@software{agenticraft_foundation,
  title = {agenticraft-foundation: Formally Verified Foundations for Multi-Agent AI},
  author = {Khateeb, Zaher},
  year = {2026},
  url = {https://github.com/agenticraft/agenticraft-foundation},
  doi = {10.5281/zenodo.20466793},
  version = {0.1.0},
}

License

Apache License 2.0