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.

翻译：信息和通信技术如今已广泛应用于包括经济和金融在内的大多数活动中。尽管现代计算机在信息处理、存储、检索和传输方面具有非凡能力，但理论计算机科学的若干成果表明，一般而言无法保证软件质量。除安全关键系统外，这一问题主要涉及封闭系统处理的信息，其社会经济影响有限。在通过互联网交换数字货币和代币化资产的新兴技术时代（尤其是央行数字货币），即使是微小的程序缺陷也可能引发金融崩溃。尽管上述不可能性结果在绝对意义上无法被克服，但存在能够为计算系统提供正确性断言的形式化方法。我们主张运用这些方法来验证支持央行数字货币的软件基础设施的运行韧性，并特别关注离线支付这一关键问题。