Authorization protocols are critical to security, yet they are among the most common sources of security breaches. We propose the formal verification of SciTokens, a federated authorization ecosystem adopted by major NSF infrastructures such as LIGO and Open Science Grid. Our in-progress work includes two critical vulnerabilities identified through the formal verification process, along with a verified-correct bug fix for the second vulnerability. We emphasize the role of formal verification in our vulnerability finding, which forces us to rigorously consider all edge cases that often escape manual auditing and testing.