Thank you for attending TruffleCon 2019!
Feel free to use this scheduler to customize your Truffle experience.
View topics, speakers, time and availability. You can also let us know how each session you attended went so we can make your experience even better! 
Back To Schedule
Friday, August 2 • 1:30pm - 5:00pm
Formal Verification of Smart Contracts Using KEVM

Sign up or log in to save this to your schedule, view media, leave feedback and see who's attending!

Feedback form is now closed.
This workshop introduces the K framework (K), the canonical formal semantics of the Ethereum Virtual Machine (EVM) in K called KEVM, and shows how to use KEVM to formally verify smart contracts at the EVM bytecode level. It also briefly shows how to use KEVM to execute smart contracts in Truffle using the Firefly tool. Our plan is to eventually connect the KEVM verifier with Microsoft's Verisol tool presented in the previous workshop, where the correctness proofs are pushed from high-level Solidity code to low-level EVM bytecode, thus eliminating trust in the Solidity compiler and closing the gap between what is verified and what is executed. Also, through KEVM, we intend to make all the benefits and tools of the K framework available to the users of Truffle.

This session has an attached slide deck.

avatar for Grigore Rosu

Grigore Rosu

CEO, Runtime Verification
Grigore Rosu is a professor in the Department of Computer Science at the University of Illinois at Urbana-Champaign (UIUC), where he leads the Formal Systems Laboratory (FSL), and the president and CEO of Runtime Verification, Inc (RV). His research interests encompass both theoretical... Read More →
avatar for Everett Hildenbrandt

Everett Hildenbrandt

Runtime Verification, Inc.

Friday August 2, 2019 1:30pm - 5:00pm PDT