SafeCap is a modern toolkit for modelling, simulation and formal verification of railway networks, focused on fully-automated scalable safety verification of Solid State Interlocking (SSI) programs – a technology at the heart of many railway signalling solutions worldwide. In this paper, we elaborate on the formal foundations of the employed method by presenting the formal proof semantics of the modelled systems and the properties we are interested in verifying. We discuss the composite nature of this semantics, namely, interrelationships between signalling programs, signalling plan data, and the safety principles we need to ensure. The main focus is to formally justify the derivation of a number of proof obligations that a specific interlocking solution must satisfy. The semantic definitions, properties, and inference rules are formalised with the Coq proof assistant.