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.

The part that’s not clear to me is, does the spec actually align with what’s been implemented, or has the spec only been formally verified. I think the risk with vibe coding this sort of thing is that claude assures you the rust code implements the spec when it doesn’t