Thanks for the good points! Bolt and LMDB seem approachable, and I'm especially interested how ACID compliance is implemented and how to check/prove the correctness of it...