Авторы 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 бади-аллокатора p KVM. Результаты показывают, что C* поддерживает верификацию широкого подмножества идиом программирования на C и эффективно справляется с сложными задачами рассуждения в реальных сценариях.