Research
A running catalogue of the systems, theories, and tools I have formally verified — organized by method.
Applying large language models to automate tactic selection and proof-sequence generation in interactive theorem provers.
Explainable AIGenerating formally verified explanations for machine-learning model decisions, including adversarial-example detection.
Formal analysis of image-processing filters using higher-order-logic theorem proving.
Systems BiologyFormal reasoning about synthetic biology using higher-order-logic theorem proving.
AerospaceFormal analysis of UAV continuous dynamics using higher-order logic.
Transform MethodsFormalization of transform methods in higher-order logic, from foundations to real-world case studies.
Systems BiologyFormal reasoning about systems biology using theorem proving.
RoboticsFormal analysis of robotic cell injection systems using theorem proving.
TransportationFormal analysis of macroscopic traffic-flow models in higher-order logic.
Formal analysis of a ZigBee-based routing protocol using the UPPAAL model checker.
PRISMFormal analysis of weather forecasting models using probabilistic model checking.