Leon is an automated system for verifying functional Scala programs and finding counter examples to the validity of user-specified properties, based on a new algorithm for solving constraints expressed as functional programs. In our approach, both properties and programs are expressed in the same language, a subset of Scala.

Project Website

Our implementation makes use of the Z3 constraint solver and takes form of a plugin for the Scala compiler. We have used Leon to automatically verify detailed correctness properties for functional data structure implementations, as well as syntax tree manipulations. We have found Leon to be fast for both finding counterexamples and correctness proofs of detailed correctness properties.