In his 1900 book The Wonderful Wizard of Oz, L. Frank Baum tells a story that will resonate with any software engineer. A woodman by the name of Nick Chopper suffers a series of workplace accidents. In turn, his arms, legs, body, and even his head are replaced by metal prosthetics. Eventually, what remains is an entirely different man made of tin. Like Baum’s Tin Man, all software projects are repaired and reconfigured, and a project can transform by degrees into something entirely unlike its starting point. As software engineers have long known, this shift of code and specification is the norm. Studies have shown that maintenance consumes the majority of resources in large-scale projects1, and many systems are built on the bones of previous projects. In recent years, many companies have begun to use formal proofs to provide assurance for software. For example, AWS now formally verifies significant portions of its s2n library, which provides cryptographic security for Amazon.com, Alexa, and more. Proofs are used for assurance at Facebook, Google, Intel, Apple, and others. For these companies, proof engineering is software engineering. As software evolves, proofs of that software must evolve in kind. A key method for success at these companies has been a close alignment between proof tools and continuous integration (CI) development environments. This linkage between proofs and code means that edits to the code can be rechecked within seconds in order to re-establish assurance of the software as it changes. However, experience shows this linkage is fragile. Automated tools can often re-establish a proof if code changes are small. But if the code is restructured beyond a certain point, proof tools are typically unable to re-establish a proof of correctness, even if the software contains no defects. Instead, the internal scaffolding of the proof must be rebuilt by hand by a formal methods expert. Consequently, proofs are tended and maintained by embedded proof experts...