[alpaylan]

You cannot escape from the human verifying the properties you want verified mechanically. This only gives you leverage in specific scenarios where specification is much simpler than the implementation.