Formal methods · Ethereum

Seulkee
Baek

I am the maintainer of Jaune and Blanc—two open-source projects exploring how executable specifications and interactive theorem proving can make Ethereum smart contracts more trustworthy.

Selected work

01 / Selected work

Making the EVM
easier to trust.

Jaune

Executable formal specification

An executable formal specification of the Ethereum Virtual Machine, implemented entirely in Lean 4 and tested against Ethereum’s official execution test suite.

Lean 4
EVM
Formal semantics

Source on GitHub

Blanc

Minimal EVM language

A low-level EVM programming language designed for interactive verification, with a Lean 4 toolchain and proofs about the bytecode that actually runs.

Lean 4
Smart contracts
Verification

Source on GitHub

02 / About

Research at the edge of
proof and execution.

I’m an independent researcher working on formal methods for crypto, with a current focus on verifying EVM smart contracts through interactive theorem proving.

My earlier work includes proof formats for automated reasoning tools and automation tactics for theorem provers. I work mainly in Lean, with experience in Coq, SAT solvers, and first-order automated theorem proving.

03 / Contact

Let’s compare notes.

seulkeebaek@gmail.com

SeulkeeBaek