This paper demonstrates the use of formal methods to verify the correctness of safety controllers. PLCopen organization specified Function Block software models to be used in Programmable Controllers. Based on these specified semi-formal models, we develop formal models for implementation. On both levels, a verification of the specified properties is applied to the models using different model checking techniques and tools (Uppaal on model level and [mc]square on code level). The paper shows how the two levels interact and demonstrates that, by using the presented method, unclarities especially margin of interpretation in the semi-formal specification can be uncovered. The approach is demonstrated using the emergency stop function block as an example.