Skip to main content

CADL: Contract Architecture Description Language

Language Specification — Version 0.2 (Draft)

Graduate School of Informatics, Nagoya University — ERTL

October 10, 2026

Overview​

CADL (Contract Architecture Description Language) is a domain-specific language (DSL) for formally specifying, verifying, and deploying institutional designs in multi-agent System of Systems (SoS).

CADL adopts a three-layer architecture — Institution, Protocol, and Algorithm — so that governance rules and coordination mechanisms are described precisely within a single unified language. The Algorithm layer names the central and local algorithms each side runs; it does not describe their internals. From a CADL specification, the toolchain automatically generates simulator configurations and verifies design consistency.

Architecture at a Glance​

One source drives three outputs: formal verification and institutional-constraint code (smart contracts / policy / runtime classes) are produced from the parsed definition, and runtime simulator configs from the three-layer IR. Experiment results feed back into the CADL source so governance parameters (α, β, λ, ρ) can be tuned; α, β, and λ are the per-contract parameters, and ρ belongs to the motivation extension (Appendix C). The cadl tool covers the source, verifier, codegen, IR, and simulator-config steps; running experiments and evaluating them is done with a simulator or with CADL Explorer.

How to Read This Specification​

This document is organized into three parts. Readers are encouraged to follow the order below, but each chapter is also self-contained.

Part I — Background and Requirements​

  • 1. Introduction — Motivation, problem setting, and the role of CADL within the SoS research agenda.
  • 2. Objectives — What CADL aims to solve, and the scope of this draft.
  • 3. Comparison — Relationship to existing ADLs, contract languages, and multi-agent DSLs.
  • 4. Requirements — Functional and non-functional requirements that drive the language design.

Part II — Language and Design​

  • 5. Language Specification — Core syntax and semantics of the three layers (Institution / Protocol / Algorithm).
  • 6. Design — Design rationale, toolchain architecture, verification engine, and runtime system. The intermediate representation (IR) is described in Appendix E, §E.7 and the Glossary.
  • 7. Examples — Worked examples illustrating typical CADL usage.

Part III — Applications and Outlook​

  • 8. Use Cases — Application domains and case studies.
  • 9. Research — Open research questions and theoretical foundations.
  • 10. Roadmap — Implementation phases and the current status of the reference implementation.

Appendices​

Suggested Reading Paths​

  • First-time readers — Read Chapters 1–2, skim Chapter 5, then look at Chapter 7 for concrete examples. The Chapter 7 listings are conceptual; runnable examples are in the examples/ directory of the cadl repository and in the hands-on course.
  • Implementers / tool builders — Focus on Chapters 5, 6, and Appendix A.
  • Researchers — Chapters 3, 9, and 10 give the broader context and open problems.

Getting the tool​

The reference implementation is cadl. It is installed with pip install cadl-lang (Python 3.9+); the command is cadl. A first check is:

pip install cadl-lang
cadl --version

Then, with a .cadl file such as those in the repository's examples/ directory, run cadl check <file>.cadl and cadl verify <file>.cadl. See the repository README for all commands and the hands-on course for a guided walkthrough.

  • cadl — The CADL compiler and command-line tool (reference implementation), published on PyPI as cadl-lang.
  • CADL Explorer — An interactive web application that demonstrates the CADL governance pipeline end-to-end, from specification through simulation to governance evaluation.
  • cadl-raspimouse-simulator — The simulator used by the hands-on course.

Learning by doing​

To write and run the language rather than only read about it, see the hands-on materials: starting from robot delivery, they walk through authoring a spec, generating code, and running the simulation.

Status​

This is Version 0.2 (Draft). The language and toolchain are under active development; syntax and semantics may change in future revisions.

Version 0.2 reconciles the text of Version 0.1 with the reference implementation. The changes that affect how an existing file is read are:

  • β is the degree of centralisation of decision-making: 0 is fully decentralised and 1 is fully centralised (Section 5.4.2). Parts of Version 0.1 described it in the opposite direction.
  • SoS-DSL extension (Appendix E): on_violation.transition and on_match.transition name a target state (rules L-5 and M-3), and on_match.violation is a label that needs no declaration (rule M-2). The extension itself is still sos-dsl: 0.1.
  • A sharing: entry MUST be a quoted string (- "TAXI[*] -> CENTRAL : position"); unquoted, YAML reads it as a mapping and not as a string (Appendix A, §A.4).
  • The bound of a symbolic range is a symbolic size: in [1..N], N stands for any number of actors, and the language has no construct that gives it a value (Section 5.2.2, Appendix A, §A.3).
  • Identifiers are ASCII; strings and comments may contain any Unicode character (requirement NFR-7 in Chapter 4, Appendix A, §A.1).

The motivation extension keeps its own label, v0.1-ext.

The specification and the reference implementation are numbered independently: this specification is Version 0.2, and the reference implementation it was checked against is cadl 0.3.13.

Feedback and discussion are welcome via GitHub Issues. Problems with the specification or this site can be reported at cadl-spec Issues.