Stainless is a tool for verifying mostly functional programs developed by LARA at EPFL. Stainless accepts as its inputs programs in a subset of Scala. Stainless can verify that your program is correct for all inputs and it can also report counterexample inputs for invalid programs. See:
- GitHub Repository and its EPFL GitLab mirror