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.

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