Spi2Java is a model driven development (MDD) framework to semi-automatically generate Java security protocol implementations from verified Spi Calculus formal specifications of such protocols. The aim of the framework is to provide high correctness confidence on the generated code, thus making a step towards bridging the gap between the verified abstract formal models, and their concrete implementations.
Get more details on the Spi2Java home page.