Separation logic & proof assistants
As is incredibly difficult for fully automatic techniques to prove full functional correctness, a number of projects use separation logic within a proof assistant (in the sense of the LCF/HOL/Isabelle/Coq tradition). Often these interactive proofs are assisted by advanced tactics that carry out many mundane proof steps.
CAP/SCAP/XCAP (Yale)
Concurrent C Minor (Princeton)
Holfoot (Cambridge)
L4.verified (Sydney)
SepLog in Coq (Tokyo)
Ynot (Harvard)