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.