I wrote my Master's thesis about Rust verification, exploring type invariants and ghost code
Hi fellow rustaceans!
Last year, I wrote my Master's thesis and decided to combine my love for Rust and formal methods. So, I teamed up with Xavier Denis and Jacques-Henri Jourdan to improve and extend the Rust verifier Creusot. Creusot is a tool that can (semi-) automatically check that a Rust program satisfies user-annotated specifications.
My work focused on two features: type invariants and ghost code. Type invariants let you attach logical predicates to data types, which Creusot enforces for all values of a type. Ghost code is extra code added to aid verification without affecting the program’s runtime behavior.
In my thesis, I:
- Explain the basics of Rust verification with Creusot
- Discuss the design of type invariants and compare them to similar concepts like refinement types
- Analyze soundness issues around ghost code
- Evaluate the implementation of these features in Creusot
I am happy to answer any questions!