Oracles are constructs used in decentralized finance to price assets relative to each other. However, oracles contain defects that could lead to manipulation attacks. Such attacks exploit pricing models embedded within oracles to defraud creators and users. We automatically verify defects, which if mitigated, improves the security of digital currency.
