Design and Formalization of Blockchain Oracles

 Oracles are crucial components that connect the smart contracts deployed on Blockchain to the external world. With the recent surge in popularity of decentralized finance (DeFi) applications, it is critical to provide assurances about the oracle implementations as they deal with high-value transactions and a small mistake can lead to huge losses. We present a simple oracle implementation in Solidity, as well as a formalization in the Coq proof assistant where we prove that the oracle protocol satisfies certain desirable economic sustainability properties.