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.

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