I have used SPARK Ada myself on a couple of security focused products developed by a team of 10-15 developers. For a long time, SPARK has made use of formal methods practical for real-world software. Effective use does require learning and commitment, but that's within reason. By the time the projects were nearly done, I felt that the SPARK findings always turned out to be correct and that any remaining problems could be traced back to poor or missing requirements, not the implementation itself.