Symbolic Software公司揭露了Cryspen公司旗下libcrux密码学库中存在的多个安全漏洞和实现缺陷，包括平台相关的密码学故障、HPKE规范中缺失的X25519全零验证、序列号溢出导致的nonce重用、ECDSA签名可延展性以及Ed25519双重钳位等问题。这些问题暴露了形式化验证在实际应用中可能存在的局限性，以及Cryspen公司在信息披露和工程实践方面的问题。
