该论文针对密码学软件中的瞬态执行攻击（尤其是Spectre v1）提出了一种基于类型系统的方法，以确保推测性常数时间（Speculative Constant-Time），从而在保持高性能的同时为密码实现提供形式化保证。当前密码库的黄金标准是在高效实现的同时系统性地防御计时攻击，通常借助高保证密码学工具（如Jasmin框架）进行形式化验证。然而，现有工具基于过于简化的执行模型，忽略了瞬态执行产生的微架构泄漏，导致经过验证的实现仍可能受到Spectre等攻击。已有的防御措施往往因性能开销过大而未被实际采用。作者提出了一种值依赖的信息流类型系统，根据执行是否处于错误推测状态动态跟踪安全级别，从而强制实现推测性常数时间属性。该类型系统被集成到Jasmin框架中，并用于保护一个实验密码学库的全部实现，涵盖对称原语、椭圆曲线密码（如X25519）以及Kyber（NIST选定的后量子KEM）。实验结果表明，性能开销极低：Kyber的开销小于1%，X25519几乎为零。这项工作证明了形式化方法可以在不显著牺牲性能的前提下有效缓解瞬态执行攻击。论文的主要贡献包括：提出推测性常数时间的正式定义、设计并实现相应的类型系统、将其集成到Jasmin框架，并通过实际密码库验证其实用性。适合密码学库开发者、系统安全研究员以及形式化验证社区阅读。