Past Meetup

Securify: Automated Formal Verification of Ethereum Smart Contracts

This Meetup is past

113 people went

Location image of event venue


Dear all,
It's my great pleasure to announce a very interesting presentation from two researchers of the ETH Zurich, in a field where progress is dearly needed: Automated Formal Verification of Smart Contracts.

Permissionless blockchains such as Bitcoin and Ethereum have allowed for mutually mistrusting entities to trade and interact, without relying on a trusted third party. Beyond the simple transfer of funds, Turing-complete smart contracts permit the execution of arbitrary code on top of the blockchain. Smart contracts are praised for simplifying many real-world processes due to the ability of being enforced autonomously.

Despite their potential, repeated security concerns have shaken the trust in handling billions of USD in decentralized smart contracts. It has become apparent that writing secure smart contracts is a significant challenge.
Reliable tools are therefore required to guide developers in writing secure contracts as well as to enable contract users to verify the contracts they interact with.

In their talk, Petar Tsankov and Arthur Gervais will present Securify (, the first smart contract checker that provides:

(i) strong security guarantees

(ii) fully automated analysis, and is

(iii) easily extensible to capture new security vulnerabilities.

Securify is capable to verify all execution paths in a given contract, and therefore provides maximum cover. Indeed, Securify discovers security issues in 38% of the smart contracts published on the Ethereum blockchain. For each vulnerable contract, Securify is capable to pinpoint the instructions that may cause security issues and therefore
provides practical and useful guidelines to contract developers. Securify is also easily extensible, allowing to capture new security vulnerabilities as soon as they are discovered.

About the speakers:


Petar Tsankov is a Postdoctoral Researcher at the Software Reliability Lab at ETH Zurich. The goal of his research is to make it easier for developers who are not security experts to build secure and reliable systems. Towards this goal, he combines novel techniques from Program Analysis, Machine
Learning, and Probabilistic Programming to build new practical systems that solve important problems in Information Security.

Petar obtained his PhD and Master's degree from ETH Zurich (Switzerland) and his Bachelor’s degree from at Georgia Tech (USA). For more information on his work visit

Petar’s CV:

Arthur Gervais is a Postdoctoral Researcher in the Institute of Information Security at ETH Zürich, mainly interested in the security and privacy of decentralized ledgers. Arthur will join Imperial College London in October 2017 as Lecturer (equivalent Assistant Professor) and will also be Lecturer
(Dozent) at the Lucerne University of Applied Sciences and Arts (HSLU).
From December 2012 to December 2016, he was working at ETH Zurich on his PhD thesis "On the Security, Performance and Privacy of Proof of Work Blockchains" as well as on Web Privacy. He obtained his Master degrees from KTH Stockholm (Sweden) and Aalto University (Finland) in 2012. Furthermore,
he holds a diplôme d'ingénieur from INSA de Lyon (France) from 2012. His Master's thesis was on the security of industrial control systems [PDF]. His professional website is

Arthur CV: