This paper describes formalization of interlocking safety requirements and automatic verification of interlocking functional specification. Safety requirements of interlocking are expressed by sub-routes. In this approach, functional specifications of interlocking machines are translated to intermediate specifications expressed by sub-routes and automatically verified by a proof checker.