Verification of a Smart Contract for a Simple Casino

TL;DR

This paper details the automated verification process of a simple casino smart contract using the Whiley language and verification tools, ensuring correctness after fixing initial issues.

Contribution

It introduces a fully automated verification approach for smart contracts using Whiley, Boogie, and Z3, demonstrating its effectiveness on a casino application.

Findings

All smart contract operations verified successfully after fixes.

Identification and correction of specification and code issues.

Verification process is fully automated.

Abstract

We describe the verification of an existing smart contract for a simple casino application, using the Whiley specification and programming language, with a fully automated verification engine based on Boogie and Z3. After finding and fixing several specification and code issues in the smart contract, we are able to verify all the operations of the smart contract.