Functional Safety is a major concern in the design of automation systems today. Many of those systems are realized using PLCs programmed according to IEC 61131-3. PLCopen as IEC 61131 user organization specified a set of software Function Blocks to be used in Safety Applications according to IEC 61508 in 2006. The specification of Technical Committee 5 contains twenty Safety Function Blocks (SFBs) as a library together with some specifications of their use. A second part issued in 2008 demonstrates the use of the defined SFBs in real applications. In the presented work, formal models for the SFBs are derived from the semi-formal specification in the PLCopen documents. Those blocks are verified using model checking and the accordance of their temporal behavior with the PLCopen specification is further validated by simulation. The resulting library of formal models allows to build a formal model of a given safety application - built from SFBs - and to verify its properties. This is demonstrated using an example from the second part of the PLCopen specification.