Hi! My name is Max von Hippel

Max von Hippel ... and I am a Staff Scientist at Anduril Industries, where I lead formal methods for the company. Previously, I co-founded Benchify (YC S24), an autoformalization startup, and before that, I completed a PhD at Northeastern University Khoury College of Computer Science, advised by Dr. Cristina Nita-Rotaru, as well as a BS in pure mathematics from the University of Arizona, an International IB diploma from UWCCR, and most importantly, a Blue Belt from 10th Planet Jiu Jitsu. During grad school I became one of the last remaining ACL2 enthusiasts. I also co-organize the Boston Computation Club and am heavily involved with the FMxAI community. I grew up in Anchorage, Alaska. You can email me at maxvh-at-hey-dot-com. My old website is archived here.

Blog Posts

crane Your Software Should Build Itself, by Max von Hippel. LessWrong, 2026.
crane How to Solve Secure Program Synthesis, by Max von Hippel, Simon Henniger, Quinn Dougherty, & Evan Miyazono. LessWrong, 2026.
fencing The Scalable Formal Oversight Research Program, by Max von Hippel. LessWrong, 2026. See also: my SOTA Letter
fencing Can You Just Vibe Vulnerabilities?, by Max von Hippel. LessWrong, 2026.
fencing Lies, Damned Lies, and Proofs: Formal Methods are not Slopless, by Quinn Dougherty & Max von Hippel. LessWrong, 2026.

Datasets and Benchmarks

saturn FVSpec: Real-World Property-Based Tests as Lean Challenges, Quinn Dougherty, Mike Dodds, Max von Hippel, Simon Henniger, and Hazel Shackleton. See also our preprint.
saturn BuddenBench: Over 1K Open Problems in Pure Mathematics, by Max von Hippel.

Dissertation

dissertation Verification and Attack Synthesis for Network Protocols, by Max von Hippel. Ph.D. Dissertation, Northeastern University (2025). Committee: Cristina Nita-Rotaru, Pete Manolios, Guevara Noubir, & Joseph Kiniry. [PDF]

Publications

sos AI Security is a LangSec Problem, by Max von Hippel and Evan Miyazono. LangSec Workshop, 2025. [PREPRINT]
package A Formal Analysis of SCTP: Attack Synthesis and Patch Verification, by Jacob Ginesin, Max von Hippel, Evan Defloor, Cristina Nita-Rotaru, & Michael Tüxen. Applied Networking Research Prize! USENIX, 2024. [RFC ERRATUM] [PREPRINT] [CODE]
package Formal Model-Driven Analysis of Resilience of GossipSub to Attacks from Misbehaving Peers, by Ankit Kumar, Max von Hippel, Pete Manolios, & Cristina Nita-Rotaru. IEEE S&P, 2024. [CVE] [PREPRINT] [CODE]
package Verification of GossipSub in ACL2s, by Ankit Kumar, Max von Hippel, Pete Manolios, & Cristina Nita-Rotaru. Best Student Paper Award! ACL2, 2023. [PDF] [CODE]
package A Case Study in Analytic Protocol Analysis in ACL2, by Max von Hippel, Pete Manolios, Kenneth L. McMillan, Cristina Nita-Rotaru, & Lenore Zuck. 2nd Best Student Paper Award! ACL2, 2023. [PDF] [CODE]
package A Formal Analysis of Karn’s Algorithm, by Max von Hippel, Kenneth L. McMillan, Cristina Nita-Rotaru, & Lenore Zuck. Best Paper Award! NETYS, 2023. [PDF] [CODE] [KHOURY NEWS] [APNIC BLOG] [RIPE BLOG]
map HoLA Robots: Mitigating Plan-Deviation Attacks in Multi-Robot Systems with Co-Observations and Horizon- Limiting Announcements, by Kacper Wardega, Max von Hippel, Roberto Tron, Cristina Nita-Rotaru, & Wenchao Li. AAMAS, 2023. [CODE] [PDF]
bee Byzantine Resilience at Swarm Scale: A Decentralized Blocklist Protocol from Inter-robot Accusations, by Kacper Wardega, Max von Hippel, Roberto Tron, Cristina Nita-Rotaru, & Wenchao Li. AAMAS, 2023. [CODE] [PDF]
reading Automated Attack Synthesis by Extracting Finite State Machines from Protocol Specification Documents, by Maria Lenore Pacheco, Max von Hippel, Ben Weintraub, Dan Goldwasser, & Cristina Nita-Rotaru. IEEE S&P, 2022. [CODE] [PDF] [DEV BLOG] [APNIC BLOG] [VIDEO] [TEASER]
robot Automated Attacker Synthesis for Distributed Protocols, by Max von Hippel, Cole Vick, Stavros Tripakis, & Cristina Nita-Rotaru. SafeCOMP 2020. [CODE] [PDF] [DEV BLOG] [VIDEO]
ice Long-Term and Inter-Annual Mass Changes in the Iceland Ice Cap Determined from GRACE Gravity using Slepian Functions, by Max von Hippel & Christopher Harig. Frontiers in Earth Science, 2019. [CODE]
DNA Reproducible, Interactive, Scalable and Extensible Microbiome Data Science using QIIME 2, by Evan Bolyen, Jai Ram Rideout, Matthew R Dillon, [...], Max von Hippel, [...], & Greg Caporaso. Nature Biotechnology, 2019. [CODE]

Research Talks

sos Vibed Vulnerability Classes. Presented to the TwoSix Mathematics Seminar (2025).
sos Systems Engineering for AI. Presented to EN.601.229: Computer System Fundamentals at Johns Hopkins (2025).
package A Case Study in Analytic Protocol Analysis in ACL2. Presented to the ACL2 Workshop (2023) and Galois Tech Talks (2023).
handshake Formal Analysis of Ethereum’s GossipSub in ACL2s. Presented to New England Systems Verification Day (2022).
reading Automated Attack Synthesis by Extracting Finite State Machines from Protocol Specification Documents. Presented with Maria Lenore Pacheco to Microsoft Research Redmond Cryptography and Privacy Colloquium (2022), MIT CSAIL Security Seminar (2022), Trail of Bits Security Seminar (2022), ASU SEFCOM Seminar (2022), & IETF ANRW (2022).
robot Automated Attacker Synthesis for Distributed Protocols. Presented to NDS2 Seminar (2019), University of Arizona Mathematics Seminar (2019), MIT CSAIL Security Seminar (2020), University of Connecticut Security Seminar (2020), & Lindy Labs Lunch Seminar (2022). Presented in Spanish to Universidad del Valle de Guatemala Mathematics Seminar (2022).

Internships

galois Galois: Working on the DETECT project, as part of DARPA's HARDEN program. (Fall 2023)
DoD Department of Defense. (Summer 2019)
nasa National Aeronautics and Space Administration: Working on super-sonic ADS-B for the FA-18B war-bird. (Summer 2018)
nasa National Aeronautics and Space Administration: Estimating ice mass loss in Iceland using GRACE data. (Fall 2017/Spring 2018)

Committee Memberships

microscope IETF Usable Formal Methods Working Group (2023)
satellite World Technology Games Advisory Group (2023-now)

Emojis from OpenMoji