Because formal verification doesn't scale at the moment. There are a relatively few number of experts on formal method around the globe and some of them need to

Because formal verification doesn't scale at the moment. There are a relatively few number of experts on formal method around the globe and some of them need to work on SQLite indefinitely unless you're okay with just one-off verification. Frama-C has a different background because it's from Inria, the institution with many formal method experts.