As the practice of formally verifying software in proof assistants increases in importance and popularity, the lack of proper support for large-scale proof engineering is becoming increasingly apparent. In particular, the productivity of proof engineers is lowered by inadequate interfaces, processes, and tool support, which lone expert users may not be hindered by, but become serious problems in large evolving projects with many contributors. Traditional software engineering practices fail to carry over in a unique setting that mixes formal requirements with rigorous mathematical proofs, and powerful reasoning capabilities with limited computational support. This project aims to increase the productivity of proof engineers by simplifying the process of developing, executing, and maintaining verified software in proof assistants, leveraging synthesis and testing based approaches to facilitate proof construction, extraction, and maintenance, as well as to establish the trustworthiness of proof checkers themselves.