These oracles are typically associated with formalized approaches to software modeling and software code construction. They are connected to [[formal specification]],<ref>{{cite book |last1=Börger |first1=E |title=Applied Formal Methods — FM-Trends 98 |chapter=High Level System Design and Analysis Using Abstract State Machines |editor-last1=Hutter |editor-first1=D |editor-last2=Stephan |editor-first2=W |editor-last3=Traverso |editor-first3=P |editor-last4=Ullman |editor-first4=M |date=1999|title=High Level System Design and Analysis Using Abstract State Machines |journal=Applied Formal Methods — FM-Trends 98 |volume=1641 |pages=1–43 |doi=10.1007/3-540-48257-1_1 |series=Lecture Notes in Computer Science |isbn=978-3-540-66462-8 |citeseerx=10.1.1.470.3653 }}</ref> [[model-based design]] which may be used to generate test oracles,<ref>{{cite journal |last1=Peters |first1=D.K. |date=March 1998 |title=Using test oracles generated from program documentation |journal=IEEE Transactions on Software Engineering |volume=24 |issue=3 |pages=161–173 |doi=10.1109/32.667877 |citeseerx=10.1.1.39.2890 }}</ref> state transition specification for which oracles can be derived to aid [[model-based testing]]<ref>{{cite journal| author-last1=Utting |author-first1=Mark |author-last2=Pretschner |author-first2=Alexander |author-last3=Legeard |author-first3=Bruno |title = A taxonomy of model-based testing approaches |journal = Software Testing, Verification and Reliability |volume= 22|issue= 5 |issn= 1099-1689|doi=10.1002/stvr.456 |pages= 297–312|year=2012 |url=https://eprints.qut.edu.au/57853/1/master_pdflatex.pdf }}</ref> and [[conformance testing|protocol conformance testing]],<ref>{{cite book|author-link1=Marie-Claude Gaudel |last1=Gaudel |first1=Marie-Claude |title=Reliable SoftwareTechnologies — Ada-Europe 2001 |chapter=Testing from Formal Specifications, a Generic Approach |editor-last1=Craeynest |editor-first1=D.|editor-last2=Strohmeier |editor-first2=A|date=2001 |title=Testing from Formal Specifications, a Generic Approach |journal= Reliable SoftwareTechnologies — Ada-Europe 2001 |volume=2043 |pages=35–48 |doi=10.1007/3-540-45136-6_3 |series=Lecture Notes in Computer Science |isbn=978-3-540-42123-8 }}</ref> and [[design by contract]] for which the equivalent test oracle is an [[assertion (software development)|assertion]].
Specified Test Oracles have a number of challenges. Formal specification relies on abstraction, which in turn may naturally have an element of imprecision as all models cannot capture all behavior.<ref name="Oracle survey"/>{{rp|514}}