Working on verifiable correctness for programs written in LM or anything that generates annotated assembly. Basically low-level proofs that accessed memory is valid and live or that function pre/post-conditions are met.

The goal is that these proofs are compiler agnostic, so more people can use them.