Verification of Templated Code in C++

Gregory Malecha, David Swasey, Simon Hudon

C++ templates are used pervasively and a major blocker for applying verification to real code bases. We present an approach to verifying templated code that avoids enlarging the trusted computing base of the C++ semantics. Our approach uses a shallowly embedded logic that enables reasoning about unresolved symbols as hygienic macros. We have applied our approach to verify several small function templates and used their proofs to derive proofs for concrete instantiations of these functions.

rocq c++ program verification separation logic brick templates skylabs-ai

paper conference link talk

@inproceedings{malecha2026-templates,
  title={Verification of {T}emplated {C}ode in {C}++},
  author="Gregory Malecha and David Swasey and Simon Hudon",
  booktitle={Rocq for Programming Languages 2026},
  location={online},
  year="2026",
  month="January"
}