An seL4-based architecture for layered attestation. - Grant Jurgensen; Michael Neises; Perry Alexander (HotSoS, 2020)

Design and formal verification of a copland-based attestation protocol. - Adam Petz; Grant Jurgensen; Perry Alexander (MEMOCODE, 2021)

A Proof of the Schröder-Bernstein Theorem in ACL2. - Grant Jurgensen (CoRR, 2025)