Paris Métro Line 14

Paris Métro Line 14 is a fully automated subway line in Paris, France, and one of the most significant industrial applications of formal methods in the history of software engineering. The train control system was developed and verified using the B method, with the entire software specification refined through mathematically proven steps from abstract safety requirements to concrete implementation. The project demonstrated that formal verification could scale to real-time, safety-critical infrastructure carrying millions of passengers annually. Line 14 operates without human drivers, relying instead on automated train control, platform screen doors, and centralized traffic management — all verified against formal specifications. The success of the B-method verification on Line 14 influenced subsequent metro automation projects worldwide and remains a primary case study in the argument that formal methods are not merely academic exercises but engineering practices capable of guaranteeing safety at scale. The line's operational history — now spanning decades without a software-related safety incident — is perhaps the strongest empirical argument that mathematical proof, when properly integrated into industrial process, outperforms conventional testing regimes in domains where failure is unacceptable.