Every formal verification depends highly on requirements. It's pretty easy to make a mistake in defining the task itself. In the end, you'd want to verify system behavior in real world, and it's impossible to completely define real world. You always make some assumptions/models to reason within, and it impossible to verify the assumptions are correct.