KU Leuven’s DistriNet research group is offering a fully funded PhD position focused on mechanized verification and formal methods in system security. The research aims to develop universal contracts for authoritative semantics of Instruction Set Architectures (ISAs) and advance end-to-end system verification techniques. The candidate will work on the Katamaran project, which develops a deductive separation logic-based verifier for ISAs and explores automated verification processes. Ideal candidates should have a background in computer science or mathematics and be eager to learn statically-typed functional programming and formal verification tools like Agda or Coq.