In the SPARK subset of Ada, the specifications and contracts live alongside your code in the same language, then you can prove that the specs are satisfied. Yo

In the SPARK subset of Ada, the specifications and contracts live alongside your code in the same language, then you can prove that the specs are satisfied. You can also leave out the contracts and just prove absence of behaviors like divide by zero, out-of-bounds array access and integer overflow. Proving that code meets the specification can be really difficult but proving absence of bad behavior is usually a straightforward endeavor.