Automatic software verifiers have an ambitious goal: quick formal verification of software, without the need for specialised proof tools. While incredibly successful, these verifiers are still unable to automatically verify complex real-world programs. These programs require proofs that are simply beyond the capability of automated reasoning. Existing verifiers allow users to manually prove select verification goals when the automatic tools fail; however, these manual proofs use complex logics and translations that do not resemble the source program. In this talk we outline the limitations of current software verifiers and propose new techniques to enable interactive proofs at the abstraction level of the source program. These techniques should allow interactive proofs to be completed more easily when an automatic verifier fails.