2026-06-19·9 min read·sota.io team

Deploy CADP to Europe — Hubert Garavel 🇫🇷 (INRIA Grenoble 1989), the EU-Native Distributed Systems Verification Toolbox Behind Airbus and French Nuclear Safety, on EU Infrastructure in 2026

When Airbus engineers verify the communication behaviour of the A380's Avionics Full-Duplex Switched Ethernet (AFDX) network — that every critical message is delivered within its deadline, that no priority inversion can cause a safety-relevant frame to be dropped, that the entire distributed avionics system cannot deadlock — they reach for CADP. Not a unit testing framework, not a static analyser: a process algebra verification toolbox that models distributed systems as communicating concurrent processes, computes their complete state spaces as labeled transition systems, and verifies temporal properties using μ-calculus model checking with mathematical exhaustiveness.

CADP (Construction and Analysis of Distributed Processes) has been developed since 1989 at INRIA Grenoble Rhône-Alpes — the Institut National de Recherche en Informatique et en Automatique, France's national computer science research institute, one of the largest public research institutions in the world. CADP's principal architect is Hubert Garavel 🇫🇷, who has led the CONVECS (Construction of Verified Concurrent Systems) team at INRIA Grenoble for over three decades, building a toolbox that now contains more than 50 integrated tools, compilers, and utilities for every stage of the distributed systems verification workflow.

CADP's roots are in LOTOS (Language of Temporal Ordering Specification), the ISO 8807 standard developed in the 1980s for specifying distributed systems — particularly OSI (Open Systems Interconnection) network protocols. LOTOS combined CCS (Robin Milner's Calculus of Communicating Systems, Edinburgh) with ACT ONE algebraic data type specifications, producing a rigorous language for protocol behaviour specification that became the first ISO-standardised process algebra. From LOTOS, Garavel's group developed the full CADP toolchain: a LOTOS compiler, a binary format for labeled transition systems, a μ-calculus model checker, bisimulation checkers, minimisation algorithms, and a distributed verification engine — all integrated around a common intermediate representation called BCG (Binary Coded Graphs).

In 2026, with the EU AI Act mandating systematic verification of distributed high-risk AI systems and NIS2 requiring formal analysis of network protocol implementations, CADP offers the most comprehensive EU-native distributed systems verification environment available: every tool in the CADP suite was designed, implemented, and is maintained by INRIA — a French public institution funded by the French Ministry of Higher Education and Research and the French Ministry of Economy — with no US ownership, no Cloud Act exposure, no ITAR restriction.

What CADP Is — Process Algebra Verification at Scale

CADP's central abstraction is the Labeled Transition System (LTS): a directed graph where nodes are system states and edges are labeled by the actions a process can perform (internal actions τ, or observable events on named channels). An LTS precisely captures the concurrent behaviour of a distributed system — every possible execution path, every interleaving of concurrent components, every deadlock state, every infinite cycle.

CADP's primary input language is LNT (LOTOS New Technology), the modern successor to original LOTOS introduced in the 2000s. LNT combines the process algebra of LOTOS with an imperative functional data language, producing specifications that read like modern programming code while retaining full formal verification semantics:

-- LNT: mutual exclusion with process algebra
-- Verifies: deadlock-freedom + mutual exclusion property
-- Tool: svl (Specification and Verification Language) pipeline

module mutex is

type Bool is false, true end type

process LOCK (in lock: Bool) : bool is
  select
    [lock == false] ->
      return (true)
  []
    [lock == true] ->
      LOCK (lock)
  end select
end process

process PROCESS (id: nat, lock: bool) is
  -- try phase
  lock := LOCK (lock);
  -- critical section
  i_critical_section (id);
  -- release
  lock := false
end process

process SYSTEM is
  var lock: bool := false in
    par
      PROCESS (0, lock)
    ||
      PROCESS (1, lock)
    end par
  end var
end process

end module

The par operator models true concurrency with all interleavings explored; the select operator models nondeterministic choice. CADP's CAESAR compiler translates this to a BCG labeled transition system, which BISIMULATOR and EVALUATOR can then analyse.

The key verification tools in CADP:

CAESAR — the LOTOS/LNT compiler. Translates process algebra specifications to either C source (for on-the-fly verification) or BCG binary files (for explicit-state exploration). CAESAR implements LOTOS's full ISO 8807 semantics and LNT's extended syntax.

CAESAR.ADT — the algebraic data type compiler. Handles LOTOS's type ... is sections and LNT's data types — integers, records, lists, sets — translating them to C code that CAESAR links with the process algebra semantics.

EVALUATOR — the μ-calculus model checker. Verifies properties expressed in the modal μ-calculus (Kozen 1983): a fixed-point logic that subsumes CTL, LTL, CTL*, and most other temporal logics as fragments. EVALUATOR 4 implements an on-the-fly BFS algorithm — it explores the state space only as far as needed to confirm or refute the property, avoiding full state-space generation for many queries.

BISIMULATOR — checks equivalence between two LTS models using various bisimulation relations: strong bisimulation, branching bisimulation (van Glabbeek + Weijland), weak bisimulation, τ.a-bisimulation. Bisimulation is strictly stronger than trace equivalence — it captures branching-time behaviour, distinguishing systems that have the same observable sequences but differ in their decision points. This is the correct equivalence for hardware/software co-design, refinement checking, and component substitution proofs.

REDUCTOR — LTS minimisation by bisimulation. A large system specification may generate a state space of millions of states; REDUCTOR computes the quotient under bisimulation equivalence, collapsing bisimilar states into a single representative. The minimal LTS is equivalent to the original but exponentially smaller — enabling verification that would be infeasible on the raw state space.

DISTRIBUTOR — distributed BFS for state-space generation. When a single workstation's memory is insufficient, DISTRIBUTOR partitions the BFS frontier across multiple machines using a hash function over state labels, enabling state spaces of billions of states to be explored on a compute cluster.

OPEN/CAESAR — the plugin API. Third-party tools can connect to CADP's on-the-fly exploration engine without implementing LOTOS parsing, state encoding, or BFS themselves. EVALUATOR, BISIMULATOR, REDUCTOR, and external tools all use this API — enabling a rich ecosystem of property checkers, performance analysers, and testing tools built on CADP's core.

Hubert Garavel and INRIA Grenoble — 35 Years of EU Verification Infrastructure

INRIA (Institut National de Recherche en Informatique et en Automatique) was founded in 1967 as a national public research institution. It operates under joint authority of the French Ministry of Higher Education and Research and the Ministry of Economy. INRIA's 2,700 researchers across nine centres (Grenoble, Paris, Bordeaux, Lille, Lyon, Nancy, Rennes, Saclay, Sophia Antipolis) represent France's largest concentration of computer science research — and one of Europe's most influential research institutions.

INRIA Grenoble Rhône-Alpes occupies a unique position: the Grenoble technology cluster (Minalogic) hosts Schneider Electric 🇫🇷 (industrial automation), STMicroelectronics 🇮🇹🇫🇷 (semiconductors), Soitec 🇫🇷 (silicon wafers), CEA-Leti 🇫🇷 (microelectronics), and Thales Alenia Space 🇫🇷 — making INRIA Grenoble's formal verification research directly adjacent to the EU's most safety-critical industrial design centres.

Hubert Garavel 🇫🇷 joined INRIA Grenoble in the late 1980s and has led the VASY (Vérification des Architectures et des Systèmes) team — now renamed CONVECS (Construction of Verified Concurrent Systems) — since 1990. His research interests span process algebra, formal specifications, compiler construction, and the engineering of large-scale verification tools. Garavel is the primary author of CAESAR, CAESAR.ADT, BCG format, and the CADP toolbox integration architecture.

The connection to Joseph Sifakis 🇬🇷🇫🇷 is direct: Sifakis co-founded VERIMAG at the Université de Grenoble (later Université Grenoble Alpes) in 1993, adjacent to INRIA Grenoble. Sifakis received the 2007 ACM Turing Award — shared with Edmund Clarke and E. Allen Emerson — specifically for his contributions to model checking. The Grenoble cluster thus concentrated both INRIA's process algebra verification (CADP/Garavel) and VERIMAG's timed systems verification (IF/BIP/Kronos/Sifakis) within the same technology park, producing two complementary EU-native formal verification traditions: CADP for distributed protocol correctness, VERIMAG for real-time system timing properties.

INRIA's intellectual output from Grenoble influenced the international formal methods landscape in multiple directions:

LOTOS → SDL → UML state machines: The LOTOS process algebra semantics shaped ITU-T SDL (Specification and Description Language), which in turn influenced UML 2 state machine and activity diagram semantics — embedded in every model-driven engineering tool in EU aerospace and automotive.
BCG format: The Binary Coded Graphs format became a de facto interchange standard for labeled transition systems, supported by mCRL2 (TU Eindhoven 🇳🇱), LNT/LOTOS converters, and verification tools from INRIA, Edinburgh, and Bordeaux.
OPEN/CAESAR: The plugin architecture influenced subsequent EU verification toolbox designs, including mCRL2's open model checking framework.

The μ-Calculus — The Logic of All Temporal Logics

CADP's EVALUATOR model checker uses the modal μ-calculus — a fixed-point temporal logic introduced by Dexter Kozen at Cornell in 1983 that has a special status in formal verification: it is the minimal modal logic that subsumes all other temporal logics as syntactic fragments.

The μ-calculus is built from:

Modal operators: [a] φ (after any a-step, φ holds) and <a> φ (there exists an a-step after which φ holds)
Fixed-point operators: μX.φ(X) (least fixed point — for reachability, safety with liveness) and νX.φ(X) (greatest fixed point — for invariants, fairness)
Boolean connectives: ∧, ∨, ¬, ⊤, ⊥

The following standard temporal properties are all μ-calculus fragments:

-- CTL AG p (invariant: p holds on all paths, all states)
νX.(p ∧ [true]X)

-- CTL EF p (reachability: there exists a path to a p-state)
μX.(p ∨ <true>X)

-- CTL AF p (inevitability: all paths eventually reach a p-state)
μX.(p ∨ [true]X)

-- LTL G p (globally p on all paths — requires path quantification)
νX.([true]X ∧ [true]p)

-- LTL F p (eventually p on some path)
μX.(p ∨ <true>X)

-- Weak until: p W q (p holds until q, or p holds forever)
νX.((q) ∨ (p ∧ [true]X))

This universality makes μ-calculus model checking strictly more expressive than CTL or LTL alone — and CADP's EVALUATOR is the most mature EU-native implementation. Industrial verification teams that need to express arbitrary combinations of safety, liveness, and fairness conditions — not just the fragments that CTL or LTL support — can specify them directly in μ-calculus without approximation.

Industrial Applications in EU Critical Infrastructure

CADP's deployment record in EU critical infrastructure is unique in the formal verification landscape — almost exclusively French industrial clients, reflecting INRIA Grenoble's proximity to France's safety-critical industrial centres:

Airbus 🇫🇷 — CADP has been used in Airbus programmes for verification of avionics communication protocols, particularly the AFDX (Avionics Full-Duplex Switched Ethernet, ARINC 664 Part 7) network that routes all flight-critical data on the A380 and A350. AFDX's virtual links, traffic shapers, and end-system queuing policies are modelled as communicating LNT processes; EVALUATOR verifies worst-case latency bounds and frame-loss impossibility. DO-178C (DO-333 formal methods credit) at DAL A (highest assurance) requires exhaustive verification of network behaviour — CADP's model checking provides mathematical proof, not statistical confidence.

EDF 🇫🇷 — Électricité de France, the French national electricity company and Europe's largest nuclear power operator, has applied CADP to verification of safety system communication in nuclear reactor instrumentation and control. French nuclear safety is regulated by ASN (Autorité de sûreté nucléaire) under IEC 61508 SIL 4 equivalents. CADP's deadlock-freedom and liveness proofs provide the highest assurance level for reactor protection system (RPS) communication protocols — if a safety trip signal cannot be blocked, delayed indefinitely, or lost under any execution interleaving, CADP can prove it.

Thales Group 🇫🇷 — The French defence, aerospace, and transportation technology company (Thales Avionics, Thales Ground Transportation Systems) has used CADP in multiple EU programmes: avionics protocol verification, railway signalling system verification for EN 50128 SIL 4, and air traffic management protocol verification for EUROCONTROL SESAR (Single European Sky ATM Research). Thales's French engineering teams have direct access to INRIA Grenoble expertise through co-located research agreements.

RATP 🇫🇷 — The Régie Autonome des Transports Parisiens (Paris Metro and RER operator) has applied CADP-based process algebra verification to communication protocols in Paris Metro line automation systems. The METEOR line (Line 14, the world's first fully automated metro line, 1998) and subsequent RATP automated extensions have used formal methods for interlocking and communication protocol verification — CADP's LOTOS-based specification fits naturally with the LOTOS/LOTOS-based industrial standards in European railway signalling.

Orange Labs 🇫🇷 — France Télécom/Orange's research division has used CADP for protocol verification of telecom network management and SDN (Software-Defined Networking) control plane specifications. LOTOS and CADP were originally developed for OSI protocol verification — the telecom connection is direct.

CEA 🇫🇷 — The Commissariat à l'Énergie Atomique et aux Énergies Alternatives (French atomic energy commission) has applied CADP to verification of concurrent safety-critical software components in instrumentation and control systems for both nuclear and renewable energy installations.

EU Research Ecosystem — CADP at the Centre

CADP has been a central tool in EU research funding programmes for three decades:

FP6 AEOLUS (Algorithmic Principles for Building Efficient Overlay Computers): distributed systems verification including CADP applications to P2P network protocols. FP7 HATS (Highly Adaptable and Trustworthy Software using Formal Methods): CADP as verification backend for component-based distributed systems. FP7 CONNECT (Emergent Connectors for Eternal Software Intensive Networked Systems): CADP connector verification for interoperating distributed systems. FP7 SENSATION (Self Energy-supporting Autonomous Computation): embedded system verification. H2020 HEADS (High-performance Embedded Architecture and Design Spaces): CADP for heterogeneous distributed system verification.

The INRIA transfer mechanism brings CADP directly into EU industrial projects: research contracts between INRIA Grenoble and Airbus, EDF, Thales, and Schneider Electric have produced CADP extensions and application methodologies that feed back into the open-source toolbox — creating a virtuous cycle between public research and EU industrial verification practice.

mCRL2 (TU Eindhoven 🇳🇱) acknowledges BCG-format interoperability with CADP, enabling Dutch process algebra verification research to leverage French tooling and vice versa. LNT/LOTOS converters from Edinburgh, Bordeaux, and Nancy extend CADP's reach across EU universities. The FORMATS (Formal Modelling and Analysis of Timed Systems) and TACAS (Tools and Algorithms for Construction and Analysis of Systems) conference series — both EU-hosted — regularly feature CADP-based verification results.

EU AI Act Art. 9 and NIS2 — Process Algebra as Compliance Evidence

CADP's distributed systems focus makes it uniquely relevant to EU AI Act compliance for networked AI systems:

Article 9 Risk Management for high-risk AI systems that operate as networks of agents — multi-agent reinforcement learning, federated learning coordinators, AI pipeline orchestration — requires systematic verification of communication safety. CADP's LNT process algebra can model the communication protocol of a distributed AI system: message passing between agents, coordinator–worker synchronisation, failure-handling protocols. EVALUATOR μ-calculus verification of deadlock-freedom and message-delivery guarantees provides machine-checkable evidence that the AI system's communication substrate meets the systematic verification requirement.

Annex III distributed AI systems: autonomous vehicle coordination protocols, infrastructure management networks, and multi-stakeholder AI decision systems all involve concurrent processes communicating over shared channels — exactly CADP's verification domain. The μ-calculus property νX.([send_critical_message]μY.(<deliver_message>⊤ ∨ <τ>Y) ∧ [true]X) expresses "every send of a critical message is eventually followed by delivery on all execution paths" — a liveness property that neither CTL nor LTL alone can express cleanly, but μ-calculus handles directly.

NIS2 network protocol security: operators of essential services implementing custom network protocols for OT/IT integration (industrial Ethernet, EtherCAT, PROFINET) can use CADP to verify protocol correctness — that no message sequence can cause the protocol to deadlock, lose synchronisation, or enter a security-sensitive state. The OPEN/CAESAR API allows integrating CADP verification into CI/CD pipelines for protocol implementations.

GDPR Art. 5(1)(f) data confidentiality: CADP can model data access control protocols as LNT processes and verify non-interference properties — that low-security processes cannot influence high-security data channels through any sequence of observable events. This is the formal verification counterpart to GDPR's "appropriate technical measures" requirement.

Deploying CADP on sota.io

sota.io is a European PaaS — infrastructure in EU data centres, GDPR-compliant by design, managed PostgreSQL, zero DevOps overhead, and a free tier. For CADP verification workloads, EU infrastructure ensures that both the system specifications being verified (which may contain proprietary protocol or avionics logic) and the verification artefacts (BCG state spaces, counterexample traces) remain within EU jurisdiction — a mandatory requirement for Airbus DO-178C, EDF nuclear safety, and NIS2 critical infrastructure work.

Install CADP (academic licence, free):

# Register at cadp.inria.fr for academic/research licence
# Download for Linux x86-64:
wget https://cadp.inria.fr/distrib/CADP.linux-64.x86_64.tgz
tar xzf CADP.linux-64.x86_64.tgz
source $CADP/com/cadp_env   # sets PATH, CADP_PATH

# Verify installation
caesar.adt --version
evaluator4 --help

Basic LNT verification pipeline:

# 1. Write your LNT specification: mutex.lnt
# 2. Compile to BCG
caesar.adt mutex.lnt 2>&1    # compile data types
caesar -open mutex.lnt       # compile processes to BCG

# 3. Verify μ-calculus property
evaluator4 -diag mutex.bcg \
  '[ true* . "critical_section_0" . true* . "critical_section_1" ] false'
# Property: "there is no path where process 0 and process 1 are simultaneously in critical section"
# (expressed as: the sequence critical_section_0 followed by critical_section_1 is unreachable)

# 4. Check bisimulation equivalence between spec and implementation
bisimulator -strong spec.bcg impl.bcg

# 5. Minimise state space
reductor -branching mutex.bcg mutex_min.bcg
bcg_info mutex_min.bcg   # print minimised LTS statistics

Dockerfile for CI verification:

# Dockerfile: CADP verification in CI pipeline
FROM debian:12-slim

# Install dependencies
RUN apt-get update && apt-get install -y \
    wget curl tar gcc make \
    && rm -rf /var/lib/apt/lists/*

# Copy CADP (pre-downloaded to avoid CI download of licence-protected binary)
COPY cadp/ /opt/cadp/
ENV CADP=/opt/cadp
ENV PATH="$CADP/bin:$PATH"

WORKDIR /workspace
COPY specs/ ./specs/
COPY properties/ ./properties/

# Run verification pipeline
RUN for spec in specs/*.lnt; do \
      name=$(basename $spec .lnt); \
      caesar.adt $spec && \
      caesar -open $spec && \
      for prop in properties/${name}*.mcl; do \
        echo "Checking $prop against $name.bcg..." && \
        evaluator4 -diag ${name}.bcg "$(<$prop)" || \
        (echo "PROPERTY VIOLATION: $prop" && exit 1); \
      done; \
    done
CMD ["echo", "All properties verified"]

SVL (Specification and Verification Language) automation:

% mutex.svl — CADP SVL verification script

% compile specification
"mutex.bcg" = caesar.open "mutex.lnt";

% minimise by branching bisimulation (keeps observable behaviour)
"mutex_min.bcg" = branching minimisation of "mutex.bcg";

% verify mutual exclusion (safety property)
property MUTUAL_EXCLUSION of "mutex_min.bcg"
is
  "No two processes simultaneously in critical section"
  is
  [ true* . 'critical_section_0' . true* . 'critical_section_1' ] false
end property

% verify starvation-freedom (liveness property — LTL fragment in mu-calculus)
property STARVATION_FREE of "mutex_min.bcg"
is
  "Every process that tries eventually enters critical section"
  is
  nu X . ([true]X and [true]<true>true)
  -- (simplified — full starvation-freedom requires fair path quantification)
end property

sota.io free tier (512 MB RAM, 0.5 vCPU) handles CADP verification of small to medium protocol models (≤ 10^6 states, ≤ 10 MB BCG files). Industrial-scale CADP workloads — Airbus AFDX models with millions of states — benefit from the Standard tier (€9/month, 2 GB RAM) or using DISTRIBUTOR across multiple Standard instances.