formal-verification

Creusot与Rust形式化验证：基于最弱前置条件演算的自动化验证流水线

探索Creusot如何将Rust所有权系统映射到谓词逻辑，通过最弱前置条件演算构建可落地的形式化验证流水线。