CADL: Contract Architecture Description Language

English | 日本語

CADL is a domain-specific language for formally describing, verifying, and deploying institutional designs in Systems of Systems (SoS). It enables stakeholders — from engineers to citizens — to define governance rules, contracts, protocols, and incentive structures in a machine-readable, verifiable format.

CADL is developed at ERTL, Graduate School of Informatics, Nagoya University.

Documentation

• Specification and language reference (日本語) — start with Chapter 5 for the language and Appendix A for the complete syntax
• Hands-on course — a guided walkthrough of the toolchain
• This README — installation, commands, and the bundled examples
• CHANGELOG · Contributing · Security policy · Issues

Motivation

In SoS environments, independently operated systems must coordinate under shared rules. Today, these rules exist mostly as natural-language contracts and tacit agreements, making them prone to ambiguity, contradiction, and drift between design intent and implementation.

CADL addresses three core goals:

1. Make institutions computable — Model real-world rules (authority structures, information-sharing policies, incentive mechanisms) as first-class data objects that can be copied, composed, versioned, and searched.
2. Detect contradictions and violations — Enable automated consistency checking (via SMT solvers and model checkers) and runtime monitoring of institutional constraints.
3. Generate executable artifacts — Translate verified institutional designs into control logic, monitoring code, and smart contracts for target platforms.

Language Overview

A CADL file (.cadl) uses a YAML-like declarative syntax. Each file describes one SoS definition containing:

A contract may also carry lifecycle: and monitors: blocks (the SoS-DSL extension), which describe the states a contract instance goes through and the conditions watched while it runs. The complete list of keys is in Appendix A and Appendix E of the specification.

Institutional Parameters

CADL quantifies institutional characteristics using three continuous parameters in [0, 1]:

• alpha — Information sharing degree (0 = local only, 1 = full sharing)
• beta — Decision centralization (0 = fully distributed, 1 = centralized)
• lambda — Incentive strength (0 = directive-based, 1 = market mechanism)

Example

sos:
  name: "RobotDeliverySystem"
  type: Acknowledged
  version: "1.0.0"

  actors:
    - id: DISPATCHER
      role: "global_planner"
      autonomy: low
    - id: "ROBOT[1..N]"
      role: "delivery_vehicle"
      autonomy: high

  contracts:
    - id: DELIVERY_SLA
      parties:
        - DISPATCHER
        - "ROBOT[*]"
      assume:
        - "DISPATCHER.is_operational == true"
        - "network_latency <= 200ms"
      guarantee:
        - "all_routes_conflict_free()"
        - "delivery_time <= promised_time * 1.2"
      authority:
        decision_holder: DISPATCHER
        beta: 0.8
      information:
        alpha: 0.8
      incentives:
        type: reputation
        lambda: 0.5
        rules:
          - "reward(ROBOT[i], 10) when on_time_delivery"
          - "penalty(ROBOT[i], -5) when route_deviation"
      duration: indefinite

  protocols:
    - id: FAILURE_REPLAN
      trigger: "road_failure_detected_by(ROBOT[i])"
      steps:
        - "ROBOT[i] -> DISPATCHER : failure_report"
        - "DISPATCHER : recompute_routes"
        - "DISPATCHER -> ROBOT[*] : new_route"
      timing:
        max_total: 500ms
      postcondition: "all_routes_conflict_free()"

  transitions:
    - from: IDLE
      to: ACTIVE
      condition: "delivery_request_pending == true"
      safety_invariant: "all_routes_conflict_free()"
    - from: ACTIVE
      to: IDLE
      condition: "all_deliveries_complete == true"
      safety_invariant: "all_robots_at_base == true"

Installation

Requires Python 3.9+.

pip install cadl-lang

# With AI features (requires Anthropic API key)
pip install "cadl-lang[ai]"

The distribution is named cadl-lang on PyPI; the import package and the command are both cadl.

To work on CADL itself, install from source:

git clone https://github.com/ertlnagoya/cadl
cd cadl
pip install -e ".[dev]"
pytest

Usage

# Parse a CADL file and display summary
cadl parse examples/robot_delivery.cadl

# Parse and run type checks
cadl check examples/robot_delivery.cadl

# Full verification (type check + SMT + deadlock detection)
cadl verify examples/robot_delivery.cadl

# Generate Python runtime code
cadl codegen examples/robot_delivery.cadl -o /tmp/robot_delivery

# Generate Solidity smart contracts
cadl codegen examples/robot_delivery.cadl --target solidity -o /tmp/solidity_out

# Generate OPA/Rego policies
cadl codegen examples/robot_delivery.cadl --target opa -o /tmp/rego_out

# Generate Unity C# for SoS-DSL contracts (lifecycle / monitors)
cadl codegen examples/sos_dsl_robot_delivery.cadl --target unity-csharp -o /tmp/unity_out

# Analyze regime transitions
cadl regime-map examples/smart_city_traffic.cadl
cadl regime-map examples/smart_city_traffic.cadl --format dot -o regime.dot

# IEC 62853-oriented dependability summary
cadl iec62853 examples/robot_delivery.cadl
cadl iec62853 examples/smart_city_traffic.cadl --format json

# Generate CADL from natural language (requires ANTHROPIC_API_KEY)
cadl ai "A fleet of 5 autonomous drones surveying farmland, coordinated by a ground station"
cadl ai -f requirements.txt -o output.cadl

Architecture

The CADL toolchain follows a standard compiler pipeline:

.cadl file
    |
    v
+------------------+
|  Parser          |  YAML structure + Lark expression grammar
|  (parser.py)     |  -> Abstract Syntax Tree
+--------+---------+
         |
         v
+------------------+
|  Type Checker    |  Actor reference resolution, parameter range
|  (type_checker)  |  validation, contract party consistency
+--------+---------+
         |
         v
   [Checked AST]
         |
    +----+----+----------+-----------+
    v         v          v           v
  SMT       Code       Regime      IEC 62853
  Verify    Generate   Map         Summary
  (Z3)      (codegen/) (regime_map) (iec62853)
              |
        +-----+-----+--------+
        v     v     v        v
     Python Solidity OPA/Rego Unity C#

Code Generation

cadl codegen generates executable code from a CADL definition. It runs the type check but not the verifier, so run cadl verify first. Four targets are supported:

Python (--target python, default):

Generated code inherits from base classes in cadl.codegen.runtime_support.

Solidity (--target solidity):

Generates Ethereum smart contracts (.sol):

• One contract per CADL ContractDef with checkAssumptions(), checkGuarantees(), runMonitorCycle()
• RegimeController.sol with enum-based state machine for transitions
• Main orchestrator contract importing all sub-contracts
• Institutional parameters (alpha, beta, lambda) as scaled uint256 constants

OPA/Rego (--target opa):

Generates Open Policy Agent policies (.rego):

• One package per CADL ContractDef with assumptions_hold, guarantees_hold, allow, and violation rules
• Main policy package aggregating all contracts
• Information sharing and authority policy rules

Unity C# (--target unity-csharp):

Generates C# for contracts that use the SoS-DSL extension (lifecycle: / monitors:):

• Generated/<Contract>State.cs, <Contract>Contract.cs, <Contract>Monitors.cs per contract
• Runtime/ support classes (contract runtime, event bus, predicate evaluator)

The hands-on textbook runs this target end to end.

Regime Transitions

cadl regime-map analyzes the regime transition graph:

• Builds a directed graph of regime states from transitions: definitions
• Reachability analysis — BFS from initial state to find unreachable regimes
• Dead-state detection — identifies states with no outgoing transitions
• Cycle detection — Tarjan's SCC algorithm to find cyclic regime patterns
• Shortest path — BFS-based shortest path between any two regimes
• Export formats: text summary, Graphviz DOT, JSON

IEC 62853-oriented Summary

cadl iec62853 summarises a CADL definition around the themes of IEC 62853 (Open Systems Dependability). The indicator names are defined by CADL, not by the standard, and the report does not assess conformance to IEC 62853.

Simulator Config Generation

cadl sim-* commands lower a CADL definition to a 3-layer Intermediate Representation (IR) and generate simulator-specific configuration files:

CADL YAML ─── Parser ──► AST ─── Lowering ──► 3-Layer IR ─── Generator ──► Simulator Config
                                                 │
                                    ┌────────────┼────────────┐
                                    ▼            ▼            ▼
                              Layer 1       Layer 2       Layer 3
                            Institution    Protocol     Algorithm
                            /Governance   /Interaction  /Operational

Three simulator targets:

# Validate IR
cadl sim-validate examples/a_sos_robot_delivery.cadl

# Print IR (YAML or JSON)
cadl sim-ir examples/a_sos_robot_delivery.cadl
cadl sim-ir examples/c_sos_taxi_fleet.cadl --format json

# Generate simulator configs
cadl sim-gen examples/a_sos_robot_delivery.cadl --target python -o sim_config.yaml
cadl sim-gen examples/a_sos_robot_delivery.cadl --target unity -o sim_config.json
cadl sim-gen examples/c_sos_taxi_fleet.cadl --target go -o sim_config.json

A-SoS vs C-SoS Comparison

Raspimouse Swarm Simulator — D-SoS / C-SoS / MCP-SoS Comparison

Three CADL definitions model the same 5-robot swarm on an 11-node graph network under different SoS paradigms. These connect to the raspimouse-swarm-simulator (a research repository that is not public; the part needed for the hands-on course is published as cadl-raspimouse-simulator) via the Unity config generator (cadl sim-gen --target unity).

The beta and alpha rows show the values of the main contract of each definition; the C-SoS and MCP-SoS files contain a second contract with its own values.

# Generate Unity configs for all three modes
cadl sim-gen examples/raspimouse_d_sos.cadl --target unity -o output/raspimouse_d_sos_unity.json
cadl sim-gen examples/raspimouse_c_sos.cadl --target unity -o output/raspimouse_c_sos_unity.json
cadl sim-gen examples/raspimouse_mcp_sos.cadl --target unity -o output/raspimouse_mcp_sos_unity.json

AI Integration

cadl ai generates CADL from natural language descriptions via Claude API:

1. User provides an NL description (Japanese or English)
2. Claude generates a CADL definition using few-shot examples
3. The generated CADL is parsed and type-checked
4. On validation errors, the system retries with error feedback

Requires ANTHROPIC_API_KEY environment variable and pip install "cadl-lang[ai]".

Type Checks

The type checker (cadl check) validates:

1. Actor reference existence — Actors referenced in parties, authority, information sharing, protocol steps, and assume: / guarantee: predicates are defined. In a predicate a name is treated as an actor when it is indexed (ROBOT[i]) or is the object of a member access (ROBOT.battery); a bare name is taken as a state variable
2. Contract party consistency — Every contract has parties, and no party is listed twice
3. Protocol step validity — Senders and receivers match actor definitions
4. Information sharing coherence — Sharing declarations reference valid actors
5. Parameter range constraints — 0 <= alpha, beta, lambda <= 1
6. Unique ids and known severities — No duplicate actor, contract, protocol, or metric ids; severity: is Minor, Major, or Critical
7. Identifiers — Actor, contract, protocol, and metric ids and regime names are ASCII identifiers and are not reserved words (AND, OR, NOT, IN, in, exists, true, false)
8. Sharing entries — Each sharing: entry is a quoted string "SOURCE -> TARGET : item"; an unquoted or malformed entry is an error, and an item with arguments is accepted with a warning
9. Autonomy — autonomy: is low, medium, or high
10. SoS-DSL static semantics (Appendix E, E.4) — in a lifecycle:, the initial, terminal, from, to, and on_violation.transition states are listed in states, and a terminal state exists and is reachable (L-1, L-2, L-3, L-5); the on_match.transition of a monitor is a state of the same contract (M-3); states, transition ids, and monitor ids are identifiers and the ids are unique; the actors of a message event in on: are declared, and so is the object of each observe: entry (M-1). Warnings: a deadline: without on_violation: (L-4) and an on:, when:, or rule: that is not a rule of Appendix E

It also reports, without failing the check, a codegen: target that cadl codegen cannot emit (warning), an extension name it does not know, and a motivation: block, which it keeps and passes on in cadl sim-ir but does not interpret (informational).

Hands-on

A self-paced workshop of about 95 minutes (or a 5-session exercise course) walks you through the complete CADL toolchain end-to-end on a robot delivery System of Systems: CADL modelling → SoS-DSL contracts (lifecycle + monitors) → visualisation → code generation → live simulation.

The hands-on materials include:

• Main textbook — six 15-minute steps, with full bilingual EN / JA pages and a runnable end-to-end script (scripts/sos_dsl_handson_e2e.sh).
• Exercises booklet — a 5-session structured course (compact 3-session version available) with graded ★ / ★★ / ★★★ tasks and a rubric.
• Academic background — Maier's five SoS criteria, the ISO/IEC/IEEE 21839 / 21840 / 21841 standards, related research (ADLs, Normative MAS, Runtime Verification), and an annotated bibliography.

The materials are hosted in the cadl-spec repository — English sources under docs/handson/, Japanese under i18n/ja/docusaurus-plugin-content-docs/current/handson/ — and rendered on the Hands-on section of the spec website.

To run the full pipeline locally on the bundled robot-delivery example:

./scripts/sos_dsl_handson_e2e.sh

This generates the IR JSON, the Unity C# tree, and drops the latter into the Unity project of cadl-raspimouse-simulator when it is cloned next to this repository (otherwise pass --unity "" to stop after code generation). See the hands-on textbook for the rest of the walkthrough.

Examples

CADL Definitions

Demo Scripts

Run the demo scripts to see the full toolchain in action:

# End-to-end workflow: parse -> verify -> codegen (Python/Solidity/Rego) -> regime map -> IEC 62853
python examples/demo_robot_delivery.py

# Regime transitions, dependability summary, and multi-target generation
python examples/demo_smart_city.py

# Side-by-side comparison of Python, Solidity, and Rego output
python examples/demo_codegen_targets.py

# 3-layer simulator IR and A-SoS / C-SoS comparison
python examples/demo_sim_ir.py

Project Structure

src/cadl/
  __init__.py          Package root
  ast_nodes.py         AST node definitions (30+ dataclasses)
  grammar.lark         Lark grammar for the expression sub-language
  parser.py            Hybrid parser (YAML structure + Lark expressions)
  type_checker.py      Static semantic checks
  verifier.py          SMT-based contract verification (Z3)
  deadlock.py          Protocol deadlock detection
  regime_map.py        Regime transition graph analysis
  iec62853.py          IEC 62853-oriented dependability summary
  unparse.py           Expression AST back to CADL source text
  cli.py               Command-line interface
  codegen/
    __init__.py        Public generate() API (multi-target dispatch)
    runtime_support.py Base classes for generated code
    expr_compiler.py   Expression AST -> Python source
    emitter.py         Code emission utilities
    actor_gen.py       Actor class generation
    contract_gen.py    Contract monitor generation
    protocol_gen.py    Protocol state machine generation
    transition_gen.py  Regime controller generation
    metric_gen.py      Metrics collector generation
    runtime_gen.py     Orchestrator generation
    solidity/
      solidity_expr.py Expression AST -> Solidity source
      solidity_gen.py  Solidity smart contract generation
    opa/
      rego_expr.py     Expression AST -> Rego source
      rego_gen.py      OPA/Rego policy generation
    unity_csharp/
      contract_emitter.py  Per-contract C# (state enum, contract, monitors)
      runtime_template.py  C# runtime support emitted with every generation
    safety.py          Input checks applied before code generation
  ai/
    __init__.py        Public generate_cadl() API
    prompts.py         System prompts and few-shot examples
    llm_client.py      Claude API client wrapper
    nl_to_cadl.py      NL-to-CADL generation pipeline
  sim/
    __init__.py        Public API: lower_to_ir, validate_ir, generate_config
    ir.py              3-layer IR dataclasses (SimIR, InstitutionLayer, etc.)
    lower.py           AST -> IR lowering
    validate.py        IR-level validation
    gen_python.py      IR -> Python simulator YAML config
    gen_unity.py       IR -> Unity JSON config
    gen_go.py          IR -> Go JSON config

tests/
  test_parser.py         Parser tests
  test_type_checker.py   Type checker tests
  test_verifier.py       SMT verifier tests
  test_deadlock.py       Deadlock detector tests
  test_codegen.py        Python code generation tests
  test_ai.py             AI integration tests
  test_runtime.py        Runtime base class tests
  test_regime_map.py     Regime map graph analysis tests
  test_solidity_gen.py   Solidity code generation tests
  test_opa_gen.py        OPA/Rego code generation tests
  test_iec62853.py       IEC 62853-oriented summary tests
  test_sim_ir.py         Simulator IR lowering and validation tests
  test_sim_gen.py        Simulator config generator tests
  test_sim_ir_sos_dsl.py SoS-DSL lifecycle / monitors in the simulator IR
  test_sos_dsl_extension.py       SoS-DSL parser tests
  test_unity_csharp_codegen.py    Unity C# generation tests
  test_unity_csharp_structural.py Structural checks on the generated C#
  test_expr_parser.py    Expression grammar tests
  test_unparse.py        Expression round-trip tests
  test_name_resolution.py Actor vs state-variable resolution in generated code
  test_method_dispatch.py Verification method dispatch tests
  test_codegen_safety.py Code generation input-safety tests
  test_examples_verify.py Every example passes `cadl verify`
  test_actor_reference_check.py   Which names `cadl check` treats as actors
  test_conformance_checks.py      Identifier rules, sharing entries, codegen targets, extensions
  test_codegen_deterministic.py   Generated code is identical across runs
  test_keyword_boundaries.py      Keywords are not split out of longer names

examples/
  robot_delivery.cadl        Robot delivery SoS (Acknowledged type)
  smart_city_traffic.cadl    Smart city traffic management (Collaborative type)
  supply_chain.cadl          Supply chain management (Collaborative type)
  iot_data_sharing.cadl      IoT data sharing (Virtual type)
  household_chores.cadl      Family chore sharing (Collaborative type)
  demo_robot_delivery.py     End-to-end workflow demo
  demo_smart_city.py         Regime map & IEC 62853 demo
  demo_codegen_targets.py    Multi-target code generation demo
  a_sos_robot_delivery.cadl  A-SoS MAPF robot delivery sample
  c_sos_taxi_fleet.cadl      C-SoS autonomous taxi fleet sample
  raspimouse_d_sos.cadl      Raspimouse swarm D-SoS (Directed)
  raspimouse_c_sos.cadl      Raspimouse swarm C-SoS (Collaborative)
  raspimouse_mcp_sos.cadl    Raspimouse swarm MCP-SoS (LLM-controlled)
  test_raspimouse.sh         Parse, validate, and generate Unity configs for Raspimouse
  sos_dsl_robot_delivery.cadl  Robot delivery with SoS-DSL lifecycle and monitors
  demo_sim_ir.py             3-layer simulator IR and A-SoS / C-SoS comparison demo

scripts/
  sos_dsl_handson_e2e.sh     Hands-on pipeline: check -> Sim-IR -> Unity C# -> Unity project

Status

CADL is alpha software (see CHANGELOG.md); the language and the generated output may change between releases.

Related Projects

• cadl-spec — The specification and the hands-on course, published at https://www.ertl.jp/cadl-spec/.
• cadl-explorer — A Streamlit application that draws the contract lifecycle from the IR that cadl sim-ir produces and explores governance settings on a synthetic model.
• cadl-raspimouse-simulator — The simulator used by the hands-on course: Unity project, Go arbitrator and Python reference runtime for the C-SoS robot-delivery scenario.
• raspimouse-swarm-simulator (research repository, not public; public export: cadl-raspimouse-simulator) — Multi-agent swarm robotics simulation platform. CADL files in examples/raspimouse_*.cadl describe its three SoS modes, and the Unity config generator produces configuration JSON for the simulator.

References

• Benveniste et al., "Contracts for System Design," Foundations and Trends in EDA, 2018.
• ISO/IEC/IEEE 21841:2019, Taxonomy of Systems of Systems.
• Saoud et al., "Assume-guarantee contracts for continuous-time systems," Automatica, 2021.
• IEC 62853:2018, Open Systems Dependability.
• C. Shimoyama and Y. Matsubara, "Governance as a Structural Design Variable: An Empirical Study of Performance-Autonomy Value Spaces in Systems of Systems," in Proc. 21st International Conference on System of Systems Engineering (SoSE), 2026.

License

Apache License 2.0. Releases up to and including 0.3.2 were published under the MIT License.