Information and communication technologies are by now employed in most activities, including economics and finance. Despite the extraordinary power of modern computers in terms of information processing, storage, retrieval, and transmission, 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 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.
