On the Operational Resilience of CBDC: Threats and Prospects of Formal Validation for Offline Payments
This addresses a critical safety issue for financial systems and stakeholders in the emerging CBDC era, though it is incremental as it applies existing formal methods to a new domain.
The paper tackles the challenge of ensuring software quality in central bank digital currency (CBDC) systems, where minor bugs could cause financial collapse, by advocating the use of formal methods to validate operational resilience, particularly for offline payments.
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.