Stainless [0] does this well for Scala. You augment function definitions and return statements with `require()` and `assert()` respectivley.

[0] https://stainless.epfl.ch/