Sireum is a high-assurance software development platform incorporating various formal analyses and compilation toolchains.
Sireum next gen is currently under development.
Logika is a program verifier and proof checker for propositional, predicate, and programming logics.
Amandroid (now Argus-SAF) is a static analysis framework for security vetting Android apps.