Stainless

Verification framework for a subset of the Scala programming language

Stainless is a tool for verifying Scala programs developed by the LARA. It can verify that your program is correct for all inputs, it can report inputs for which your program fails when they exist, and it can prove that functions do not loop.