In this paper, we introduce a formal framework for ensuring the correctness of security patches. We discuss the issues and provide a sketch of how one could implement a system that proves (in many cases) or strongly veri es (in other cases) that a security patch xes a bug, and changes nothing else about the semantics of a program. We make use of an analysis of \bug surfaces" { the set of inputs that trigger a bug, to give a type theoretic characterization of the nonbuggy surface of a program. We thus give credence to the Langsec notion that security aws are often about input handling, and show how formal patch and bug analysis can be used to de ne a more correct input type for a program.