In this fourth installment of my continuing AuDaLa journey, I will reach the shores of the formal verification of AuDaLa, only passable with a good and sturdy boat made of proof rules. To explain what I have been doing to create this boat, I will discuss the adaptation of Concurrent Separation Logic for AuDaLa, resulting in AuDaLogic, after which I will introduce AuDaLa’s current iteration of proof rules, and, if time permits, give an example proof tree. I will end my presentation with notes on what still needs to be done for my proof rules to be finished.