- Formally verify the highest-risk parts of the Monad implementation, including concurrent and parallel execution logic.
- Build and refine Rocq models of system designs, then prove the C++ implementation equivalent to those models.
- Catch design and implementation bugs before they reach main.
- Develop specifications and weakest-precondition proofs for production C++ using BRiCk and Iris separation logic.
- Strengthen theorem statements and proof automation, and devise approaches that scale verification to a fast-moving codebase.
C++