Sireum is an open source 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.