Research

My research focuses on formal methods, logics, protocol verification, and model checking — including formal verification of security protocols and machine learning systems.

Ongoing Projects

• Neurosymbolic AI — Formally verifying neural networks and differentiable logics using the Rocq proof assistant, with applications to safety-critical machine learning systems.

• Verified Mathematical Foundations in Rocq — Contributing to MathComp-Analysis, a Rocq formalization of mathematical analysis, focusing on probability theory and concentration inequalities.

• NLP for Interactive Theorem Proving — Integrating large language models with the Rocq prover for automated proof generation, proof translation, and learning environments.

Neurosymbolic AI

Overview

Neurosymbolic AI combines the pattern-recognition power of neural networks with the rigour of symbolic reasoning. My work in this area focuses on formally verifying correctness and robustness properties of neural networks and other machine learning systems using the Rocq proof assistant.

A central goal is to give machine learning systems the same level of trustworthiness that we expect from safety-critical software, by providing machine-checked proofs of their behaviour.

Differentiable Logics in Rocq

Differentiable logics are a family of logical frameworks that allow neural networks to be trained to satisfy logical specifications by differentiating through the logic. I am working on:

NLP for Interactive Theorem Proving

Overview

Large language models (LLMs) have shown surprising ability at natural language reasoning. Interactive theorem provers (ITPs) such as Rocq provide a rigorous setting where every reasoning step can be machine-checked. Combining the two opens a new frontier in automated mathematical reasoning.

I explore the integration of LLMs with ITPs, aiming to make proof development faster, more accessible, and eventually capable of tackling frontier mathematical problems.

Research Directions

Automated proof generation. Given a theorem statement in Rocq, can an LLM propose a valid proof? I study how to prompt, fine-tune, and evaluate models for this task, with a focus on proofs that are verified end-to-end by the Rocq kernel.

Verified Mathematical Foundations in Rocq

Overview

Rigorous mathematics requires that theorems be provably correct. Proof assistants such as Rocq make this literal: every step of a proof is mechanically verified by a computer. I contribute to MathComp-Analysis, a large-scale formalization of mathematical analysis built on the Mathematical Components library.

My focus is on probability theory — building machine-checked foundations for the mathematics that underpins statistics, machine learning, and information theory.

Probability Theory and Lebesgue Integration

Classical probability theory rests on measure theory and the Lebesgue integral. I formalize this infrastructure in Rocq, including: