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.