As far as names go, Aether is or was a P2P social network
Aether: High-performance, formally-verified storage engine written in Rust
11–15 of 15 posts
Re: Aether: High-performance, formally-verified storage engine written in Rust
#12The 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 implementation…
> no sane person would have been able to write such complex piece of software in the pre-AI era.
Insane take
Re: Aether: High-performance, formally-verified storage engine written in Rust
#13Formally 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.
Re: Aether: High-performance, formally-verified storage engine written in Rust
#14The 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 implementation…
> no sane person would have been able to write such complex piece of software in the pre-AI era. Insane take
Why do you say so?
Re: Aether: High-performance, formally-verified storage engine written in Rust
#15Earlier quoted context omitted.
Formal verification should catch vibe coding bugs.
This is the entire formal verification effort, as far as I can tell: https://codeberg.org/gregburd/aether/src/branch/main/aether/... They use TLA+ with TLC which model checks the write ahead log (a component of the system). But that only models the WAL protocol, not the actual Rust code and not the other 99% of the system. Any formal verification is of course awesome to see though.
And just because you model the system in tla+ and its a valid model doesn't mean the vibe coded implementation matches the tla+ model