PLDI 24
Steffen Smolka
Staff Software Engineer at Google, building the network infrastructure enabling AI at scale. I bring a programming languages and formal methods background to planet-scale systems — delivering tools that enable velocity through reliability, rather than trading one for the other.
Programming Languages
AI Infrastructure
Network Verification
Formal Methods
Compilers
Tools
01 Overview
At Google, I founded and lead ARCNET (Automated Reasoning and Contracts for Networking) — a team applying formal methods, AI, and domain-specific languages to make Google's data center networks fast and easy to program, evolve, reason about, and get right. Watch this recent talk to get a taste.
I have a theory and research background that I've found surprisingly useful on the applied side. At Cornell, I did a PhD with Nate Foster on language-theoretic foundations for network programming and verification — NetKAT, ProbNetKAT, and GKAT — and built compilers and verifiers.
02 Experience
Staff Software Engineer (L6) · Network Infrastructure · Sunnyvale, CA
Founded and leads ARCNET — formal methods and AI for network velocity and reliability at hyperscale.
Member, Technical Steering Committee · Co-Chair, P4 API Working Group
Engineering Intern · Sunnyvale, CA
Built and shipped a network analysis tool — patented and launched as Network Intelligence Center.
Visiting Researcher · Host: Alexandra Silva
Researched decision procedures for probabilistic programs.
Intern · Palo Alto, CA
P4 data plane programming and verification — contributed to a data plane verification patent.
Research Intern · Host: Dimitrios Vytiniotis · Cambridge, UK
Designed and implemented a parallelizing compiler for Ziria, a domain-specific language for software-defined radio.
03 Publications
SIGCOMM 22
Guarded Kleene Algebra with Tests:
Verification of Uninterpreted Programs in Nearly Linear Time
POPL 20
Proof Carrying Network Code
CCS 19
Scalable Verification of Probabilistic Networks
PLDI 19
Performance Annotations for Cloud Computing
HotCloud 17
Cantor Meets Scott: Semantic Foundations for Probabilistic Networks
POPL 17
A Fast Compiler for NetKAT
ICFP 15
Semi-intelligible Isar Proofs from Machine-Generated Proofs
JAR 15
PxTP 13
04 Patents
Cloud Network Reachability Analysis for Virtual Private Clouds
2024
Data Plane Program Verification
2023
05 Talks
P4-Based Automated Reasoning (P4‑BAR) for the (Networking) Masses!
More talks on YouTube
Conference presentations from PLDI, POPL, ICFP, and SIGCOMM. Slide decks linked in the publications section above.
06 Selected Honors & Awards
SIGPLAN Distinguished Paper Award
ACM SIGPLAN · For Guarded Kleene Algebra with Tests at POPL 2020
SIGPLAN Research Highlight
ACM SIGPLAN · For A Fast Compiler for NetKAT at ICFP 2015
Cornell Fellowship
Cornell University
DAAD Fellowship (Jahresstipendium für Studienaufenthalte im Ausland)
German Academic Exchange Service · ~50 recipients per year across all disciplines in Germany
Fulbright Fellowship
Declined in favor of DAAD fellowship
Deutschlandstipendium (Germany Scholarship)
Merit-based scholarship awarded to the top ~1% students across all disciplines in Germany
best.in.tum
Technische Universität München · Top 2% of students
Mathematics Award
Faculty of Mathematics and Informatics, Saarland University · Awarded to the best graduating math student at each high school
07 Teaching
Teaching Assistant · Adrian Sampson · Cornell University
Teaching Assistant · Andrew Myers · Cornell University
Guest Lecturer · Nate Foster · Cornell University
Guest Lecturer · Dexter Kozen · Cornell University
Guest Lecturer · Nate Foster · Cornell University
Teaching Assistant · Andrey Rybalchenko · TU München
08 Education
09 Side Projects
Things I build outside of work.
Your P4 programs, finally explained.
A glass-box P4 simulator that tells you exactly what happened to your packet — every parser transition, table lookup, action, and branch — delivered as a structured trace tree you can actually read. Includes an in-browser playground, C++ embedding library, and P4Runtime gRPC service.
Spoken Mexican Spanish at your rhythm.
An active recall app for mastering real-world Mexican Spanish. Combines FSRS spaced repetition with studio neural audio, typed recall, and a fast keyboard and gesture flow — online or offline.