Aether: High-performance, formally-verified storage engine written in Rust (codeberg.org)

It's so hard to trust a vibe coded software with something with a thing as valuable as data.

I see no reason why would anyone even bother checking this out, while there a trusted, battle scared, and non vibe-coded alternatives such as postgres, duckdb,boltdb,SQLite.

Sorry mate.

big words, either you are a genius, or it's AI slop and we'd be better off using write(). Don't think there's inbetween.

I don't think formally verifying my showing that the model is correct is good enough anymore. You must prove that your implementation refines the model.

The rest of the comments, as of now, are unreasonably unsubstantiated and a little bit hostile. AFAICS it's a large effort combining some pretty damn cool ideas from database internals world - this must have been written by someone experienced. It reminded me of RocksDB immediately, and wanted to see the example of integration, but then I saw redis, memcached, and "financial" database workload/protocol implementations. Good stuff, especially the benchmarks.

The code was obviously written using LLMs and I don't say this because the code looks like it's been LLM-generated but because of the fact that no sane person would have been able to write such complex piece of software in the pre-AI era. To me personally it shows how things dramatically shifted in software, and how domain expertise along with the AI became not 10x but 100x multiplier.

As far as names go, Aether is or was a P2P social network

Formally verified only matters if the implementation actually improves the model, not just matches it in some abstract way. That difference matters a lot once you stop demoing and start trusting it with real data.