Comment by 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.