The Ironclad project[1] claims to have created a formally-verified differential privacy database. I recommend watching the demo video, the development efficienc

The Ironclad project[1] claims to have created a formally-verified differential privacy database. I recommend watching the demo video, the development efficiency they saw using formal verification is jaw-dropping. [1] https://www.usenix.org/conference/osdi14/technical-sessions/presentation/hawblitzel https://www.usenix.org/conference/osdi14/technical-sessions/...