search

formal-land / coq-of-rust

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦
GNU Affero General Public License v3.0
418 stars 14 forks source link

Move - Simulations - Verifier - TypeSafetyChecker #572

Closed clarus closed 3 months ago

clarus commented 4 months ago

Write a simulation for the type TypeSafetyChecker and its impl in https://github.com/move-language/move-sui/blob/main/crates/move-bytecode-verifier/src/type_safety.rs

InfiniteEchoes commented 3 months ago

Done in #578 .