We research formal methods for system design. We look at both functional properties and at security properties. For example, we develop methods to ensure that machine learning systems fulfill certain formal properties, or that systems are not vulnerable to power sidechannel or fault injection attacks. We use mathematical methods and create software tools to automatically prove correctness. One of our specialties is reactive synthesis: methods and tools that automatically generate correct systems from their specs. We publish at conferences like Computer Aided Verification (CAV) and Formal Methods for Computer Aided Design (FMCAD).