Devcon Archive logo
Devcon Forum Blog
  • Watch
  • Event
    Event: background logo
    • Devcon 7
    • Devcon 6
    • Devcon 5
    • Devcon 4
    • Devcon 3
    • Devcon 2
    • Devcon 1
    • Devcon 0
  • Categories
    Categories: background logo
    • Cryptoeconomics
    • Devcon
    • Developer Experience
    • Coordination
    • Core Protocol
    • Layer 2s
    • Real World Ethereum
    • Cypherpunk & Privacy
    • Security
    • Applied Cryptography
    • Usability
  • Playlists

Suggested

Loading results..

View all

About Devcon —

Devcon is the Ethereum conference for developers, researchers, thinkers, and makers.

An intensive introduction for new Ethereum explorers, a global family reunion for those already a part of our ecosystem, and a source of energy and creativity for all.

  • Watch
  • Devcon
  • Forum
  • Blog

Get in touch

devcon@ethereum.org

Subscribe to our newsletter

Crafted with passion ❤️ at the Ethereum Foundation

© 2025 — Ethereum Foundation. All Rights Reserved.

devcon 3 / formal verification

  • YouTube
  • IPFS
  • Details

Formal Verification

Duration: 00:25:50

Speaker: Everett Hildenbrandt, Loi Luu, Phil Daian, Reto Trinkler, Yoichi Hirai

Type: Panel

Expertise: Advanced

Event: Devcon

Date: Invalid Date

Phil Daian, Everett Hildenbrandt, Yoichi Hirai, Loi Luu, & Reto Trinkler discuss Formal Verification.

Categories

Developer Infrastructure
  • Related
KEVM: Overview and Progress Report preview
Devcon
Talk
21:35

KEVM: Overview and Progress Report

Since the IC3 Crypto Boot Camp, we have been extending the KEVM semantics in several directions. At the time, we only supported the VMTests from the Ethereum Test Suite, it was somewhat difficult to write properties and proofs about programs in EVM, and EVM-PRIME was a simple demonstrative toy language. This session will cover the progress so far in addressing these issues, as well as our goals and intentions for the semantics moving forward. In particular, we are focused on providing tools to ease the process of writing and proving specifications about programs written in high-level languages. Everett Hildenbrandt is a CS PhD student at University of Illinois Urbana-Champaign studying formal methods and programming languages. He is focused on improving the scalability of symbolic reasoning for applications in both distributed and physical systems. In the context of blockchain systems, he is interested in formalizing the semantics of both the underlying languages used and the consensus protocols. To this end, he recently led the KEVM project which developed an executable mathematical model of the EVM in the K Framework.

Oyente: Development update preview
Devcon
Talk
14:12

Oyente: Development update

Oyente: An Analysis Tool for Smart Contracts. https://github.com/melonproject/oyente

Morphing Smart Contracts with Bamboo preview
Devcon
Talk
19:36

Morphing Smart Contracts with Bamboo

An Ethereum contract language called Bamboo mitigates common mistakes. A Bamboo program textually displays all states and transitions. A program runs always one-pass without loops or functions. Runtime checks never allow reentrant execution. Erlang folks might like the syntax. OCaml people, I need you.

Connecting Decentralized Liquidity preview
Devcon
Talk
22:01

Connecting Decentralized Liquidity

The talk will introduce decentralized liquidity, its role in the ecosystem and how several defi projects are utilising the decentralized liquidity in different ways. The talk will also touch base on what Kyber does to connect different decentralized liquidity sources to make them available for the defi ecosystem.

Making Smart Contracts Smarter - Oyente preview
Devcon
Talk
11:46

Making Smart Contracts Smarter - Oyente

The contract analyzer OYENTE was built to detect vulnerabilities in smart contracts and will soon be released as open source. This presentation will give an overview of Oyente and how it can me used to make smart contracts smarter.

Formal Verification for Solidity preview
Devcon
Talk
19:29

Formal Verification for Solidity

Christian Reitwiessner & Yoichi Hirai speak on Formal Verification for Solidity.

Formal Verification of Smart Contracts preview
Devcon
Other
15:34

Formal Verification of Smart Contracts

Yoichi Hirai gives their talk on Formal Verification of Smart Contracts.

Farcaster frames: building embeddable Ethereum apps preview
Devcon
Workshop
1:24:46

Farcaster frames: building embeddable Ethereum apps

Frames are an open standard for creating embeddable, interactive apps in social media feeds and on the web. They help solve one of the hardest problems for Ethereum dapp developers: distribution. Although frames originated on Farcaster, it's now possible to build cross-platform frames that work on Farcaster, Lens, XMTP, and the open web. In this hands on workshop we'll introduce the core concepts behind frames and build a simple frame app that interacts with a smart contract.

Keynote: Nomic Foundation’s vision for Ethereum’s tooling ecosystem preview
Devcon
Talk
17:35

Keynote: Nomic Foundation’s vision for Ethereum’s tooling ecosystem

Nomic Foundation is the nonprofit behind Hardhat. Nomic’s co-founder and CTO will walk you through Nomic’s long-term vision for a community-driven developer tooling ecosystem for Ethereum.

Blockchain Model Canvas preview
Devcon
Talk
12:36

Blockchain Model Canvas

Blockchain Model Canvas