Formal Verification of Smart Contracts - Ethereum Engineering

FormalVerification_Ethereum_Part1.txt

References 
https://github.com/pirapira/evmverif
https://yoichihirai.com/edcon-yoichi-hirai.pdf

Proof Checkers

Kepler Conjecture

Testing shows the presence, not the absence of bugs - E.W. Dijkstra



Verification of EVM Bytecodes

EVM definition in Lem
EVM definition in Ocaml
EVM definition in Isabelle

formal conditions of Solidity smart contracts can be automatically verified 
even in the presence of potential re-entrant calls from other contracts.

Desirable Contract Properties

Only this kind of callers can alter the storage
Only this kind of callers can decrease the balance
The invalid opcode is never hit
Bidding honestly should be the dominant strategy

Addendum

Smart Contracts can be perceived as counter party risks
Every smart contract has a program counter
Reentrancy as an annoyance for formal methods
Transactions are constructed as function calls
Transactons can carry additional data in the form of argumentss
Contracts may also use non-volatile storage and log events
Ethereum addresses can refer indistingushably to a contract or a user public key
There is no distinction between transactions and method calls
Theree main types of declarations within a contract are type declarations, property declarations and methods