Local-first software manages and processes private data locally while still enabling collaboration between multiple parties connected via partially unreliable networks. Such software typically involves interactions with users and the execution environment (the outside world). The unpredictability of such interactions paired with their decentralized nature make reasoning about the correctness of local-first software a challenging endeavor. Yet, existing solutions to develop local-first software do not provide support for automated safety guarantees and instead expect developers to reason about concurrent interactions in an environment with unreliable network conditions. We propose LoRe, a programming model and compiler that automatically verifies developer-supplied safety properties for local-first applications. LoRe combines the declarative data flow of reactive programming with static analysis and verification techniques to precisely determine concurrent interactions that violate safety invariants and to selectively employ strong consistency through coordination where required. We propose a formalized proof principle and demonstrate how to automate the process in a prototype implementation that outputs verified executable code. Our evaluation shows that LoRe simplifies the development of safe local-first software when compared to state-of-the-art approaches and that verification times are acceptable.

翻译：摘要：本地优先软件在本地管理和处理私有数据，同时仍能通过部分不可靠网络连接的多方之间实现协作。此类软件通常涉及与用户及执行环境（外部世界）的交互。这些交互的不可预测性及其去中心化的特性，使得对本地优先软件正确性的推理成为一项具有挑战性的任务。然而，现有的本地优先软件开发方案并不支持自动化的安全保证，而是期望开发者在网络条件不可靠的环境下推理并发交互。我们提出LoRe，一种编程模型和编译器，能够自动验证开发者提供的本地优先应用的安全属性。LoRe将响应式编程的声明式数据流与静态分析和验证技术相结合，以精确判定违反安全不变量的并发交互，并选择性地通过协调机制在必要时采用强一致性。我们提出形式化的证明原理，并通过原型实现演示如何自动化该过程，输出已验证的可执行代码。评估结果表明，与现有先进方法相比，LoRe简化了安全本地优先软件的开发，且验证时间在可接受范围内。