Scala, because of its functional nature, already gives us some design tools to write correct programs: type polymorphism, higher-order functions, immutability, and others. There are also many test frameworks that allow us to detect some bugs. This is a good start, but we can do more: proving the absence of bugs. In this talk I will show how to use Isabelle, a proof assistant, to implement algorithms, prove them correct, and compile them as Scala programs. We’ll see how to formulate universal properties on programs and how to check them.