- It's like asking why can't we connect together all software ever written so each software problem only needs to be coded once. Ideally you could, but you can't. The same way there's different programming languages (with major and subtle differences), different libraries that do similar things, different APIs, different data structures etc. all attempting to improve on something, formal verification has competing languages, logics, tools etc. You can't just take a PHP library and use it as if it was a JavaScript library, the same way you can't take a proof in Isabelle and use it in a Coq proof.

- Correctness proofs of even simple algorithms can be research grade problems that take several person years of effort from (hard to find) experts, so you're not likely to get casual Stack Overflow style contributions because of the order of magnitude difference in time and expertise required.

- The time required to verify correct software will come at a major cost to other factors like features and speed. I don't think 100% correctness is a driving factor for many domains like web servers, browsers and IDEs, so your database of correct software isn't going to be widely used until it catches up on other factors.