Think of them as richer versions of asserts. And in languages where they are first-class parts of the language, that is they become meaningful metadata on functions, variables, classes, etc., then you can end up deriving tests from them or running them through a prover (not always possible, or might restrict you to a subset of the language). They are complementary to the type system and test systems, just like asserts are, but richer in potential than plain asserts. See the recent AdaCore blog post:

https://blog.adacore.com/i-cant-believe-that-i-can-prove-tha...

HN discussion: https://news.ycombinator.com/item?id=31975507