I'm not sure what exactly you're asking. Would you like to read an in-depth survey of the present state of the art in automated theorem proving and automatic verification? Or are you interested in the fundamental question of why these problems are intractable in the great majority of really interesting cases? The former would require expert input, but the latter mostly boils down to some basic observations from the theory of computation, the foundations of math, and complexity theory.