Maximilian Schäffeler
Since early 2026, I have been a postdoctoral researcher at King’s College London, working with Mohammad Abdulaziz on AI for interactive theorem proving. This work is part of the Copilots for Isabelle project, where we combine LLMs with symbolic methods to make the Isabelle proof assistant more powerful and easier to work with.
Before that I did my PhD at the Chair for Logic and Verification, Technical University of Munich, supervised by Prof. Nipkow. There I formalized solution methods for Markov decision processes (MDPs) in Isabelle/HOL. Much of this work is collected in FormPlan, a library of formally verified software for planning and model checking. I also completed my Bachelor’s and Master’s in Computer Science at TUM, specializing in IT security, functional programming and formal methods.
If you are interested in collaborating on a project, feel free to send me an email.
Contact
maximilian.schaffeler at kcl.ac.uk
Preprints
- Safe Agentic Workflows for Isabelle (2026)
Maximilian Schäffeler, Lukas Stevens, Kevin Kappelmann, Mohammad Abdulaziz, Andrei Popescu, Dmitriy Traytel — Isabelle Workshop 2026 - Just Type It in Isabelle! AI Agents Drafting, Mechanizing, and Generalizing from Human Hints (2026)
Kevin Kappelmann, Maximilian Schäffeler, Lukas Stevens, Mohammad Abdulaziz, Andrei Popescu, Dmitriy Traytel — to appear
Publications
- Formally Verified Solution Methods for Markov Decision Processes (2025)
Maximilian Schäffeler — PhD thesis, Technical University of Munich - A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs (2025)
Bram Kohlen, Maximilian Schäffeler, Mohammad Abdulaziz, Arnd Hartmanns, Peter Lammich — CAV 2025 · preprint - Fixed Point Certificates for Reachability and Expected Rewards in MDPs (2025)
Krishnendu Chatterjee, Tim Quatmann, Maximilian Schäffeler, Maximilian Weininger, Tobias Winkler, Daniel Zilken — TACAS 2025 · preprint - Formally Verified Approximate Policy Iteration (2025)
Maximilian Schäffeler, Mohammad Abdulaziz — AAAI 2025 · preprint - Formally Verified Solution Methods for Markov Decision Processes (2023)
Maximilian Schäffeler, Mohammad Abdulaziz — AAAI 2023 · preprint
Archive of Formal Proofs
- Type Annotations with Roundtrip Property (2026)
Kevin Kappelmann, Lukas Stevens, Maximilian Schäffeler, Mohammad Abdulaziz, Andrei Popescu, Dmitriy Traytel - Markov Decision Processes with Rewards (2021)
Maximilian Schäffeler, Mohammad Abdulaziz - Verified Algorithms for Solving Markov Decision Processes (2021)
Maximilian Schäffeler, Mohammad Abdulaziz