My research focuses on formal methods, logics, protocol verification, and model checking — including formal verification of security protocols and machine learning systems.
Neurosymbolic AI
Formally verifying neural networks and differentiable logics using Rocq, with applications to intrusion detection and autonomous driving.
Verified Math Foundations
Contributing to MathComp-Analysis: probability theory, concentration inequalities, and Lebesgue integration in Rocq.
Proof Theory & Automation
Proof theory for linear and intuitionistic logics, Skolemization, and AI-assisted theorem proving in Rocq.
Security Protocol Verification
Formal analysis of security protocols using model checking and abstraction, with applications to IoT, e-voting, and cryptographic choreographies.