Frama-C brought multiple static-analysis and deductive-verification techniques into one extensible platform for industrial C, with ACSL contracts serving as a shared language for expressing what code should guarantee.
PVS integrated a rich higher-order specification language, type checking, automated decision procedures, and interactive theorem proving into one environment for serious formal verification.
Rustan Leino’s Dafny made specifications, executable code and automated verification part of one programming language, using Boogie and SMT solving to check functional correctness as developers write programs.