The Confidential Consortium Framework (CCF) is an open-source platform for developing trustworthy and reliable cloud applications. CCF powers Microsoft's Azure Confidential Ledger service and as such it is vital to build confidence in the correctness of CCF's design and implementation. This paper reports our experiences applying smart casual verification to validate the correctness of CCF's novel distributed protocols, focusing on its unique distributed consensus protocol and its custom client consistency model. We use the term smart casual verification to describe our hybrid approach, which combines the rigor of formal specification and model checking with the pragmatism of automated testing, in our case binding the formal specification in TLA+ to the C++ implementation. While traditional formal methods approaches require substantial buy-in and are often one-off efforts by domain experts, we have integrated our smart casual verification approach into CCF's CI pipeline, allowing contributors to continuously validate CCF as it evolves. We describe the challenges we faced in applying smart casual verification to a complex existing codebase and how we overcame them to find six subtle bugs in the design and implementation before they could impact production

翻译：机密联盟框架（CCF）是一个用于开发可信赖云应用的开源平台。CCF支撑着微软Azure机密账本服务，因此建立对其设计与实现正确性的信心至关重要。本文报告了我们应用智能非正式验证方法来验证CCF新型分布式协议正确性的经验，重点关注其独特的分布式共识协议和定制客户端一致性模型。我们使用"智能非正式验证"这一术语来描述我们的混合方法——该方法将形式化规范与模型检查的严谨性，同自动化测试的实用性相结合，在我们的案例中体现为将TLA+形式化规范与C++实现相绑定。传统形式化方法需要大量专业投入且通常由领域专家进行一次性验证，而我们将智能非正式验证方法集成到CCF的持续集成流水线中，使贡献者能够在CCF演进过程中持续进行验证。我们阐述了在复杂现有代码库中应用智能非正式验证所面临的挑战，以及我们如何克服这些挑战，在影响生产环境之前发现了设计与实现中的六个微妙缺陷。