Marco Eilers

• 2026

  Our paper Towards Cross-Language Verification between Python and C has been accepted in the SpecifyThis track at ISoLA 2026.

• 2026

  I am on the program committee of OOPSLA 2027.

• 2026

  I will give a talk at HYPER 2026.

• 2026

  Our paper Modular Reasoning about Object Relations has been accepted at CAV 2026 and is available here.

• 2026

  I am on the program committee of FMCAD 2026.

• 2026

  I am on the program committee of CCS 2026.

• 2026

  Won second-best team at the VerifyThis 2026 verification competition, together with Jonáš Fiala.

• 2025

  Protocols to Code: Formal Verification of a Secure Next-Generation Internet Router appeared at CCS 2025, where it received a Distinguished Artifact Award.

What I work on

I design verification techniques and build the tools that put them to work, spanning everyday programming languages, security properties that relate multiple executions, and safety-critical systems from internet routers to smart contracts.

Nagini

An automated, deductive verifier for statically typed Python programs. Nagini proves memory safety, absence of runtime errors, and rich functional, progress and information flow properties of real Python code. I lead its development.

Code Nagini, CAV 2018

IF

Information Flow & Hyperproperties

Techniques to prove that programs do not leak secret information, and more generally to verify hyperproperties relating multiple executions. I design techniques that let standard verification tools check hyperproperties via modular product programs and extend them to concurrent programs (CommCSL).

CommCSL, PLDI 2023 Modular Product Programs, TOPLAS 2020 Product Programs in the Wild, CAV 2021

Viper

A verification infrastructure for permission-based reasoning developed at ETH Zurich. Its intermediate language and back-end verifiers are the foundation of tools like Nagini, 2vyper, Prusti, Gobra and VerCors. I have been one of its main developers since 2022.

Project Try online Fifteen Years of Viper, CAV 2025

Full-stack verification of the SCION next-generation internet architecture. Using Viper-based tools, we prove safety and security properties of the production Go implementation of the SCION router — from protocol models all the way down to running code.

Project Code Protocols to Code, CCS 2025 ★

Smart Contract Verification

Specifying and verifying rich functional and security properties of Ethereum smart contracts. The 2vyper tool verifies contracts written in Vyper against expressive, resource-style specifications that capture properties beyond conventional contract analyzers.

Code Rich Specifications, OOPSLA 2021 ★

Selected publications

A full and up-to-date list is available on DBLP and Google Scholar.

Awards & honors

• 2026

  Second-best team, VerifyThis 2026 verification competition (with Jonáš Fiala).

• 2025

  Distinguished Artifact Award, CCS 2025 CCS ★
  for Protocols to Code: Formal Verification of a Secure Next-Generation Internet Router.

• 2023

  Best team, VerifyThis 2023 verification competition (with Alexander J. Summers).

• 2022

  ETH Medal ETH ★ for an outstanding doctoral thesis, ETH Zurich.

• 2021

  Distinguished Artifact Award, OOPSLA 2021 OOPSLA ★
  for Rich Specifications for Ethereum Smart Contract Verification.

• 2021

  Best student team, second place, VerifyThis 2021 (with Vytautas Astrauskas).

• 2018

  Best Paper Award nomination, ESOP 2018, for Modular Product Programs.

• 2011

  Best student in Business Information Systems (2008 cohort), Berlin School of Economics and Law.

• 2008

  DMV-Abiturpreis, awarded by the Deutsche Mathematiker-Vereinigung.

Selected talks and posters

• Jan 2026

  Protocols to Code: Formal Verification of a Secure Next-Generation Internet Router (poster) · Dagstuhl seminar “Software Contracts Meet System Contracts”

• Oct 2025

  Modular Reasoning about Global Variables and Their Initialization · OOPSLA, Singapore

• Jul 2025

  Fifteen Years of Viper · CAV, Zagreb

• Jul 2024

  Verification Algorithms for Automated Separation Logic Verifiers · CAV, Montreal

• Jul 2024

  VerifiedSCION: Verified Secure Routing · FRIDA workshop, Montreal

• Mar 2024

  Resource-Based Specifications for Smart Contracts · Lorentz Center, Leiden

• Sep 2023

  Proving Python code correct with Nagini · Swiss Python Summit, Rapperswil

• Jun 2023

  CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity · PLDI, Orlando

Teaching & supervision

As lecturer at ETH Zurich:

• Spring 2023–26

  Lecturer · Program Verification (MSc), every spring semester

I have also been a teaching assistant for MSc and BSc courses including Concepts of Object-Oriented Programming, Software Architecture & Engineering, Rigorous Software Engineering and Computer Science I.

Student supervision

I have supervised more than 30 Master’s and Bachelor’s theses, internships and research projects. A selection:

• 2025–26

  Luca Schafroth, MSc · Formally Verified ASN.1 Python Encoders and Decoders · Report

• 2025

  Nicolas Kaletsch, MSc · Verification of Information Flow Security in the Presence of Unverified Code · Report

• 2024–25

  Markus Limbeck, MSc · Enhancing Deductive Verification of Unbounded Heap Data Structures · Report

• 2024–25

  Etienne Birling, MSc · Cross-Language Verification of Python Modules Written in C · Report

• 2023–24

  Frédéric Necker, MSc · Verification of Object Invariants in the Presence of Unverified Code · Report

• 2020

  Christian Bräm, MSc · Verification of Advanced Properties for Real World Vyper Contracts · Report