"The Verification Theater: When Formal Methods Create False Assurance in Cryptographic Libraries", http://t.cn/AX5u3PdC Symbolic Software发布的一篇论文，发出了一些反向的声音，很有意义。他们发现，声称已经被verified的Cryspen公司的基于Rust的密码学库，有若干漏洞。“形式化验证虽然对其所针对的特定属性具有价值，但必须辅以传统的工程实践，并且必须准确地沟通其实际范围，否则就会沦为一种安全作秀。”