Mathematics, software, science, indeed society, depends on trust, yet trust is in short supply. Formal verification offers a path toward proven correct solutions, thus ameliorating the need for trust. Using math as a case study, I will argue that we are on the cusp of large-scale automatic formalization, by which we can move from implicit dependence between research and informal argumentation in papers to explicit dependence and formal verification. I will conclude by outlining major research directions required in order to realized trusted foundations across mathematics, software, science, and society.