Foundational verification allows programmers to build software which has beenempirically shown to have high levels of assurance in a variety of importantdomains. However, the cost of producing foundationally verified softwareremains prohibitively high for most projects,as it requires significant manualeffort by highly trained experts. In this paper we present Proverbot9001,aproof search system using machine learning techniques to produce proofs ofsoftware correctness in interactive theorem provers. We demonstrateProverbot9001 on the proof obligations from a large practical proof project,theCompCert verified C compiler,and show that it can effectively automate whatwere previously manual proofs,automatically producing proofs for 27.5% oftheorem statements in our test dataset, when combined with solver-basedtooling. Without any additional solvers,we exhibit a proof completion rate thatis a 4X improvement over prior state-of-the-art machine learning models forgenerating proofs in Coq.