Assistant Professor · NUST, Pakistan

Formal Methods,
rigorously verified.

I work at the intersection of formal verification, AI-assisted reasoning, and functional safety - proving the correctness of cyber-physical and biomedical systems by mathematics rather than testing, and building AI tools that help automate the proof process itself.

Adnan Rashid
50+Peer-reviewed publications
2019PhD, NUST
2023–25Postdoctoral Fellow, Concordia University
10+Years of research

About

Correctness by proof, not by chance.

I hold a PhD from the National University of Sciences and Technology (NUST) and was a Postdoctoral Research Fellow at Concordia University's Hardware Verification Group from 2023 to 2025. My work centers on the formal verification of complex cyber-physical and biomedical systems, from physical human-robot interaction and micro-grid reliability, to weather-forecasting models and electrical-circuit topologies, using higher-order-logic theorem proving and probabilistic model checking to obtain guarantees that simulation and testing alone cannot provide.

A growing thread of my research turns AI toward the proof process itself. Tools like HOL4PSG and HOL4PRS use large language models to recommend and generate proof steps for the HOL4 theorem prover, and my recent work on ReasonOps proposes a unified operational paradigm for trustworthy, verified LLM reasoning. On the applied side, I built FETMA, a tool that automates functional-block-diagram and event-tree based safety analysis for systems such as smart-grid substations, and I develop end-to-end safety-assurance strategies for autonomous systems - spanning requirements engineering, traceability, and probabilistic risk assessment.

Focus areas

Where I spend my effort.

Theorem Proving

Higher-Order-Logic Verification

Formalizing transform methods, control systems, and continuous dynamics in HOL Light & HOL4 to obtain absolute correctness guarantees for safety-critical systems.

AI × Verification

AI-Assisted Formal Methods

Building tools like HOL4PSG, HOL4PRS, and ReasonOps that use large language models for proof-step generation, tactic recommendation, and trustworthy verified reasoning - scaling formal verification beyond expert-only workflows.

Functional Safety

Safety Assurance for Autonomy

End-to-end safety-case development for autonomous vehicles, robotics, and smart grids - requirements engineering, traceability, and probabilistic risk assessment.

Recent activity

What's new.