Grove is a separation logic library for verifying distributed systems. It is built as an extension of the Perennial framework, and thus actually lives in the Perennial repository here. It is described in this SOSP'23 paper.
In the Perennial repository, the
src/program_proof/vrsm
contains proofs related to the case study built in the SOSP'23 paper. The Go
source code for this case study can be found
here.