UltimaDB, a high performance full-featured MVCC transactional embedded database, with special focus for use on SMR clusters.
UDB has full transactions, selectable persistence (in-memory, eventual, strict) and consistency (SI, SSI). A lot of time was spent on performance.
Written in Rust, with 8k line of code and 15k lines of tests, 96% coverage. Formal verification with Lean 4 is in progress (see /formal), also consistency checking with elle/jepsen is in progress.