Uni-pi: safety, adaptability and resilience in distributed ecosystems, by construction

分布式软件系统在我们社会中的普遍采用，包括物联网、视频会议和社交平台，或去中心化金融和加密货币，正在彻底改变全球数字基础设施和经济的格局。为了避免灾难，即使在不断变化的环境条件、软件升级或意外事件（如故障或服务降级）下，这些系统也必须按预期运行。为了严格保证其预期行为，分布式系统的形式验证至关重要。不幸的是，目前可用的正式模型仅允许隔离地验证某些属性（例如，仅通信安全性、仅适应性），并通过剥离分布式系统的显著特征（例如，无故障、无消息损坏、无延迟）。此外，即使是正式的模型也不能免除其元理论中的错误（例如，证明中的错误），从而导致后续的（新的）理论，这是昂贵的，特别是当理论以编程语言或软件工具实现时。本项目旨在填补这一空白，并开发Uni-pi，第一个基于pi演算和线性/会话类型的统一形式模型，用于验证安全性，适应性和弹性属性，同时在出现故障、消息不一致或服务降级的情况下，保持对分布式软件生态系统的现实看法（我们将在本项目中称之为）。此外，Uni-pi将完全机械化，以获得正确的构造元理论。最后，我们将与行业合作伙伴Actyx和RChain紧密合作，通过知识交流研讨会或技术峰会等参与活动，努力建立新的联系，并根据行业实践和案例研究对Uni-pi进行评估。该项目将为未来新一代主流编程语言、软件工具和分布式生态系统奠定基础，这些语言、软件工具和生态系统安全、适应性强、和弹性，通过构造。

The pervasive adoption of distributed software systems in our society, including Internet of Things, videoconference and social platforms, or decentralised finance and cryptocurrency, is drastically changing the landscape of the global digital infrastructure and economy. To avoid catastrophe, it is imperative that these systems behave as intended, even under constantly changing environmental conditions, software upgrades, or unplanned events, such as failures or service degradation.To obtain rigorous guarantees of their intended behaviour, formal verification of distributed systems is essential. Unfortunately, the formal models currently available only allow verification of some properties in isolation (e.g., only communication safety, only adaptability) and drastically simplify the view of distributed systems by stripping them of salient features (e.g., no failures, no message corruption, no delays). Additionally, even formal models are not exempt from errors in their meta-theory (e.g., errors in proofs), thus leading to subsequent (new) theories, which is costly especially when theories are implemented in programming languages or as software tools.This project aims to fill this gap and develop Uni-pi, the first unified formal model based on the pi-calculus and linear/session types, for the verification of safety, adaptability and resilience properties, while maintaining a realistic view of-what we will call in this project-distributed software ecosystems in the presence of failures, message inconsistencies or service degradation. Furthermore, Uni-pi will be fully mechanised to obtain a correct-by-construction meta-theory. Lastly, we will evaluate Uni-pi against practices and case studies in industry, by working closely with our industrial partners Actyx and RChain and striving to build new connections via the engagement activities, such as Knowledge Exchange Workshops or tech summits.This project will lay the foundations for a new generation of mainstream programming languages, software tools and distributed ecosystems of the future that are safe, adaptable, and resilient, by construction.