David Crocker's Verification Blog

In June 2025 the ISO C++ standards committee voted to include function contracts in C++26. At the time of writing this, the latest draft specification is N5014 which includes the syntax and semantics of the support for contracts.

This post will compare the C++26 syntax with the syntax used by Escher C/C++ Verifier (eCv), examine how easily we can extend eCv to handle the C++26 syntax, and compare the strengths and weaknesses of the C++26 support for contracts with eCv from the perspective of compile-time verification.