alt Hacker NewsThis 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.
I have to admit I used to think any level of formal verification was worthwhile.
But I recently tried having agents try starting with formal models, and then building code using that as basis. In the end to models were never detailed enough to catch the most common issues that were shaken out with getting a high level of coverage and mutation testing.
At which point, the predictive power of the formal models became somewhat vacuous.
I’m trying to be more optimistic that maybe using dependently typed languages will yield better results.