Yesterday, I worked on familiarizing myself with the MultiCompUnit, and began writing a formal proof for it. Today, I'd like to refactor that proof to better match up with the description on the wiki page. Also, summer classes began today for me, so I may be less productive on Libre-SOC for the next two months. --Michael