Formal Land
We develop a solution to formally verify ink! smart contracts (using mathematical methods to check the code at 100%).
Do Your Own Research!
This information has been provided by the owner of the project and has not been verified by the core team of Aleph Zero. Details Verification status Due to the open character of Aleph Zero, anyone can submit projects to the Ecosystem page. The core team of Aleph Zero does not verify the entries, nor can it be held responsible for the success or failure of projects building on top of the network. Being listed on the ecosystem page is not to be understood as an endorsement from the Aleph Zero Foundation or any of the affiliated parties.
About Formal Land
We develop a solution to formally verify ink! smart contracts (using mathematical methods to check the code at 100%).
Our aim is to provide a tool to formally verify ink! smart contracts, that are written in the Rust language. Formal verification is about using mathematical methods to exhaustively safety properties and specifications of a program. This is a key step to ensure the security of critical code such as smart contracts. The formal verification landscape for Rust is still young. We are developing our tool coq-of-rust to verify Rust code
by translation to the proof assistant Coq. This is the technique we used to verify the code of the crypto-currency Tezos, composed of over 100,000 lines of OCaml code. We believe this can scale for the verification of Rust code as well. Our first milestone is to support enough of the Rust language to be able to analyze the ERC-20 implementation given in https://github.com/paritytech/ink/tree/master/integration-tests/erc20
and to prove its safety properties. Next, we want to stabilize our tool to also verify four other examples of ink! smart contracts.
About Formal Land
We develop a solution to formally verify ink! smart contracts (using mathematical methods to check the code at 100%).
Our aim is to provide a tool to formally verify ink! smart contracts, that are written in the Rust language. Formal verification is about using mathematical methods to exhaustively safety properties and specifications of a program. This is a key step to ensure the security of critical code such as smart contracts. The formal verification landscape for Rust is still young. We are developing our tool coq-of-rust to verify Rust code
by translation to the proof assistant Coq. This is the technique we used to verify the code of the crypto-currency Tezos, composed of over 100,000 lines of OCaml code. We believe this can scale for the verification of Rust code as well. Our first milestone is to support enough of the Rust language to be able to analyze the ERC-20 implementation given in https://github.com/paritytech/ink/tree/master/integration-tests/erc20
and to prove its safety properties. Next, we want to stabilize our tool to also verify four other examples of ink! smart contracts.
Do Your Own Research!
This information has been provided by the owner of the project and has not been verified by the core team of Aleph Zero. Details Verification status Due to the open character of Aleph Zero, anyone can submit projects to the Ecosystem page. The core team of Aleph Zero does not verify the entries, nor can it be held responsible for the success or failure of projects building on top of the network. Being listed on the ecosystem page is not to be understood as an endorsement from the Aleph Zero Foundation or any of the affiliated parties.