In this presentation, I will recap the concepts of AuDaLa and give the design of a parallel sorting algorithm, Insertion Sort, which requires the use of write-write data races. I will prove this algorithm correct, during which I will discuss finding data races in AuDaLa, creating contracts for AuDaLa steps and basic lemmas to help creating the proof of AuDaLa programs.