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.

devcon 5 / grantee expose lightning talk 1 formality an efficient proof language

  • YouTube
  • IPFS
  • Details

Grantee Exposé Lightning Talk 1 - Formality: An efficient proof language

Duration: 00:10:20

Speaker: John Burnham

Type: Talk

Expertise: Intermediate

Event: Devcon

Date: Jul 2026

Formality is a dependently-typed functional programming language similar to Agda that compiles to a non-garbage-collected, parallel runtime based on interaction combinators and Lamping's optimal reduction algorithm. The language is suitable both as a formal proof language as well as a fast low-level systems language, which allows it to be used to write verifiably secure software at every level of the stack, from hardware drivers to smart contracts and everything in between. Formal proofs are of particular interest for smart contracts applications, given that they often have large amounts of capital depending on the safety of relatively small code bases.

Categories

Securityprogrammingruntimeproofsecuritygeneral