sota.io
2026-04-08·9 min read·sota.io team

RATP Line 14 and B-Method: 26 Years of Formally Verified Metro Software in Paris (1998–2026)

On October 15, 1998, the first Météor train rolled out of Madeleine station and into service on the Paris Métro. Line 14 was the first new Paris metro line in decades. It was also the world's first fully automated urban rail line where the Automatic Train Protection (ATP) software was formally verified using mathematical proof.

That proof was produced using B-Method. The tool was Atelier B, developed by ClearSy, a company based in Aix-en-Provence, France. The mathematician behind the method was Jean-Raymond Abrial, a French computer scientist who had spent the 1980s developing a way to write software specifications that could be mechanically checked for consistency and correctness.

Twenty-six years later, Line 14 is still running.

What B-Method Is

B-Method is a formal specification method for writing software as a sequence of abstract machines — mathematical objects with a state space, invariants, and operations that must preserve those invariants. You specify what a system must do in a language called Abstract Machine Notation (AMN). Then you prove — mechanically, with a tool — that your implementation satisfies your specification.

The key output is a proof obligation: a mathematical statement that says, in effect, "if the preconditions hold, the postconditions will hold after this operation." Atelier B generates these obligations automatically. Provers discharge them automatically where they can, and flag the ones that require human attention.

What you end up with is not just software. You end up with software whose correctness is a theorem — not a confidence level, not test coverage, but a proof.

Jean-Raymond Abrial developed B-Method at Programming Research Group at Oxford (he was French, working in Oxford), then at INRIA in France, and published the foundational text The B-Book: Assigning Programs to Meanings in 1996. Two years later, ClearSy applied it to the most visible safety-critical software deployment in Europe.

The Line 14 Application

The ATP software that ClearSy formally verified for Line 14 is the system that prevents trains from colliding with each other or with fixed obstacles. In a fully automated metro — no driver on the train — this software is the only thing between normal operation and catastrophic failure.

The formal verification covered approximately 86,000 lines of B specification, generating roughly 27,000 proof obligations. All were discharged before the software went into service.

This is not a metaphor for "very well tested." The word "proof" has a specific technical meaning here: the same meaning it has in mathematics. The software cannot violate its specified safety invariants unless the specification itself is wrong. Provided the formal model accurately captures the physical system — which is the remaining engineering challenge — the software is correct.

The size of this effort was significant. ClearSy employed a team of engineers over several years to produce the specification, generate the proof obligations, and discharge them. This was not fast or cheap. But for infrastructure carrying hundreds of thousands of passengers per day, the economics are different.

26 Years in Production

Line 14 has been extended three times since the 1998 opening — in 2003 (Bibliothèque François Mitterrand to Olympiades), in 2007 (Saint-Lazare direction), and most recently in 2024 as part of the Grand Paris Express project, connecting to Saint-Denis Pleyel ahead of the Olympic Games. Each extension required updating the ATP software and re-verifying the new system state.

This is the underappreciated reality of formal verification in long-lived infrastructure: you do not prove correctness once and walk away. The proof is attached to a specific specification of a specific system at a specific point in time. When the system changes — new stations, new trains, new routes — the specification must be updated and the proof obligations must be re-discharged.

ClearSy has done this for each Line 14 extension. They have also applied the B-Method approach to other RATP lines. Lines 1 and 4 were automated between 2012 and 2022 using similar safety verification approaches. The Grand Paris Express lines (15, 16, 17, 18) — all being built between 2024 and 2030 — use formal verification for ATP systems throughout.

The 1998 decision to use formal verification was not a one-time experiment. It established a methodology that RATP and its suppliers have continued to use and build on for more than two decades.

Why Systems Get Replaced (And What That Means)

A question worth asking: if the formally verified software from 1998 was correct, why has any of it been replaced?

The answer is not "because it had bugs." The answer is capacity, communications protocols, and new system capabilities.

Line 14 originally used a train control system built around the verification that existed in 1998. When RATP moved toward CBTC (Communications-Based Train Control) — a more modern radio-based approach that allows shorter headways and higher throughput — they needed to re-specify and re-verify the control software against the new architecture. The old proofs did not cover the new system; the new system had different invariants, different communication patterns, different failure modes.

This is formally correct behavior. Formal verification proves that software meets a specification. When the specification changes — because the system design changes — you need new proofs for the new specification. The old proofs are still valid. They just prove something about a system that no longer exists.

This is a feature, not a failure. The process of updating the formal specification forces engineers to precisely define what the new system must do before building it. The new proofs then confirm it. The transition from old to new is itself subject to formal methods discipline.

No line was ever taken out of service because the formally verified software failed to meet its specification.

The EU Geography of Railway Formal Verification

Something worth noticing: almost every major actor in European railway formal verification is based in France or Germany.

ClearSy — Aix-en-Provence, France. B-Method tooling, Atelier B, ATP software for RATP, SNCF, and others. Founded by engineers from Systerel, which was the original team that did the Line 14 work. Still the dominant B-Method tooling vendor in Europe.

Alstom — Saint-Ouen, France (headquarters). One of the largest railway equipment manufacturers in the world. Uses formal methods internally for safety-critical systems. Built the Météor rolling stock for Line 14.

Siemens Mobility — Munich, Germany. Major CBTC vendor for metro systems across Europe. Uses formal verification approaches for safety cases, particularly in the German railway domain.

SNCF — Paris, France. Uses B-Method for signaling software across French national rail. Has an internal formal methods competency.

Systerel — Aix-en-Provence, France. Safety-critical software company, spun out from the Line 14 team. Applies formal methods to railway and aerospace software.

Esterel Technologies — Toulouse, France (now part of ANSYS). Developed the SCADE tool suite, widely used for safety-critical embedded software in aerospace and rail.

This concentration is not accidental. French engineering education — Grandes Écoles, INRIA — produced generations of computer scientists with deep exposure to formal methods. The same tradition that gave Europe CompCert (Xavier Leroy, INRIA Paris), Coq/Rocq (INRIA Sophia-Antipolis), and Why3 (INRIA Saclay) also gave it ClearSy, Systerel, and the techniques that keep Paris trains running.

Germany adds Siemens, TU Munich (AutoCorres, CPAchecker), and a safety-critical embedded tradition reaching back to automotive (MISRA, SPARK Ada via AdaCore Paris). The two countries together represent the spine of EU safety-critical software.

What Developers Working in EU Infrastructure Should Know

If you are building software that touches safety-critical systems — medical devices, autonomous vehicles, rail signaling, aerospace — and you are deploying in Europe, your supply chain of tools is mostly French and German. Atelier B runs in France. SCADE is from France. CompCert (the formally verified C compiler used in safety-critical paths) is INRIA France. CPAchecker is TU Munich.

The data these tools process — specifications, proof artifacts, model parameters — stays in your infrastructure. If that infrastructure is running on US-incorporated cloud providers, you have CLOUD Act exposure on your proof artifacts. For safety cases submitted to railway authorities or aviation certification bodies, the provenance and integrity of those artifacts matters.

EU AI Act Article 9 is not the only European regulation that creates an infrastructure jurisdiction question. Railway safety regulation (EN 50128, IEC 62279) and aviation certification (DO-178C, EASA standards) have similar requirements for artifact integrity and supply chain control.

EU-native infrastructure is not a nice-to-have for developers working in this space. It is the same supply-chain logic that French engineers applied to Line 14 in 1998: if you want to know your proofs are intact, you need to control where they live.

Practical Implications

B-Method is still used. ClearSy continues to develop Atelier B. The Grand Paris Express lines use it. If you work in railway safety software in Europe, B-Method literacy is not historical knowledge — it is current practice.

Formal verification scales to production. Line 14's 27,000 proof obligations discharged over a multi-year effort is the existence proof that formal verification is not just academic. It works in software that carries 200,000 passengers per day.

Systems change; proofs don't invalidate themselves. The 1998 proofs remain valid. What changed is that the system they describe was extended. That is expected behavior. The cost of extension is re-verification, which ClearSy has done for every Line 14 change since 1998.

The EU formal methods ecosystem is deep. CRA 2027, EU AI Act August 2026, EN 50128 — European regulations are increasingly creating formal requirements for software correctness proofs. The ecosystem to meet those requirements was built over the last 30 years. Much of it is within a few kilometers of Toulouse, Aix-en-Provence, and Munich.

Further reading from this series:

Deploy your safety-critical tools and verified software on EU-native infrastructure with sota.io — hosted in Europe, operated under EU law, GDPR-compliant.