At run time - the language has built in support for assertions (syntax and conciseness way more convenient than C++ et al), contracts pre and post-condition, and you can run a formal logic analyzer on it if you limit yourself to the Spark Ada subset.

Interesting. Thanks! (For a moment I thought the comment had a typo and was actually referring to Agda.)