Each planning phase of ETCS-compliant railway tracks at Deutsche Bahn (DB) prescribes a concluding review, now performed by manually inspecting printed diagrams and tables. This is time-consuming and bears the risk to overlook critical mistakes. We present a concept and a tool for fully automated formal verification of railway plannings against ETCS planning rules. The approach is based on a modular translation of track models, as well as planning rules, to the SMT-LIB language understood by Satisfiability Modulo Theories (SMT) solvers, which are used as a backend. Track models are assumed to be available in the standardized object-oriented PlanPro format and are automatically translated to SMT-LIB constraints. The planning rules themselves are given in natural language in rule books and cannot be translated automatically. Instead, we provide a translation schema that lets a planning engineer render planning rules almost one-to-one as first-order formulas. No specific knowledge of logic or SMT solver internals is required to perform this task, and it is sufficient to do it once and for all for each planning rule. Subsequent verification of a track model against a planning rule is fully automatic. Deviations are visually highlighted for manual inspection. To this end, we integrated rule verification with an existing track visualization tool into a GUI. Our approach was evaluated with real DB infrastructure data, showing that it is easy to use and sufficiently powerful to be integrated into existing planning workflows.