Formal Assurance for Railway Signalling: Expanding SAT Proof Checking to Certify Z3’s Inequality-Based SMT Proofs for ERTMS

Source abstract

Abstract Safety-critical railway systems such as Railway interlockings and the European Rail Traffic Management System (ERTMS) require strong, independently checkable guarantees of correctness. This requirement is reinforced by the new standard governing the use of software in the railway domain, EN50716 [18], which firmly promotes formal verification as part of an end-to-end assurance process. Many modern railway verification workflows rely on SMT solvers, such as Z3, to discharge safety properties expressed in propositional logic or its suitable extensions. In this paper, we show how a Z3-based verification toolchain can be extended with proof checking via independent validation of the solver’s output, thereby increasing trust in the overall verification process. To this end, we present a bespoke proof-checking framework for railway verification, capable of handling propositional logic, as well as inequality reasoning based on the Farkas lemma. The latter plays a major role in ERTMS logic, where positioning constraints are often expressed as linear inequalities. We demonstrate the application of the Farkas lemma through a small case study, showcasing the effectiveness of the tool. The methodology developed for handling Farkas certificates can serve as a foundation for incorporating additional SMT reasoning rules. The proof-checking framework has been formally specified in Rocq, with the checker extracted from the formalisation. This approach has been developed together with our industrial partner. It is concise, tailored to their framework, and independent from other larger proof checking mechanisms.