Devcon Archive logo
Devcon Devconnect Forum Blog
  • Watch
  • Event
    Event: background logo
    • Devcon 7
    • Devcon 6
    • Devcon 5
    • Devcon 4
    • Devcon 3
    • Devcon 2
    • Devcon 1
    • Devcon 0
    • Devconnect ARG
  • 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
  • Devconnect
  • Forum
  • Blog

Get in touch

devcon@ethereum.org

Subscribe to our newsletter

Crafted with passion ❤️ at the Ethereum Foundation

© 2026 — Ethereum Foundation. All Rights Reserved.

devcon8 / bug free solidity coding agents

  • YouTube
Bug-Free Solidity Coding Agents preview
  • Details

Bug-Free Solidity Coding Agents

Duration: NaN:NaN:NaN

Speaker: Mooly Sagiv

Type: Talk

Expertise: Some familiarity with the topic

Event: Devcon

Date: Nov 2026

Aave V4 spokes enable easy deployment of various lending markets, each with different collateral management, risk premiums, liquidations, per reserve risk configuration, and oracle integration, without having to manually manage liquidity. We show how to leverage agents to develop new secure spokes. The core idea is that the user provides an informal definition of correctness for these applications. Our agentic pipeline translates these informal definitions into a formal specification of the application’s safety properties/invariants. Once we have these formal specifications, we can Vibe-code the spoke implementation guardrail with the Certora Prover. The LLM cannot introduce bugs into our generated implementation because the Certora Prover will reject any potential implementation that does not satisfy the formal specification.

Categories

AISecurityFormal Verification