The Leon system aims to help developers build verified Scala software. It encourages using a small set of core Scala features, but provides unique automation functionality. In particular, Leon can

• verify statically that your program confirms to a given specification and that it cannot crash at run-time
• repair a program for you to ensure that the above holds
• automatically execute and synthesize working functions from partial input/output specifications and test cases.

[http://leon.epfl.ch/doc/intro.html Link to the documentation]