C*: Unifying Programming and Verification in C

• Despite advances in verification tooling, conventional programmers are rarely involved in the verification of their own code, resulting in higher development and maintenance costs for verified software.
• A key barrier to programmer participation