About the Lab
The Schlichtkrull Lab focuses on building mathematically rigorous foundations for trustworthy software and computational systems. The group works extensively with the Isabelle/HOL proof assistant to formalize logical systems, program analyses, and verification algorithms. Current research spans the formalization of first-order and higher-order proof systems, correctness proofs for Datalog- and pushdown-based static analysis frameworks, and automated verification of stateful security protocols. A recurring theme in the lab’s work is bridging the gap between theory and practice by creating verified oracles, generating executable code from mechanized proofs, and applying differential testing to uncover bugs in real-world verification tools. The group also contributes to the foundations of trust policy languages and self-sovereign identity models, highlighting the societal relevance of formal reasoning in security and privacy. Students who thrive here typically enjoy formal logic, functional programming, and understanding systems at a deep, structural level. The lab is well suited for those who want to work with proof assistants, design sound verification frameworks, or contribute to the reliability of safety- and security-critical software.