Schimpy.Language for the formal verification of Arduino code. The compiler generates executable Arduino code, as well as models for both the NuSMV model checker and the PRISM model checker which can be used to verify that certain properties on the program hold.