That's true for software in general. However, you're talking about high-assurance security. That takes math skills, patience, a high commitment to security, and a time commitmemt. Most FOSS developers will not build high-assurance security regardless of the model you find.
This is why I favor creating systems that, with user-provided specs, automate proofs, analyses, and testing. The specs should be easy for non-math types to understand. Any failure is fixed or becomes a runtime check with logging. We might get more adoption of something like that than the masses contributing to an Isabelle/HOL or whatever project.
This is why I favor creating systems that, with user-provided specs, automate proofs, analyses, and testing. The specs should be easy for non-math types to understand. Any failure is fixed or becomes a runtime check with logging. We might get more adoption of something like that than the masses contributing to an Isabelle/HOL or whatever project.