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 continuous integration 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 subtle bugs in the design and implementation before they could impact production.

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