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

TL;DR

This paper addresses the operational resilience of CBDCs, with a focus on offline payments, by arguing that formal verification techniques can provide correctness guarantees where standard testing falls short. It surveys formal-methods foundations (automata, Petri nets, process algebras, logics) and outlines a methodology for modeling, verifying, and prototyping offline CBDC components, emphasizing collaboration with central banks. An illustrative producer–consumer example demonstrates how equivalence and model-checking can certify implementations against a formal specification. The work highlights that while undecidability prevents absolute guarantees, formal methods can substantially reduce risk and improve trust in digital currencies deployed over the Internet.

Abstract

Information and communication technologies are by now employed in most activities, including economics and finance. Despite the extraordinary power of modern computers and the vast amount of available memory, some 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 the information processed by confined systems, with limited socio-economic consequences. In the emerging era of technologies for exchanging digital money and tokenized assets over the Internet, such as in particular central bank digital currencies (CBDCs), 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 computing systems. We advocate their use to validate the operational resilience of software infrastructures enabling CBDCs, with special emphasis on offline payments as they constitute a very critical issue.