يقدم المؤلفون Yiyuan Cao، Jiayi Zhuang، Houjin Chen، Jinkai Fan، Wenbo Xu، Zhiyi Wang، Di Wang، Qinxiang Cao، Yingfei Xiong، Haiyan Zhao، و Zhenjiang Hu لغة C*، وهو تصميم لغة مدمج بالإثبات لبرمجة C. يمدد C* لغة C بقدرات التحقق المدعومة بمحرك تنفيذ رمزي ونواة إثبات بأسلوب LCF. يتيح التحقق في الوقت الفعلي من خلال السماح للمبرمجين بتضمين كتل كود الإثبات بجانب كود التنفيذ، مما يسهل التحديثات التفاعلية لحالة الإثبات الحالية. يسمح دعم الإثبات التعبيري والقابل للتوسيع للمستخدمين ببناء مكتبات قابلة لإعادة الاستخدام من التعريفات المنطقية والنظريات وأتمتة الإثبات القابلة للبرمجة. والأهم من ذلك، يوحد C* تطوير كود التنفيذ والإثبات باستخدام C كلغة مشتركة. نفذ الفريق نموذجًا أوليًا وقيمه على معيار تمثيلي لبرامج C صغيرة ودراسة حالة حقيقية صعبة: دالة attach في مخصص الذاكرة buddy الخاص بـ p KVM. تُظهر النتائج أن C* يدعم التحقق من مجموعة واسعة من اصطلاحات برمجة C ويتعامل بفعالية مع مهام الاستدلال المعقدة في السيناريوهات الواقعية.