In model checking a formal model of a software system is constructed. That model is verified against a set of properties expressed in some logic. Once a model has been created and verified, it is still necessary to write the application itself completely by hand. No tools have yet been developed that can automatically create a system or application using a model written in Promela. ... until now! The Promela2Java Compiler to be described in this paper is a unique tool transforming a Promela model into an executable Java application. The Promela2Java Compiler has been constructed using the Stratego/XT tool set. Developers can use SPIN to check their designs for certain properties and use the Promela2Java compiler to successfully create executable Java code from their designs.