{"schema_version":1,"research_id":"eoa_inverse_innovation_exp05_external_evaluation_20260803","source_assessment_id":"computability_boundary_mapping__economics_finance:P2:v0","cell_id":"computability_boundary_mapping__economics_finance","search_queries":["formal verification auction mechanisms dominant strategy truthfulness executable auction rules paper","proof carrying code certificate checker auction mechanism formal verification","CFTC exchange rule self certification auction algorithm rules 17 CFR Part 40 official","automated mechanism verification incentive compatibility undecidable paper","auction smart contract vulnerability formal verification empirical paper auction bug","smart contract auction attacks vulnerability paper formal verification auction","online advertising auction mechanism automated verification incentive compatibility real deployment","formal verification auction smart contract truthfulness dominant strategy checker"],"sources":[{"source_id":"S1","title":"Provisions Common to Registered Entities; Final Rule","publisher":"U.S. Commodity Futures Trading Commission","url":"https://www.cftc.gov/LawRegulation/FederalRegister/finalrules/2024-24388.html","source_class":"GOVERNMENT_OR_REGULATOR","publication_date":"2024-11-07","accessed_at":"2026-08-03","claims_supported":["CFTC Part 40 governs registered entities' submission and self-certification of rules, rule amendments, and products before implementation or listing.","Registered entities include designated contract markets, derivatives clearing organizations, swap execution facilities, and swap data repositories.","The 2024 amendments require submissions complete enough to support CFTC compliance analysis, identifying both regulated authorizers and an established rule-admission workflow."]},{"source_id":"S2","title":"How Open Bidding works","publisher":"Google Ad Manager Help","url":"https://support.google.com/admanager/answer/7128958?hl=en","source_class":"OFFICIAL_PRODUCT_DOCUMENTATION","publication_date":"undated","accessed_at":"2026-08-03","claims_supported":["Google operates a real-time unified auction involving Ad Exchange, third-party exchanges, networks, direct line items, reserve prices, and dynamic allocation.","The documented nested-auction workflow demonstrates that executable, automated marketplace allocation rules exist in deployed commercial systems.","Google and participating publishers or exchanges are identifiable potential operators, although the source does not request proof-carrying admission."]},{"source_id":"S3","title":"A Proof-Carrying Code Approach to Certificate Auction Mechanisms","publisher":"University of Liverpool and Xi'an Jiaotong-Liverpool University","url":"https://cgi.csc.liv.ac.uk/~trp/Publications_files/FACS2013Revise.pdf","source_class":"PRIMARY_RESEARCH","publication_date":"2013","accessed_at":"2026-08-03","claims_supported":["The authors proposed and implemented a proof-carrying-code framework in Coq for machine-checkable certification of auction properties.","Their auctioneer publishes an auction specification and proof, while a consumer-side checker verifies the proof.","They demonstrated strategy-property certification for English and Vickrey auctions, creating a direct prior-art collision with the proposal's central proof-carrying-auction concept.","The reported implementation remained a research framework with further auction-house and ontology implementation left as future work."]},{"source_id":"S4","title":"Computer-aided Verification in Mechanism Design","publisher":"arXiv; related proceedings publication by Springer","url":"https://arxiv.org/abs/1502.04052","source_class":"PRIMARY_RESEARCH","publication_date":"2015-02-13","accessed_at":"2026-08-03","claims_supported":["Incentive-compatibility proofs can be complex and tedious to check and may require mechanism-design experts.","Machine-checkable formal proofs of incentive properties are technically feasible.","The authors formally verified incentive compatibility for VCG and a sophisticated randomized Bayesian mechanism family, showing that randomness and type distributions can be formalized but create additional obligations."]},{"source_id":"S5","title":"Towards Automated Verification of Smart Contract Fairness","publisher":"Association for Computing Machinery","url":"https://www3.ntu.edu.sg/home/yi_li/files/Liu2020TAV.pdf","source_class":"PRIMARY_RESEARCH","publication_date":"2020-11-08","accessed_at":"2026-08-03","claims_supported":["FairCon semi-automatically checks or proves truthfulness, efficiency, optimality, and collusion-freeness for Ethereum smart contracts.","The evaluation used 12 distinct real auction contracts; eight failed all four tested fairness properties with manually confirmed counterexamples, while only selected properties of four contracts held.","Bounded checking used three bidders, demonstrating that finite counterexample testing is useful but model-relative.","Manual annotation and harness instrumentation for 17 contracts required six human hours, while automated checks were fast, indicating that specification effort rather than checking alone is material.","The framework already combines checked counterexamples and proofs, substantially overlapping the proposed evidence interface."]},{"source_id":"S6","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":["Testing sampled inputs cannot prove correctness for untested inputs.","Automated theorem provers cannot always determine decidability and often require human guidance.","Formal verification is labor-intensive, specification-sensitive, subject to state or path explosion, and may fail to prove true properties.","A proof establishes correspondence only to the formal specification; an inadequate specification can create false confidence.","Ethereum documents multiple existing verification tools, making checker construction technically credible but not novel."]},{"source_id":"S7","title":"Testing Dynamic Incentive Compatibility in Display Ad Auctions","publisher":"ACM SIGKDD","url":"https://www.kdd.org/kdd2019/accepted-papers/view/testing-dynamic-incentive-compatibility-in-display-ad-auctions","source_class":"PRIMARY_RESEARCH","publication_date":"2019","accessed_at":"2026-08-03","claims_supported":["Transparency in complex black-box display-ad auctions is described as a point of contention between buyers and sellers.","The authors developed statistical incentive-compatibility tests based on bid perturbations and evaluated them using data from a major ad exchange.","Statistical field tests are a practical comparator that addresses deployed behavior but do not provide class-wide source-rule certificates."]},{"source_id":"S8","title":"Decidable Verification of Uninterpreted Programs","publisher":"arXiv; Proceedings of the ACM on Programming Languages","url":"https://arxiv.org/abs/1811.00192","source_class":"PRIMARY_RESEARCH","publication_date":"2018-11-01","accessed_at":"2026-08-03","claims_supported":["Completely automatic verification of the studied unrestricted program class is undecidable.","The authors identify mechanically recognizable coherent and k-coherent subclasses with decidable verification, including results for recursion.","The work supports separating unrestricted verification from enforceable decidable fragments, but it does not itself prove the proposal's auction-specific combined-property reduction."]}],"problem_evidence":{"support":"MODERATE","rationale":"Deployed platforms run complex nested auctions, researchers identify transparency and incentive-modeling concerns, and FairCon found checked fairness counterexamples in real auction contracts. General verification sources also confirm that sampling and unsuccessful proof search cannot establish universal properties. However, no source documents the proposal's exact claimed failure mode: a marketplace currently converting timeout into a Boolean truthfulness verdict for unrestricted submitted auction programs.","source_ids":["S2","S4","S5","S6","S7","S8"]},"stakeholder_evidence":{"support":"MODERATE","rationale":"CFTC-regulated exchanges have identifiable rule-submission and authorization processes, and Google, publishers, exchanges, and advertisers participate in deployed automated auctions. CFTC requires compliance-supporting submissions, while the KDD study records buyer-seller demand for auction transparency. No identified operator or regulator explicitly requests proof-carrying termination-and-truthfulness certificates or commits resources to this protocol.","source_ids":["S1","S2","S7"]},"prior_art":{"proximity":"SUBSTANTIAL_COLLISION","closest_analogues":[{"name":"Proof-Carrying Code Approach to Certificate Auction Mechanisms","similarity":"Directly proposes producer-supplied, machine-checkable auction-property proofs and consumer-side checking in Coq, including strategy properties for English and Vickrey auctions.","remaining_difference":"It does not present the candidate's regulated admission board, joint termination-plus-dominant-strategy property for arbitrary stateful executable rules, six-state operational output contract, checked undecidability reduction, or version-triggered invalidation workflow.","source_ids":["S3"]},{"name":"FairCon automated smart-contract fairness verification","similarity":"Checks real auction contracts for truthfulness and other fairness properties, generates concrete counterexamples, and proves selected properties using synthesized invariants.","remaining_difference":"It is an analysis framework rather than a submitter-carried certificate admission protocol, and its counterexample experiments are explicitly bounded by modeled participant configurations.","source_ids":["S5"]},{"name":"Computer-aided verification in mechanism design","similarity":"Constructs automatically checkable formal incentive-compatibility proofs for sophisticated and randomized mechanisms.","remaining_difference":"It focuses on formalizing particular mechanisms and theorems rather than governing open-ended executable-rule submissions with explicit unknown and out-of-model states.","source_ids":["S4"]},{"name":"Statistical testing of dynamic incentive compatibility","similarity":"Tests incentive compatibility in a deployed major ad exchange and responds to auction-transparency concerns.","remaining_difference":"It provides empirical evidence about black-box deployed behavior, not a model-relative universal certificate for submitted source rules.","source_ids":["S7"]},{"name":"Decidable coherent-program verification","similarity":"Maps a boundary between undecidable general program verification and enforceable decidable subclasses.","remaining_difference":"It does not cover auction utility semantics or prove the proposed computation-to-auction reduction; it instead strengthens the fixed-fragment comparator.","source_ids":["S8"]}],"distinctive_claim_remaining":"Relative to the 2013 proof-carrying auction framework and later auction-verification systems, the remaining testable increment is a governed admission workflow for stateful executable rules that jointly checks termination and dominant-strategy truthfulness, preserves CERTIFIED, REFUTED, UNKNOWN, OUT_OF_MODEL, INVALID_CERTIFICATE, and SYSTEM_FAILURE, and invalidates certificates on model-version change. In a preregistered synthetic exercise, it should accept every planted valid certificate, reject every planted invalid certificate or in-model counterexample, terminate on every certificate input, and produce fewer false binary dispositions than the current simulation-plus-Boolean baseline. Any accepted invalid proof, collapsed timeout label, checker nontermination, or formal/executable semantic mismatch falsifies that claim.","confidence":"HIGH"},"implementation_evidence":{"support":"STRONG","rationale":"Coq proof-carrying auction certification has already been implemented; computer-aided mechanism proofs and FairCon demonstrate checkable incentive properties and counterexamples; Ethereum guidance documents mature verification tools and known specification, labor, and decidability limits. The components are technically credible, but the proposal's combined reduction, total certificate grammar, semantic correspondence, and production workflow have not been built or checked.","source_ids":["S3","S4","S5","S6","S8"]},"scores":{"meaningful_impact":{"score":4,"rationale":"Incorrect incentive or execution properties can affect automated transactions, while real contract experiments found numerous fairness failures; actual impact for the proposed admission population is unmeasured.","source_ids":["S2","S5","S7"]},"stakeholder_pull":{"score":3,"rationale":"There are identifiable platform operators, market participants, exchange rule submitters, and regulators with transparency or compliance needs, but no adopter has requested this specific protocol.","source_ids":["S1","S2","S7"]},"incremental_advantage":{"score":2,"rationale":"Explicit status separation and joint termination-plus-truthfulness governance could improve a Boolean workflow, but proof-carrying auction certificates, checked incentive proofs, and proof/counterexample systems already exist.","source_ids":["S3","S4","S5"]},"distinctiveness_plausibility":{"score":2,"rationale":"A narrow workflow-level increment remains, but the central technical concept substantially collides with published research.","source_ids":["S3","S5"]},"technical_implementability":{"score":4,"rationale":"Existing implementations establish feasibility of certificate checking and auction-property verification; the main uncertainty is specification correspondence and coverage for unrestricted rule languages.","source_ids":["S3","S4","S5","S6"]},"adoption_authority_feasibility":{"score":3,"rationale":"Exchange and platform rule-governance bodies are plausible authorities, and an offline synthetic pilot is within ordinary internal authority, but the generic marketplace has no named committed sponsor.","source_ids":["S1","S2"]},"evidence_readiness":{"score":4,"rationale":"The six-rule offline exercise can produce objective checker, label, proof, and counterexample results without production data; the auction-specific reduction still needs independent mathematical review.","source_ids":["S3","S5","S8"]},"safety_net_benefit":{"score":4,"rationale":"An explicit UNKNOWN/OUT_OF_MODEL path and sandboxed offline testing reduce the risk of treating incomplete analysis as clearance, consistent with documented prover and specification limits.","source_ids":["S6","S8"]},"scalability":{"score":3,"rationale":"Certificate checking can be cheap, but proof construction, specification work, and state/path explosion can constrain submission coverage and recurring review throughput.","source_ids":["S3","S5","S6"]}},"score_confidence":"MODERATE","costs":{"first_evidence":{"band_2026_usd":"10K_TO_50K","scope":"A two-to-four-week offline exercise covering six synthetic rules, a frozen bounded economic model, one minimal checker, planted proofs and counterexamples, label-propagation tests, and independent review.","confidence":"LOW","assumptions":["Uses existing open-source proof assistants and verification infrastructure.","Requires roughly two to six specialist person-weeks split among a formal-methods engineer, mechanism designer, and independent reviewer.","Excludes production integration, confidential bids, legal opinions, and live-market experiments.","The source set supports the labor-intensive character of specification but contains no 2026 compensation quote."],"source_ids":["S3","S5","S6"]},"initial_deployment_startup":{"band_2026_usd":"250K_TO_1M","scope":"Harden a certificate grammar and checker, formalize one marketplace rule language and economic model, establish reproducible builds and sandboxing, commission independent kernel and semantic-correspondence review, and define admission governance.","confidence":"LOW","assumptions":["Six to twelve months for a small cross-functional team.","One rule language and one declared incentive model only.","No automated production approval authority.","Cost includes security and independent proof review but not platform-wide rule migration."],"source_ids":["S1","S3","S6"]},"operational_launch":{"band_2026_usd":"1M_TO_5M","scope":"Production-grade integration with submission, artifact storage, audit logging, version invalidation, sandbox execution, access control, monitoring, incident response, reviewer training, and staged rollout for one marketplace.","confidence":"LOW","assumptions":["Integration occurs in an established marketplace with existing admission and identity systems.","Requires formal-methods, economics, security, platform, compliance, and operations participation.","Launch remains advisory to the admission board rather than an autonomous deployment gate.","No estimate for transaction losses, regulatory capital, or bidder compensation is included."],"source_ids":["S1","S2","S6"]},"annual_recurring":{"band_2026_usd":"250K_TO_1M","scope":"Maintain the checker and specifications, review certificates and model changes, independently revalidate releases, operate sandboxes and logs, and investigate inconsistencies for one marketplace.","confidence":"LOW","assumptions":["Two to five resource-equivalent specialist FTEs plus periodic external review.","Submission volume is moderate and proof generation remains primarily the submitter's responsibility.","Major language or economic-model changes would be separately funded.","No source provides observed recurring cost for a comparable production service."],"source_ids":["S3","S6"]}},"verified_pipeline_gates":{"externally_supported_problem":{"status":"YES","reason":"Independent research and first-party documentation show deployed complex auctions, real auction-contract fairness failures, transparency concerns, and the inability of sampled tests to prove universal properties. The exact timeout-to-Boolean practice remains unverified.","source_ids":["S2","S5","S6","S7"]},"externally_credible_adopter_or_authorizer":{"status":"YES","reason":"Marketplace operators and publishers are identifiable operators, while CFTC-regulated exchanges and the CFTC provide a concrete rule-submission and authorization structure. Specific commitment to this intervention is absent.","source_ids":["S1","S2"]},"distinct_testable_incremental_claim":{"status":"YES","reason":"Despite substantial prior-art collision, the joint-property admission workflow, six-state label preservation, terminating checker obligation, and version invalidation can be tested against explicit comparators and falsifiers.","source_ids":["S3","S5","S6"]},"bounded_next_evidence_step":{"status":"YES","reason":"A synthetic six-rule, non-production exercise can test proof acceptance, counterexample handling, termination, semantic correspondence, and label propagation within a fixed schedule and dataset.","source_ids":["S3","S5"]},"no_unresolved_safety_or_authority_stop":{"status":"YES","reason":"The proposed first step is offline, synthetic, sandboxed, reversible, and excluded from bids, payments, deployment, and production admission decisions. Existing regulatory authority remains with the marketplace and applicable regulator.","source_ids":["S1","S6"]},"credible_cost_scope_and_range":{"status":"UNCERTAIN","reason":"The four ranges have bounded scopes and explicit staffing assumptions, and sources confirm meaningful specialist labor. No direct 2026 wage, vendor-price, or comparable-production cost evidence was found, so the monetary bands remain low-confidence resource-equivalent estimates.","source_ids":["S5","S6"]}},"next_evidence_step":"Preregister and run a four-week offline benchmark on six synthetic rules: two planted total-and-truthful rules with independently authored certificates, one profitable-misreport rule, one divergent rule, one malformed-certificate rule, and one unrestricted-language specimen used in the proposed reduction. Compare (A) the current sampled-simulation plus forced-Boolean review, (B) a finite-catalog or bounded exhaustive checker, and (C) the proof-carrying six-state protocol. Measure false CERTIFIED/REFUTED decisions, UNKNOWN and OUT_OF_MODEL rates, checker termination, certificate-check latency, expert hours, proof size, semantic-correspondence failures, and downstream label preservation. Require a reviewer independent of the checker author to check reduction direction and both implications, certificate soundness, executable/formal correspondence, and every status transition. Falsify the intervention if any invalid certificate is accepted, any valid-syntax certificate makes the checker fail to terminate, an accepted certificate is contradicted by an in-model checked counterexample, formal and executable outputs diverge, labels collapse downstream, or all eligible positive cases remain UNKNOWN. No production rule, bid, payment, proprietary bidder data, or admission decision enters the exercise.","blocking_evidence":["No independently checked reduction establishes undecidability of the exact frozen joint TOTAL_AND_TRUTHFUL property for the proposed auction-rule language.","No prototype demonstrates that the certificate checker terminates on every certificate in its declared syntax and rejects all planted invalid proofs.","No executable-to-formal semantic-correspondence test has shown that a certificate covers the behavior actually run by a marketplace.","No comparative exercise shows that six-state proof-carrying review reduces false binary dispositions relative to sampled simulation, bounded exhaustive checking, or manual review.","No evidence measures certificate expressiveness, submitter burden, UNKNOWN rates, or reviewer throughput for representative expressive auction rules.","No marketplace or regulated exchange has committed to sponsor, adopt, or authorize the protocol.","No direct 2026 cost benchmark supports the resource-equivalent monetary ranges."],"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 a direct 2013 proof-carrying auction-certificate analogue and multiple later formal or empirical auction-verification approaches, so no novelty claim should attach to proof-carrying auction certification itself. Only the narrower combined-property, multi-status, version-governed admission workflow remains available for contrastive testing, and this evaluation does not establish that even that combination is globally novel.","arm":"COMPLETE_PROPOSAL_PORTFOLIO","candidate_version":0,"controller_recommendation":{"action":"STOP_EMPIRICAL_RESEARCH_NEEDED","repairable":false,"material_progress_observed":true,"progress_targets":["Obtain an independently checked reduction for the exact frozen rule language and TOTAL_AND_TRUTHFUL property, or narrow the claim to unresolved.","Demonstrate total checker termination and zero acceptance of planted invalid certificates in the six-rule benchmark.","Demonstrate formal/executable semantic correspondence under the same versioned model.","Compare six-state proof-carrying review against forced-Boolean simulation/manual review and bounded exhaustive checking using preregistered error and labor measures.","Measure certificate coverage, UNKNOWN rate, authoring effort, checking latency, and reviewer throughput.","Secure a named marketplace or regulated-exchange sponsor for a non-production evaluation.","Replace low-confidence resource estimates with observed pilot labor and integration costs."],"reason":"Bounded web research found both external support for the problem and substantial collision with proof-carrying auction certification and automated fairness verification. The decisive remaining questions concern checker behavior, semantic correspondence, workflow error rates, certificate burden, and adopter willingness; these require artifact construction, independent proof review, and controlled field or laboratory evidence rather than more web search. Under the controller rule, this empirical-research stop is terminal and therefore marked not repairable."},"proposal_index":2}