I admit to curiosity as to whether static analysis could have caught this. E.g., Rust's type system (yeah yeah I know) catches all data races, unless they originate in unsafe code, which this one might or might not have; a hypothetical Rust SQLite would probably need a lot of unsafe (https://github.com/tursodatabase/turso has 556 unsafe blocks in the core), and I don't have a sense of whether the particular part that contained this bug would be included in that.
Interesting. I don't think this kind of technique could realistically have caught the bug in advance, though; you're not going to model the entire codebase in TLA+, so the investigation in that post modeled just the parts that turned out in hindsight to be relevant.
LLMs are not at the point where they can reliably complete this kind of task without making mistakes. The model checker can tell you whether the formal design specification contradicts itself, but it can't tell you whether it matches the implementation, nor whether it matches the programmers' intentions. And it's too much for humans to review by hand.
This is importantly different from formal code verification, in which the specification that needs to match the programmers' intentions is small enough to review, while the bulk of the LLM's output is proof tactics and such, which don't need human review because the verifier guarantees* that they're right.
I suppose you could just tell Fable "hey try using TLA+ to look for bugs in this code" and see whether it finds any.
It sounds like it was a bug caused by pushing on performance/safety ratio, it could easily have been avoided by adding enough mutexes in the code, but for performance reasons (I assume) they don't do that. To write it like that in Rust you'd have to use unsafe blocks and then you don't gain much from the typesystem in this case.
