There's also a new startup[0] that came out recently from stealth with mission to auto formally verify all of open source in Lean.

[0] https://andtruth.com/the-proof/