Why do you care about AI Existential Safety?

My background is in formal methods: I’ve worked with tools like Gobra for verifying Go programs and Lean for machine-checked proofs. In that world, you learn to be deeply skeptical of informal reasoning. A system that “seems to work” is not the same as a system that provably works. Bugs hide in the gap.

AI existential safety feels like the same problem, but with incomparably higher stakes. We’re building increasingly capable systems whose behavior we don’t fully understand, and whose alignment with human values we can’t yet verify–let alone prove. That asymmetry troubles me: the cost of being wrong is not a buggy program, it’s irreversible.

Formal methods taught me that the hardest part isn’t writing the code but it’s precisely specifying what you want and proving you got it. AI safety faces both problems at once: we don’t have a formal specification of “beneficial”, and we have no verification framework capable of checking it. That’s not a reason for paralysis, but it is a reason to care urgently. The field needs people who are comfortable with rigor, uncertainty, and the gap between “probably fine” and “demonstrably safe”. And that’s exactly what formal reasoning trains you for.

Please give at least one example of your research interests related to AI existential safety:

Throughout my PhD and my PostDoc, I’m focusing on reasoning rigorously about implementations using my own program verifier Gobra and Lean. Over the course of the last year, I’ve extensively used AI in my work to help me coming up with proofs that are then machine checked. More specifically, I’ve recently verified a core algorithm in the Go programming language’s standard library that is used to generate RSA private keys. Giving this task to Claude Code failed several times as Claude Code could not port an existing proof to this implementation, which led me to discover a mismatch between the implementation and what its specification is saying. I’ve fixed the implementation and have a proof of its correctness and I’m now working with the Go team to get my changes into the standard library.

This is a big success story for AI as giving the AI access to tools like Gobra or Lean boosts productivity massively of AI _and_ humans as these tools provide useful error messages allowing AIs and humans to iterate until a proof is complete.