Reducing the Costs of Proof Assistant Based Formal Verification or: Conviction without the Burden of Proof

This thesis considers the challenge of fully formal software verification in the demanding and foundational context of mechanical proof assistants. While this approach offers the strongest guarantees for software correctness, it has traditionally imposed tremendous costs to manually construct proofs. In this work, I explore techniques to mitigate this proof burden through careful system design. In particular, I demonstrate how formal shim verification and extensible compiler techniques can radically reduce the proof burden for realistic implementations of critical modern infrastructure.