{"schema_version":1,"research_id":"eoa_inverse_innovation_exp05_external_evaluation_20260803","source_assessment_id":"computability_boundary_mapping__economics_finance:P1:v0","cell_id":"computability_boundary_mapping__economics_finance","search_queries":["site:cftc.gov smart contracts primer operational risks oracle 2018 PDF","site:bis.org CPMI IOSCO principles financial market infrastructures model risk settlement finality PDF","ISDA Common Domain Model smart contracts formal verification official","formal verification financial smart contracts finite state model checking research","site:cftc.gov \"Primer on Smart Contracts\" risks oracle operational","site:cftc.gov derivatives clearing organization programmable smart contracts DLT risk management","site:isda.org Tokenovate taskforce develop smart contract framework CDM 2025","site:docs.daml.com termination recursion language smart contracts","site:docs.marlowe.io finite contract timeout static analysis financial contracts official","Marlowe financial contracts semantics finite horizon static analysis paper","site:docs.daml.com recursion termination language restrictions official","site:bls.gov OEWS software developers May 2025 wage"],"sources":[{"source_id":"S1","title":"A Primer on Smart Contracts","publisher":"U.S. Commodity Futures Trading Commission, LabCFTC","url":"https://www.cftc.gov/sites/default/files/2018-11/LabCFTC_PrimerSmartContracts112718.pdf","source_class":"GOVERNMENT_OR_REGULATOR","publication_date":"2018-11-27","accessed_at":"2026-08-03","claims_supported":["Smart contracts are coded functions that may automate payments based on external events or data.","CFTC-regulated derivatives, clearing, and settlement are identified as possible smart-contract uses.","The CFTC identifies unintended software vulnerabilities, scaling issues, external-system dependencies, oracle failure, weak safeguards, and governance as material risks.","Code-based derivatives remain subject to applicable law, supervision, and financial-integrity requirements."]},{"source_id":"S2","title":"Clearing Organizations","publisher":"U.S. Commodity Futures Trading Commission","url":"https://www.cftc.gov/es/node/123606","source_class":"GOVERNMENT_OR_REGULATOR","publication_date":"undated","accessed_at":"2026-08-03","claims_supported":["DCOs mutualize or transfer credit risk and arrange settlement or netting.","DCO core principles require product-eligibility standards, appropriate risk management, timely settlement under varying circumstances, systems safeguards, governance, records, and a well-founded legal framework.","A DCO and its listing or risk-governance bodies are identifiable adopters and authorizers, while the CFTC is the relevant U.S. regulator."]},{"source_id":"S3","title":"Principles for Financial Market Infrastructures","publisher":"Committee on Payment and Settlement Systems and International Organization of Securities Commissions, hosted by the Bank for International Settlements","url":"https://www.bis.org/cpmi/publ/d101a.pdf","source_class":"STANDARD","publication_date":"2012-04","accessed_at":"2026-08-03","claims_supported":["FMIs should manage credit, collateral, liquidity, settlement-finality, operational, and legal risks.","Principle 17 requires identification of internal and external operational risks, reliable and scalable systems, clear responsibilities, testing after significant changes, and management of service-provider risks.","Operational failures can produce financial loss, legal consequences, and systemic risk.","FMI rules and procedures should be clear, comprehensive, current, and understandable to participants."]},{"source_id":"S4","title":"CDM Smart Contract Taskforce: Interest Rate Resets","publisher":"International Swaps and Derivatives Association","url":"https://events.isda.org/CDM-Smart-Contract/home","source_class":"OFFICIAL_ORGANIZATION_DATA","publication_date":"2026-09-23","accessed_at":"2026-08-03","claims_supported":["ISDA, Tokenovate, and the FINOS CDM Smart Contract Taskforce are developing a smart-contract framework built on the Common Domain Model.","The framework targets consistent execution of multi-step derivatives processes such as interest-rate resets.","The stated benefits include accurate processing, alignment with industry definitions, transparent audit trails, and reduced operational risk.","This is visible industry pull for standardized executable derivatives infrastructure, although it does not expressly request a computability gate."]},{"source_id":"S5","title":"Marlowe: Implementing and Analysing Financial Contracts on Blockchain","publisher":"Springer Nature, Financial Cryptography and Data Security 2020","url":"https://link.springer.com/chapter/10.1007/978-3-030-54455-3_35","source_class":"PRIMARY_RESEARCH","publication_date":"2020-08-07","accessed_at":"2026-08-03","claims_supported":["A restricted financial-contract DSL can support exhaustive pre-execution analysis and counterexample generation.","Marlowe uses bounded recursion and has a finite bound on accepted transactions, enabling finite symbolic analysis.","Its semantics and termination-related properties were formally verified, including conservation of money and eventual timeout closure.","The work is close prior art for language restriction, exhaustive checking, fixed semantics, and financial-contract safety guarantees."]},{"source_id":"S6","title":"eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts","publisher":"ACM CCS 2020 authors; arXiv distribution","url":"https://arxiv.org/abs/2005.06227","source_class":"PRIMARY_RESEARCH","publication_date":"2020-05-13","accessed_at":"2026-08-03","claims_supported":["Sound automated over-approximation of smart-contract bytecode is technically feasible.","Unknown callers, callees, and blockchain data complicate sound analysis and require explicit abstractions.","In the reported evaluation, the sound analyzer terminated on 95 percent rather than all representative contracts, illustrating the need to preserve non-results instead of forcing Boolean answers.","The research distinguishes bounded execution of an instance from unrestricted language expressiveness and documents false-alarm and soundness tradeoffs."]},{"source_id":"S7","title":"Formal Verification of Smart Contracts","publisher":"Ethereum.org","url":"https://ethereum.org/developers/docs/smart-contracts/formal-verification/","source_class":"OFFICIAL_GUIDANCE","publication_date":"2026-06-26","accessed_at":"2026-08-03","claims_supported":["Smart-contract verification already uses finite-state models, temporal logic, model checking, theorem proving, SMT solving, symbolic execution, and formal EVM semantics.","Specifications must unambiguously state the property being checked.","High-level models can omit implementation details, creating a semantic-fidelity risk.","Multiple existing tools and specification languages make a small offline prototype technically plausible."]},{"source_id":"S8","title":"Occupational Employment and Wages — May 2025","publisher":"U.S. Bureau of Labor Statistics","url":"https://www.bls.gov/news.release/ocwage.htm","source_class":"GOVERNMENT_OR_REGULATOR","publication_date":"2026-05-15","accessed_at":"2026-08-03","claims_supported":["May 2025 mean annual wages were $148,100 for software developers, $153,930 for computer and information research scientists, $141,480 for actuaries, and $185,840 for lawyers.","OEWS wages exclude supplementary benefits and other employer costs, so loaded resource-equivalent costs must exceed salary figures.","These wage anchors support only broad order-of-magnitude staffing estimates, not vendor prices or clearinghouse-specific budgets."]}],"problem_evidence":{"support":"MODERATE","rationale":"Programmable derivatives and smart-contract use in clearing and settlement are visibly contemplated, and official sources identify software, oracle, external-dependency, settlement, collateral, and operational risks that matter for a clearinghouse. Primary research also demonstrates that even a sound analyzer may not terminate on every contract. However, no opened source verifies the candidate's precise operational premise: a DCO admitting contracts with unbounded recursion or adaptive modules while forcing analyzer timeouts into a solvent/insolvent interface. That workflow remains hypothetical or proprietary.","source_ids":["S1","S2","S3","S6"]},"stakeholder_evidence":{"support":"MODERATE","rationale":"A DCO listing committee/model-risk function is an identifiable authorizer under CFTC product-eligibility, risk-management, settlement, and safeguards duties. ISDA, Tokenovate, and FINOS are visibly developing standardized executable derivatives workflows and explicitly seek accuracy, auditability, and lower operational risk. No DCO, regulator, or named funder was found expressly requesting the proposed computability classification, seven-status router, or pilot.","source_ids":["S2","S3","S4"]},"prior_art":{"proximity":"ADJACENT_PRIOR_ART","closest_analogues":[{"name":"Marlowe financial-contract DSL and static analyzer","similarity":"Very close on restricted financial-contract semantics, enforceable finite execution, exhaustive analysis, counterexamples, termination proof, and money-preservation guarantees.","remaining_difference":"It is a contract language and analysis environment, not a DCO listing-governance process that first classifies unrestricted solvability and preserves exact, approximate, unknown, out-of-scope, and failure statuses through authorization.","source_ids":["S5"]},{"name":"eThor sound EVM static analysis","similarity":"Close on sound over-approximation, formal semantic grounding, external-code uncertainty, practical nontermination, and the need to avoid interpreting an incomplete result as safety.","remaining_difference":"It analyzes reachability/security properties in EVM bytecode and does not supply a clearinghouse-specific collateral-solvency property, parser-enforced financial fragment, governance record, or listing router.","source_ids":["S6"]},{"name":"Ethereum formal-verification toolchain and practices","similarity":"Establishes that finite-state modeling, model checking, theorem proving, SMT checking, symbolic execution, and formal execution semantics are established smart-contract practices.","remaining_difference":"It is general technical guidance rather than an institutional computability gate with explicit decision authority and downstream status preservation.","source_ids":["S7"]},{"name":"ISDA/FINOS CDM Smart Contract Taskforce","similarity":"Close on standardized executable derivatives semantics, multi-step processing, auditability, and operational-risk reduction.","remaining_difference":"The public description does not claim unrestricted solvency decidability, formal proof obligations, a bounded fragment, sound abstraction, or non-Boolean listing outcomes.","source_ids":["S4"]}],"distinctive_claim_remaining":"For a DCO reviewing programmable contracts, freezing executable semantics and enforcing a bounded fragment, then preserving EXACT_PASS, EXACT_FAIL, SOUND_SAFE, POSSIBLE_BREACH, UNKNOWN, OUT_OF_SCOPE, and SYSTEM_FAILURE through committee workflow, will reduce unjustified Boolean solvency decisions relative to simulation-plus-timeout review without automatically approving any unproved case. This is contrastive and falsifiable, but not established by the web evidence.","confidence":"HIGH"},"implementation_evidence":{"support":"MODERATE","rationale":"Restricted financial DSLs, exhaustive symbolic analysis, termination proofs, sound abstract interpretation, and existing verification tools demonstrate technical feasibility for the bounded offline prototype. CFTC and PFMI materials establish workflow and governance hooks. Remaining feasibility depends on proprietary contract semantics, compiler/oracle fidelity, usable fragment coverage, independent proof review, data access, and legal interpretation. Safety is manageable for a read-only pilot, but production clearance would require validation against executed settlement behavior and formal change control.","source_ids":["S2","S3","S5","S6","S7"]},"scores":{"meaningful_impact":{"score":4,"rationale":"Preventing an unproved SAFE decision at a clearinghouse could avoid collateral shortfalls, settlement disruption, and risk mutualization across members; realized incidence and impact are not measured.","source_ids":["S1","S2","S3"]},"stakeholder_pull":{"score":3,"rationale":"There is clear institutional demand for accurate, auditable executable derivatives workflows and clear DCO risk duties, but no expressed demand for this exact computability-gate intervention.","source_ids":["S2","S4"]},"incremental_advantage":{"score":3,"rationale":"Explicit solvability classification and status-preserving governance improve on simulation-only Boolean review, but many technical ingredients already exist in Marlowe, eThor, and established verification toolchains.","source_ids":["S5","S6","S7"]},"distinctiveness_plausibility":{"score":3,"rationale":"The clearinghouse-specific integration and seven-state authorization contract appear distinctive relative to opened sources, while component novelty and world novelty remain unmeasured.","source_ids":["S4","S5","S6","S7"]},"technical_implementability":{"score":4,"rationale":"A toy bounded implementation is credible using mature finite-state, SMT, model-checking, and proof-checking methods; production semantic fidelity and state explosion remain substantial challenges.","source_ids":["S5","S6","S7"]},"adoption_authority_feasibility":{"score":3,"rationale":"DCO governance and risk functions have relevant authority, and an offline read-only review is compatible with that structure. Production reliance would implicate listing procedures, legal review, systems safeguards, and regulator-facing obligations.","source_ids":["S2","S3"]},"evidence_readiness":{"score":2,"rationale":"Technical precedent is strong, but there is no verified DCO corpus, analyzer workflow, timeout prevalence, stakeholder commitment, or field performance evidence for the candidate.","source_ids":["S1","S4","S5","S6"]},"safety_net_benefit":{"score":5,"rationale":"Explicit UNKNOWN, OUT_OF_SCOPE, and SYSTEM_FAILURE states plus a prohibition on automatic approval directly contain the most dangerous inference error while leaving authority with the listing committee.","source_ids":["S2","S3","S6"]},"scalability":{"score":3,"rationale":"Reusable semantics, parsers, and analyzers can scale across contracts in one frozen fragment, but proof labor, abstraction refinement, semantic versioning, and state-space growth constrain expansion across products and external modules.","source_ids":["S5","S6","S7"]}},"score_confidence":"MODERATE","costs":{"first_evidence":{"band_2026_usd":"50K_TO_250K","scope":"Eight-to-twelve-week offline exercise on at most 12 de-identified contracts: formal property and toy semantics, fragment parser, exhaustive solver, one sound abstraction, reduction attempt, status record, and independent review.","confidence":"MODERATE","assumptions":["Approximately 0.3-0.6 FTE each from a formal-methods specialist and software engineer, plus part-time derivatives quant/model-risk, legal, and independent reviewer input.","Uses existing open-source solvers and no production integration.","BLS wages are increased materially for benefits, overhead, specialist scarcity, and contracting costs."],"source_ids":["S5","S7","S8"]},"initial_deployment_startup":{"band_2026_usd":"250K_TO_1M","scope":"Freeze a production-candidate DSL/compiler and settlement semantics; build corpus ingestion, enforceable fragment membership, proof and decision-record controls, security review, and governance procedures for one product family.","confidence":"LOW","assumptions":["Roughly 3-6 specialist FTE-years across engineering, formal methods, quantitative risk, legal/compliance, and assurance.","Excludes replacement of core clearing or settlement platforms.","One clearinghouse, one product family, and limited modeled oracle interfaces."],"source_ids":["S2","S3","S7","S8"]},"operational_launch":{"band_2026_usd":"1M_TO_5M","scope":"Controlled launch for one product family with production interfaces, independent validation, audit evidence, resilience testing, model governance, training, monitoring, and committee workflow integration.","confidence":"LOW","assumptions":["Requires high-assurance integration and segregation from automatic collateral or settlement action.","Includes external security/formal review and operational-resilience testing.","Does not include clearinghouse-wide platform replacement, regulatory litigation, or capital resources."],"source_ids":["S2","S3","S8"]},"annual_recurring":{"band_2026_usd":"1M_TO_5M","scope":"Ongoing formal-model maintenance, proof and abstraction review, compiler/oracle reclassification, model-risk validation, security monitoring, incident response, audit support, and committee operations.","confidence":"LOW","assumptions":["Core team of roughly 5-12 specialized staff or equivalent vendor capacity.","Every material language, compiler, oracle, or external-module change triggers review.","Specialist compensation and organizational overhead exceed published base wages."],"source_ids":["S3","S6","S8"]}},"verified_pipeline_gates":{"externally_supported_problem":{"status":"UNCERTAIN","reason":"General smart-contract, oracle, software, settlement, and operational risks are externally supported, but the exact DCO workflow—unrestricted programmable listings plus forced Boolean interpretation of timeouts—was not verified.","source_ids":["S1","S2","S3","S6"]},"externally_credible_adopter_or_authorizer":{"status":"YES","reason":"A DCO listing committee and model-risk function are credible adopters under CFTC product-eligibility, risk-management, settlement, safeguards, and governance duties; ISDA/FINOS activity confirms an adjacent industry constituency.","source_ids":["S2","S4"]},"distinct_testable_incremental_claim":{"status":"YES","reason":"The proposal makes a falsifiable comparative claim: the gate and status router should reduce unjustified Boolean clearances versus simulation-plus-timeout review while retaining useful coverage and producing no unsound SAFE verdicts.","source_ids":["S5","S6","S7"]},"bounded_next_evidence_step":{"status":"YES","reason":"A read-only exercise limited to 12 contracts, one frozen DSL/compiler, an eight-step toy horizon, finite balances, and no external calls has explicit comparators and falsifiers.","source_ids":["S5","S6","S7"]},"no_unresolved_safety_or_authority_stop":{"status":"YES","reason":"The proposed first step is offline and read-only, leaves listing authority with the committee, prohibits production actions and automatic approvals, and has clear halt conditions. Production deployment would require a new authority and safety assessment.","source_ids":["S2","S3"]},"credible_cost_scope_and_range":{"status":"YES","reason":"Scopes are bounded and order-of-magnitude ranges are consistent with multiple specialist roles anchored to current BLS wages, although deployment and recurring estimates remain low-confidence without organizational data or vendor quotes.","source_ids":["S8"]}},"next_evidence_step":"Run a partnered, offline exercise on no more than 12 frozen, de-identified contracts from one willing DCO or derivatives platform. Freeze one DSL/compiler version and a toy settlement model with two assets, eight event steps, four price intervals per asset, bounded fixed-point balances, declared oracle ranges, and no external calls. Compare (A) the existing simulation-plus-runtime-budget Boolean workflow, (B) parser-enforced exhaustive analysis, and (C) sound over-approximation with explicit UNKNOWN/POSSIBLE_BREACH. Pre-register outcomes: fragment coverage; exact and abstract runtimes; false-alarm rate against exhaustive bounded truth; rate of UNKNOWN/OUT_OF_SCOPE; number of baseline Boolean approvals lacking a certificate; and downstream label preservation. Independently check the unrestricted reduction direction, semantic preservation, parser enforcement, termination/correctness argument, and abstraction soundness. Falsify the intervention if any concrete bounded breach receives SAFE, fragment checks are bypassable, labels collapse downstream, or fewer than 3 of 12 economically faithful cases receive a usable certified result. Falsify the stated problem if audited current workflow already enforces a total bounded language and never converts timeout, unsupported input, or analysis failure into a semantic verdict.","blocking_evidence":["No public evidence verifies that a clearinghouse currently admits the candidate's unrestricted programmable-contract class.","No public evidence verifies a Boolean analyzer interface that converts timeouts or unsupported features into solvency decisions.","No de-identified contract corpus, production compiler semantics, oracle contract, or settlement implementation was available.","No adopter commitment, procurement owner, budget, or regulator consultation specific to this intervention was found.","The proposed halting-style reduction has not been constructed or independently checked for an actual contract language.","Fragment coverage, sound-abstraction precision, analyst usability, and downstream label preservation require proprietary data and live organizational testing.","Legal enforceability, model-risk classification, and production change-control requirements remain jurisdiction- and clearinghouse-specific.","Cost ranges lack clearinghouse-specific staffing plans, integration estimates, and vendor quotations."],"research_disposition":"PARTNERED_RESEARCH_PROGRAM","world_novelty_boundary":"World novelty, patentability, freedom to operate, market size, and realized impact were not measured. The search establishes only that restricted financial-contract DSLs, exhaustive analysis, sound incomplete static analysis, smart-contract verification tools, standardized executable derivatives models, and FMI risk governance are existing adjacent art; it does not establish whether the proposed integrated DCO computability gate has or has not been implemented elsewhere.","arm":"COMPLETE_PROPOSAL_PORTFOLIO","candidate_version":0,"controller_recommendation":{"action":"STOP_EMPIRICAL_RESEARCH_NEEDED","repairable":false,"material_progress_observed":true,"progress_targets":["Obtain a willing DCO or derivatives-platform partner and a frozen de-identified corpus of up to 12 representative contract programs.","Audit whether current workflow distinguishes timeout, unsupported input, analyzer failure, unknown, and semantic failure.","Freeze executable settlement, numeric, oracle, event-horizon, and compiler semantics for one product family.","Construct and independently check the unrestricted-class reduction rather than relying on a halting-problem analogy.","Measure parser enforcement, certified-result coverage, runtime, abstraction false alarms, and any unsound SAFE result against bounded exhaustive truth.","Demonstrate that all seven result labels survive storage, analyst display, committee review, and audit export without Boolean promotion.","Obtain legal/model-risk review of authority, records, and production change-control obligations.","Replace broad resource-equivalent estimates with partner staffing estimates and at least one independent implementation quotation."],"reason":"Web research establishes meaningful adjacent risk, credible authority, and technical precedent, but cannot verify the candidate's central operational premise or its comparative performance. Those questions require proprietary workflow observation, a real contract corpus, independent proof work, and offline testing. Under the controller rule, that requires STOP_EMPIRICAL_RESEARCH_NEEDED; all STOP recommendations are non-repairable within this web-evaluation cycle."},"proposal_index":1}