On the Operational Resilience of CBDC: Threats and Prospects of Formal Validation for Offline Payments

TL;DR

This paper discusses the importance of formal validation methods to ensure the operational resilience of CBDC systems, especially for offline payments, to prevent potential financial crises caused by software bugs.

Contribution

It proposes applying formal methods to validate the correctness of CBDC software infrastructures, focusing on offline payment systems to enhance security and reliability.

Findings

Formal methods can improve confidence in CBDC software correctness.

Offline payment validation is critical for CBDC resilience.

Potential to prevent financial crises due to software bugs.

Abstract

Information and communication technologies are by now employed in most human activities, including economics and finance. Modern computers have reached an extraordinary power in terms of information processing, storage, retrieval, and transmission. However, several results of theoretical computer science imply the impossibility of certifying software quality in general. With the exception of safety-critical systems, this has primarily concerned information processed by confined systems, with limited socio-economic consequences. In the emerging era of technologies for exchanging tokenized assets and digital money over the Internet, such as in particular central bank digital currency (CBDC), even a minor bug could trigger a financial collapse. Although the aforementioned impossibility results cannot be overcome in an absolute sense, there exist formal methods that can provide correctness assertions for software system models under suitable conditions. We advocate their use to validate the operational resilience of software infrastructures enabling CBDC, with special emphasis on offline payments as they constitute a very critical issue.