2 posts tagged with "Move"

We are continuing our formal verification work for the implementation of the type-checker of the Move language in the 💧 Sui blockchain. We verify a manual translation in the proof system 🐓 Coq of the 🦀 Rust code of the Move checker as available on GitHub.

In this blog post, we present in detail the verification of a particular function AbstractStack::pop_eq_n that manipulates 📚 stacks of types to show that it is equivalent to its naive implementation.

All the code presented here is on our GitHub at github.com/formal-land/coq-of-rust 🧑‍🏫.

In this blog post, we present our project to formally verify the implementation of the type checker for smart contracts of the 💧 Sui blockchain. The Sui blockchain uses the Move language to express smart contracts. This language is implemented in 🦀 Rust and compiles down to the Move bytecode that is loaded in memory when executing the smart contracts.

We will formally verify the part that checks that the bytecode is well-typed, so that when a smart contract is executed it cannot encounter critical errors. The type checker itself is also written in Rust, and we will verify it using the proof assistant Coq 🐓 and our tool coq-of-rust that translates Rust programs to Coq.