CLEARSY uses Claude & B language to validate railway data with AI-fenced pipeline

CLEARSY's ongoing ValidAItion project tackles a critical problem in railway safety: validating ERTMS/ETCS data, a distributed safety-critical system where errors propagate through trackside, onboard, and radio-block centre components. The pipeline integrates the ERTMS Operational Simulator with the CLEARSY Data Solver, applying rules expressed in the B mathematical language—a formal method already trusted in safety certification. Claude, a large language model, authors the rule corpus and parsers via a Model Context Protocol (MCP) server, but every generated proposal is first checked by the downstream formal toolchain and then by systematic human review. This multi-layered approach has already caught a syntactically valid but semantically illegal scenario, demonstrating that formal rules must remain the source of truth.

The paper (submitted to DisCoRail @ISOLA 2026) emphasizes an architectural contribution rather than a new algorithm. Instead of replacing formal methods, it creates a conversational authoring loop where the LLM acts as a “fenced assistant.” The formal oracle (B language rules) disposes; the human confirms. This blueprint for LLM integration in safety-critical systems is a progress report—rule coverage is growing, a human-review campaign is underway, and quantitative results will follow. The work argues that for industrial certification under CENELEC EN 50128/50716, AI can propose but cannot override formal verification, offering a realistic path to leveraging LLMs without undermining safety arguments.