Penulis Yiyuan Cao, Jiayi Zhuang, Houjin Chen, Jinkai Fan, Wenbo Xu, Zhiyi Wang, Di Wang, Qinxiang Cao, Yingfei Xiong, Haiyan Zhao, dan Zhenjiang Hu memperkenalkan C*, desain bahasa terintegrasi bukti untuk pemrograman C. C* memperluas C dengan kemampuan verifikasi yang didukung oleh mesin eksekusi simbolik dan kernel bukti bergaya LCF. Ia memungkinkan verifikasi real-time dengan memungkinkan programmer menyisipkan blok kode bukti di samping kode implementasi, memfasilitasi pembaruan interaktif ke status bukti saat ini.

Dukungan bukti yang ekspresif dan extensible-nya memungkinkan pengguna membangun library reusable dari definisi logis, teorema, dan otomatisasi bukti yang dapat diprogram. Pentingnya, C* menyatukan pengembangan kode implementasi dan kode bukti dengan menggunakan C sebagai bahasa umum. Tim mengimplementasikan prototipe dan mengevaluasikannya pada benchmark representatif program C kecil dan studi kasus nyata yang menantang: fungsi attach dari p KVM's buddy allocator.

Hasil menunjukkan bahwa C* mendukung verifikasi subset luas dari idiom pemrograman C dan secara efektif menangani tugas penalaran kompleks dalam skenario dunia nyata.