Formal Verification of Smart Contracts with the th2 Automation Framework

This demo showcases a solution for the formal verification of smart contracts written in Solidity, implemented with the use of the th2 automation framework. 

We apply our approach to a smart contract which automates ERC-721 non-fungible token management for the NFT marketplace launched on the P8 platform. P8 has been developed by Yaala Labs – a technology firm specialising in building mission-critical applications for global financial markets.

Watch more Exactpro demos displayed at Consensus 2022:
th2 Implementation for Reconciliation Testing of the P8 Marketplace Platform by Yaala Labs
P8 NFT Marketplace Functional Testing with the th2 Automation Framework
CBDC Sandbox Testing