I’m Agustín Martinez Suñé, a Postdoctoral Research Associate at the University of Oxford, where I work with the OXCAV research group.

I earned my Ph.D. in Computer Science from the University of Buenos Aires, Argentina, specializing in formal methods for distributed systems analysis. My research has been published in leading venues including TCS, FM, and ICTAC, where our work was recognized with the Best Paper Award in 2023.

Building on my expertise in formal methods, I worked as a Formal Verification Engineer at Nethermind, where I co-developed Horus, the first automated verification tool for StarkNet smart contracts.

In 2024, I was awarded a PIBBSS Research Fellowship to work at the London Initiative for Safe AI, where I explored approaches for integrating language models with symbolic planners to create safe LLM agents. This experience led me to focus my research on the intersection of formal verification and AI safety, with interests spanning model checking, temporal logics, SMT solving, safe reinforcement learning, and safe LLM agents.

My research vision is to bridge formal methods and machine learning to create trustworthy, verifiable AI systems that can be rigorously analyzed and certified.