Designing correct replicated data types (RDTs) is challenging because replicas evolve independently and must be merged while preserving application intent. A promising approach is correct-by-construction development in a proof-oriented programming language such as F*, Dafny and Lean, where desired correctness guarantees are specified and checked as the RDTs are implemented. Recent work Neem proposes the use of replication-aware linearizability (RA linearizability) as the correctness condition for state-based CRDTs and mergeable replicated data types (MRDTs), with automation in the SMT-aided, proof-oriented programming language F*. However, SMT-centric workflows can be opaque when automation fails to discharge a verification condition (VC), and they enlarge the trusted computing base (TCB). We present Sal, a multi-modal workflow to design and verify state-based CRDTs and MRDTs in Lean. Sal combines (i) kernel-checkable automation with proof reconstruction, (ii) SMT-aided automation when needed, and (iii) AI-assisted interactive theorem proving for remaining proof obligations. When a verification condition is shown to be invalid, we leverage Lean's property-based testing to automatically generate and visualize counterexamples, helping developers debug incorrect specifications or implementations. We report on our experience verifying a suite of 13 CRDTs and MRDTs with Sal: 69% of verification conditions are discharged by kernel-verified automation without SMT, and counterexamples automatically expose subtle bugs such as the well-known enable-wins flag anomaly. The codebase for Sal is open-sourced, and is available at \href{https://github.com/fplaunchpad/sal}{https://github.com/fplaunchpad/sal}

翻译：设计正确的复制数据类型（RDT）具有挑战性，因为副本独立演化，必须在保留应用意图的前提下进行合并。一种有前景的方法是在面向证明的编程语言（如F*、Dafny和Lean）中进行“正确性通过构造保证”的开发，在实现RDT的同时指定并检查所需的正确性保证。近期工作Neem提出将“复制感知线性化”（RA线性化）作为基于状态的CRDT和可合并复制数据类型（MRDT）的正确性条件，并在基于SMT辅助、面向证明的编程语言F*中实现自动化。然而，当自动化无法完成验证条件（VC）的消解时，以SMT为中心的工作流可能不够透明，并且会扩大可信计算基（TCB）。我们提出Sal，一种在Lean中设计和验证基于状态的CRDT和MRDT的多模态工作流。Sal结合了（i）带证明重构的内核可检查自动化、（ii）必要时基于SMT辅助的自动化，以及（iii）针对剩余证明义务的AI辅助交互式定理证明。当验证条件被证明无效时，我们利用Lean的基于属性的测试自动生成并可视化反例，帮助开发者调试错误规范或实现。我们报告了使用Sal验证13个CRDT和MRDT套件的经验：69%的验证条件由内核验证的自动化（无需SMT）消解，反例自动暴露了细微错误，例如著名的“enable-wins标志异常”。Sal的代码库已开源，地址为\href{https://github.com/fplaunchpad/sal}{https://github.com/fplaunchpad/sal}。