Skip to main content

2 posts tagged with "Move"

View All Tags

Β· 8 min read

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 πŸ§‘β€πŸ«.

Β· 3 min read

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.