GoTxn is a transaction system that makes it easy to safely access a disk with concurrent transactions that are atomic if the system crashes in the middle. The implementation is verified in Perennial, and the proof can be found alongside the Perennial framework.
The biggest use of GoTxn is GoNFS, a verified implementation of the Network File System (NFS) API that uses GoTxn to simplify implementing and verifying a concurrent file system.
This repository is still called go-journal, as GoTxn evolved from a journaling
system to a transaction system. The journaling layer is still available as
github.com/mit-pdos/go-journal/jrnl.
GoJournal: a verified, concurrent, crash-safe journaling system at OSDI 2021