Formality is An efficient proof language.
Fast: no garbage-collection, optimal beta-reduction and a massively parallel GPU compiler make it fast.
Safe: a type system capable of proving mathematical theorems about its own programs make it secure.
Portable: the full language is implemented in a 400-LOC runtime, making it easily available everywhere.
