Skip to content


Folders and files

Last commit message
Last commit date

Latest commit


Repository files navigation

GoTxn: a verified, concurrent, crash-safe transaction system


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


GoJournal: a verified, concurrent, crash-safe journaling system at OSDI 2021