Welcome to my home page, I am Will Thomas. I am a PhD student in Computer Science in the area of Formal Methods and Cybersecurity at the University of Kansas.

"A commit is worth a thousand words", so please check out my GitHub for the latest things I have been up to. The majority of my work takes place in the Rocq/Coq theorem prover, but I also frequently work in functional languages such as OCaml, CakeML, as well as some Rust when speed is imperative. Most recently, I have been working on formalizing and verifying a layered attestation manager for the Copland DSL for Attestation. I contribute regularly to VsCoq to improve the VSCode experience of proving with Coq.

Projects

Here are some of the projects I have been working on lately. The specific projects that make it to my website are usually those that I reference often, or think others may find beneficial. For a more exhaustive list check out my GitHub and the KU-SLDG Lab pages