{"schema_version":1,"experiment_id":"eoa_inverse_innovation_exp11_mechanism_context_external20_20260804","research_id":"eoa_inverse_innovation_exp11_external_scrutiny_20260804","cell_id":"computability_boundary_mapping__economics_finance","opaque_id":"computability_boundary_mapping__economics_finance__C","search_lanes":{"direct_problem":{"queries":["algorithmic trading strategy verification undecidable solvency all market paths","smart contract \"solvency\" formal verification all executions balance invariant","venue pre-deployment classifier trading strategy safe unsafe formal verification","financial regulator algorithmic trading pre deployment testing controls venue approval official"],"source_ids":["S3","S4","S6","S7"],"no_result_note":"The searches established real algorithmic-trading control failures and verification limits, but found no public evidence that a supervisor or venue currently demands an exact terminating Boolean solvency classifier for every arbitrary program and market path."},"closest_prior_art":{"queries":["automated verifier financial smart contracts balance safety unknown timeout bounded model checking","Solvent liquidity verification smart contracts every reachable state timeout","Clockwork Finance automated analysis economic security smart contracts","smart contract verification unknown timeout sound incomplete static analysis"],"source_ids":["S2","S3","S7","S8"],"no_result_note":null},"historical_terminology":{"queries":["Turing 1936 computable numbers Entscheidungsproblem original paper pdf","program verification circle-free machine general process finite number steps","smart contract liquidity solvency enabledness verification","formal verification finance trading algorithms solvency"],"source_ids":["S1","S7"],"no_result_note":null},"products_practices_standards":{"queries":["Solidity SMTChecker unknown timeout unsupported features soundness","EUR-Lex 2017/589 algorithmic trading testing validation report Article 5 6 9","FCA multi-firm algorithmic trading controls testing controlled deployment","smart contract formal verification product bounded model checking timeout"],"source_ids":["S2","S3","S4","S5"],"no_result_note":null},"non_english_regional":{"queries":["site:bafin.de algorithmischer Handel Tests Systeme Algorithmen Risikokontrollen","site:amf-france.org trading algorithmique tests algorithmes risques déploiement","検証 アルゴリズム取引 システム リスク 管理 テスト 金融庁","contrat intelligent vérification formelle indécidable délai inconnu"],"source_ids":["S6"],"no_result_note":null},"composition_subproblems":{"queries":["trading algorithm \"solvent\" model checking formal verification","smart contract solvency external oracle formal model bounded paths timeout","algorithmic trading formal verification offline testing approval audit limits","unknown timeout out-of-scope safe unsafe formal verification financial software"],"source_ids":["S2","S4","S5","S7","S8"],"no_result_note":null}},"sources":[{"source_id":"S1","title":"On Computable Numbers, with an Application to the Entscheidungsproblem","url":"https://zanotti.univ-tln.fr/turing/turing-1936.pdf","publisher":"Proceedings of the London Mathematical Society","date_or_year":"1936–1937","source_type":"PRIMARY_RESEARCH","language":"English","claims_supported":["Turing defines a machine model and proves that no general finite process decides whether an arbitrary machine is circle-free.","The result supports a general computability boundary but does not itself prove that the proposal's financial solvency predicate preserves an undecidable problem."]},{"source_id":"S2","title":"SMTChecker and Formal Verification — Solidity documentation","url":"https://docs.solidity.org/en/latest/smtchecker.html","publisher":"Solidity Project","date_or_year":"2026 (Solidity 0.8.37 development documentation)","source_type":"FIRST_PARTY_PRODUCT","language":"English","claims_supported":["The production tool distinguishes proved failure from a timeout-induced unknown and reports the latter conservatively as a potential failure.","The tool exposes resource limits, timeouts, unproved targets, unsupported language features, and sound over-approximation.","It checks insufficient funds for transfers but states that general automatic verification can be impossible or remain unsolved."]},{"source_id":"S3","title":"Formal verification of smart contracts","url":"https://ethereum.org/developers/docs/smart-contracts/formal-verification/","publisher":"ethereum.org","date_or_year":"2026-06-26","source_type":"OFFICIAL_GUIDANCE","language":"English","claims_supported":["Smart-contract verification is specification-relative and includes balance, transfer, safety, and liquidity properties.","Finite-state model checking, infinite-state theorem proving, abstraction, human assistance, and undecidability are recognized alternatives and limitations.","Poor specifications can create false assurance, and some well-specified properties cannot be proved automatically."]},{"source_id":"S4","title":"Multi-firm review of algorithmic trading controls: high-level observations","url":"https://www.fca.org.uk/publications/multi-firm-reviews/algorithmic-trading-controls-high-level-observations","publisher":"UK Financial Conduct Authority","date_or_year":"2025-08-21","source_type":"OFFICIAL_GUIDANCE","language":"English","claims_supported":["The FCA identifies inherent algorithmic-trading risks and current weaknesses in testing, documentation, ownership, and oversight.","Firms use stress scenarios, phased controlled deployment, pre-trade limits, escalation, and senior approval.","Observed practice is risk-based testing and controls, not a universal exact solvency classifier."]},{"source_id":"S5","title":"Commission Delegated Regulation (EU) 2017/589 on organisational requirements for investment firms engaged in algorithmic trading","url":"https://eur-lex.europa.eu/legal-content/EN/TXT/?uri=CELEX%3A32017R0589","publisher":"European Union, Official Journal / EUR-Lex","date_or_year":"2017-03-31","source_type":"OFFICIAL_STANDARD","language":"English","claims_supported":["A senior-management designee authorizes deployment or substantial updates of trading algorithms.","Testing must occur in a separated environment, deployment must have predefined limits, and material changes must be recorded.","Risk management, internal audit, and senior management have defined validation and approval roles, identifying adopters and authorizers.","The regulation requires stress testing, surveillance, and kill functionality but does not promise proof over every market path."]},{"source_id":"S6","title":"金融商品取引業者等に対する検査における主な指摘事項 (Principal findings from inspections of financial instruments business operators)","url":"https://www.fsa.go.jp/sesc/actions/shiteki.pdf","publisher":"Securities and Exchange Surveillance Commission, Financial Services Agency of Japan","date_or_year":"2011 (covering inspections from 2007 through March 2011)","source_type":"OFFICIAL_GUIDANCE","language":"Japanese","claims_supported":["Japanese inspections documented mass erroneous orders from algorithmic trading where preventive order limits were inadequate and program consistency failed during system updates.","Other findings documented missing requirements, inadequate monitoring, repeated system failures, and audits declaring no problem without sufficient evidence.","These findings establish operational risk and governance failures, but not demand for a universal solvency decider."]},{"source_id":"S7","title":"Solvent: liquidity verification of smart contracts","url":"https://arxiv.org/pdf/2404.17864","publisher":"arXiv; authors from the Universities of Cagliari, Modena and Reggio Emilia, Genoa, and Télécom Paris","date_or_year":"2024-09-23","source_type":"PRIMARY_RESEARCH","language":"English","claims_supported":["Solvent verifies a close financial property: whether, from every reachable state, a user has a bounded transaction sequence that withdraws specified assets.","It deliberately accepts a purified Solidity fragment and reports violation, unbounded proof, bounded proof X(N), and timeout as distinct results.","Its evaluation uses a fixed CPU-time bound and acknowledges undecidable nonlinear arithmetic, timeouts, abstraction limits, and semantic gaps such as reentrancy.","This is close prior art for model-relative solvency/liquidity analysis with bounded guarantees and explicit non-results."]},{"source_id":"S8","title":"Clockwork Finance: Automated Analysis of Economic Security in Smart Contracts","url":"https://eprint.iacr.org/2021/1147.pdf","publisher":"IACR Cryptology ePrint Archive","date_or_year":"2021 (subsequently revised)","source_type":"PRIMARY_RESEARCH","language":"English","claims_supported":["Clockwork Finance formalizes economic-security properties for composed DeFi contracts and reasons over formal contract and adversary models.","It uses over-approximation, concrete counterexample validation, and explicitly model-relative assumptions.","Its evaluation exhaustively explores only tractable bounded cases and uses randomized partial search for larger cases, demonstrating the practical boundary between proof and incomplete search."]}],"problem_evidence":{"status":"PARTLY_SUPPORTED","finding":"The underlying operational problem is real: regulators report algorithmic-trading failures and control weaknesses, while smart-contract verifiers encounter undecidability, abstraction gaps, unsupported features, and timeouts. However, the proposal's sharper institutional diagnosis—that supervisors or venues seek a universal exact terminating solvency classifier or collapse unknown into a Boolean decision—was not found in the retained public evidence. Current regulatory sources instead prescribe scoped testing, limits, surveillance, human accountability, and kill controls.","source_ids":["S2","S3","S4","S6","S7"],"uncertainty":"Public rules and supervisory reviews may not expose internal procurement requirements, tool interfaces, or how staff interpret timeout and abstention. No interviews, proprietary venue manuals, or non-public validation reports were examined."},"adopter_evidence":{"status":"SUPPORTED","finding":"Investment firms, venue-facing risk and compliance functions, internal audit, and senior management are identifiable adopters. EU RTS 6 assigns deployment authorization to a senior-management designee and validation to risk management, internal audit, and senior management; the FCA documents those roles in current firm practice.","source_ids":["S4","S5"],"uncertainty":"The legally empowered decision maker varies by jurisdiction and firm. The sources identify governance roles for algorithm deployment, not a named owner for the proposed computability classification artifact."},"implementation_evidence":{"status":"PARTLY_SUPPORTED","finding":"Most technical and governance components already have demonstrated implementations: Solidity and Solvent distinguish proof, failure, bounded proof, unknown, timeout, and unsupported scope; Clockwork uses model-relative abstraction and incomplete search; EU and FCA materials require separated testing, limits, records, approval, audit, and controlled deployment. The exact combined workflow—computability proof review plus machine-enforced fragment admission and a user-interpretation pilot—was not found as an operational financial-supervision system.","source_ids":["S2","S4","S5","S7","S8"],"uncertainty":"No evidence establishes that a faithful reduction exists for arbitrary executable strategies with stochastic real-valued markets and external oracles. Integration cost, enforceability of the fragment gate, and user comprehension remain untested."},"prior_art":{"disposition":"ADJACENT_PRIOR_ART","closest_analogues":[{"name":"Solvent liquidity verifier","source_ids":["S7"],"same_problem":true,"same_causal_lever":true,"overlap":"It addresses contract liquidity/solvency over reachable states through a restricted language, formal property specification, bounded and unbounded verification, replayable counterexamples, timeout, and separate bounded-proof outcomes.","remaining_difference":"It does not cover arbitrary trading strategies and exogenous market paths, prove the unrestricted financial task undecidable, enforce venue admission policy, or test whether institutional users correctly interpret the result states."},{"name":"Solidity SMTChecker","source_ids":["S2"],"same_problem":false,"same_causal_lever":true,"overlap":"It operationalizes conservative, model-relative verification with distinct failure, unknown/timeout, unproved, and unsupported-feature handling, including insufficient-balance targets.","remaining_difference":"It is a compiler tool for specified contract properties, not a supervisor-facing solvency boundary map with admission governance, independent proof review, or a comprehension pilot."},{"name":"Clockwork Finance","source_ids":["S8"],"same_problem":false,"same_causal_lever":true,"overlap":"It formalizes DeFi economic security under explicit models, uses over-approximation and validation, proves bounds in tractable cases, and falls back to partial randomized search for intractable cases.","remaining_difference":"Its target is extractable value under modeled transaction compositions rather than universal solvency under every admissible external market path, and it does not supply the proposed regulatory status and authorization workflow."},{"name":"EU RTS 6 algorithmic-trading testing and governance workflow","source_ids":["S4","S5"],"same_problem":false,"same_causal_lever":false,"overlap":"It already supplies separated testing, controlled deployment, predefined scope limits, change records, validation reports, audit, named authorization, re-testing, surveillance, and rollback-like kill functionality.","remaining_difference":"It manages operational and conduct risk through testing and controls rather than classifying computability or distinguishing formal unknown from false."}],"contrastive_claim_remaining":"Conditional on first finding a venue workflow that currently collapses verifier outcomes, adding an enforced supported-fragment gate and visibly distinct proven-safe, proven-unsafe, bounded-only, timeout/unknown, out-of-scope, and system-failure states will reduce false Boolean interpretations without increasing unsound admissions, compared with the venue's existing pre-deployment interface.","contrastive_claim_falsifier":"The incremental claim is falsified if a preregistered blinded comprehension test and independent-label audit show no reduction in false safe/unsafe interpretations, any increase in unsound admissions, failure to enforce the supported fragment, or no baseline workflow that collapses these states.","confidence":"HIGH","search_limitations":"This was a bounded public-web search using eight retained sources. It did not inspect proprietary venue systems, confidential supervisory files, patents, source-code histories beyond the retained documentation, or conduct stakeholder interviews. The search cannot establish world novelty, patentability, freedom to operate, market size, or realized impact."},"researchability_gates":{"externally_supported_problem":{"status":"FAIL","rationale":"Operational algorithmic risk and verifier limitations are supported, but the defining institutional problem—an actual requirement for a universal exact terminating solvency Boolean or actual collapse of unknown into safe/unsafe—was not externally demonstrated. Official sources instead show bounded testing and controls.","source_ids":["S2","S4","S5","S6","S7"]},"identifiable_adopter_or_authorizer":{"status":"PASS","rationale":"EU rules and FCA observations identify investment-firm risk, compliance, audit, senior-management, and designated deployment-authorization roles that could own a bounded offline evaluation.","source_ids":["S4","S5"]},"distinct_testable_incremental_claim":{"status":"PASS","rationale":"Despite close technical and regulatory prior art, a narrow institutional claim remains testable: whether combining enforceable fragment scope with a richer result taxonomy improves decision-maker comprehension and avoids false Boolean resolution. None of the retained sources reports that comparison.","source_ids":["S2","S5","S7"]},"bounded_next_evidence_step":{"status":"PASS","rationale":"A fixed-scope document and interface audit can examine one venue's requirements and a versioned sample of verifier outputs, followed only if warranted by a preregistered offline comprehension test using labeled specimens and no live capital.","source_ids":["S4","S5","S7"]},"no_unresolved_safety_or_authority_stop":{"status":"PASS","rationale":"A read-only requirements audit and offline test are within identifiable firm governance. Live admission, live trading, and regulatory-policy changes remain excluded and would require separately empowered authorization.","source_ids":["S4","S5"]},"adequate_search_evidence":{"status":"PASS","rationale":"All six required lanes were searched adversarially, including foundational terminology, deployed tools, official standards and current practice, Japanese/French/German terminology, and combinations of solvency, path quantification, formal verification, timeout, scope, and governance. Exactly eight sources were retained and opened; they include multiple independent publishers and seven primary, official, standards, or first-party sources.","source_ids":["S1","S2","S3","S4","S5","S6","S7","S8"]}},"strict_success":false,"screen_survival":false,"remaining_research_value":"MODERATE","recommended_next_step":"Before building the proposed classifier workflow, conduct a time-boxed, read-only requirements audit at one willing venue or supervised firm: collect a fixed versioned sample of pre-deployment requirements, tool outputs, timeout handling, and escalation records; code whether any universal Boolean promise or state collapse actually occurs; obtain legal and risk-owner review; then run the offline comprehension pilot only if that prerequisite is observed.","world_novelty_boundary":"The bounded search found close prior art for restricted, model-relative contract solvency/liquidity verification with bounded proofs and timeout states, plus established regulatory testing and governance controls. It did not find the exact combined supervisor-facing workflow or evidence of its alleged baseline demand. This supports only an adjacent, conditional incremental claim and does not establish world novelty, patentability, freedom to operate, market size, or impact."}