Isabelle (v2016-1) soundness proof for concurrent separation logic (CSL), also hosted on the website, CSL Soundness. This proof is done under the supervision of Dr. J. Brotherston.
The original proof is done by Viktor Vafeiadis, see his paper Concurrent separation logic and operational semantics.
"The new proof gives a direct meaning to CSL judgments, explains clearly the problem with the conjunction rule and "precise" resource invariants, and can easily be adapted to handle extensions of CSL, such as permissions and storable locks, as well as more advanced program logics, such as RGSep."[*]
What is Isabelle?
"Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. Isabelle was originally developed at the University of Cambridge and Technische Universität München, but now includes numerous contributions from institutions and individuals worldwide. See the Isabelle overview for a brief introduction."[*]