{"schema_version":1,"research_id":"eoa_inverse_innovation_exp05_external_evaluation_20260803","source_assessment_id":"computability_boundary_mapping__veterinary_medicine:P4:v0","cell_id":"computability_boundary_mapping__veterinary_medicine","search_queries":["site:woah.org animal health surveillance information systems data official guidelines surveillance veterinarians","site:aphis.usda.gov animal health surveillance data integration official veterinary surveillance","proof carrying code Necula 1997 PDF termination certificates checker","workflow termination verification scientific workflows static analysis termination","Necula Proof-Carrying Code POPL 1997 PDF producer proof consumer checker","site:coq.inria.fr termination structural recursion reference manual Fixpoint guarded","AProVE termination prover official termination analysis tool","site:bls.gov software developers median annual wage May 2025","CeTA certified termination analysis official paper certificate checker Isabelle termination proof certificates","site:termination-portal.org certificate format termination competition CPF CeTA","workflow management system user-authored workflows external services termination timeout surveillance epidemiology","veterinary surveillance software workflows analytics platform data processing official","Stanford Encyclopedia of Philosophy computability halting problem undecidable","Turing 1936 computable numbers undecidable halting problem PDF"],"sources":[{"source_id":"S1","title":"National Animal Health Surveillance","publisher":"USDA Animal and Plant Health Inspection Service","url":"https://www.aphis.usda.gov/livestock-poultry-disease/surveillance","source_class":"GOVERNMENT_OR_REGULATOR","publication_date":"2026-05-27","accessed_at":"2026-08-03","claims_supported":["Animal-health surveillance is operationally important for timely threat detection, animal and public health, food safety, trade, and national economic viability.","APHIS Veterinary Services and its partner network are identifiable surveillance stakeholders and possible authorizers or adopters."]},{"source_id":"S2","title":"Veterinary Services Applications","publisher":"USDA Animal and Plant Health Inspection Service","url":"https://www.aphis.usda.gov/veterinary-services/applications","source_class":"GOVERNMENT_OR_REGULATOR","publication_date":"2026-05-13","accessed_at":"2026-08-03","claims_supported":["APHIS operates or supports multiple animal-health information applications, including Surveillance Data Management, Data Integration Services, the Animal Health Event Repository, Surveillance Collaboration Services, dashboards, laboratory submission, and emergency-response systems.","Training and operational support structures exist around Veterinary Services applications, making APHIS a concrete authority context, although the page does not describe user-authored unrestricted analytic workflows or termination failures."]},{"source_id":"S3","title":"Terrestrial Animal Health Code Chapter 1.4: Animal Health Surveillance","publisher":"World Organisation for Animal Health","url":"https://www.woah.org/fileadmin/Home/eng/Health_standards/tahc/2021/en_chapitre_surveillance_general.htm","source_class":"STANDARD","publication_date":"2021","accessed_at":"2026-08-03","claims_supported":["Surveillance supports disease control, risk analysis, sanitary measures, trade assurance, and decision-making.","The standard calls for appropriate, documented analytical methods; documentation of uncertainty and assumptions; reliable data management; auditing; and attention to financial, technical, human, and authority constraints.","Software may aggregate and analyze multiple data sources, and early-warning systems should remain under Veterinary Authority control.","The standard does not express a need for proof-carrying termination admission."]},{"source_id":"S4","title":"Proof-Carrying Code","publisher":"George C. Necula, University of California, Berkeley","url":"https://people.eecs.berkeley.edu/~necula/pcc.html","source_class":"PRIMARY_RESEARCH","publication_date":"undated legacy research page","accessed_at":"2026-08-03","claims_supported":["Proof-carrying code already establishes the producer-supplied-proof and consumer-side-checker architecture proposed by the candidate.","The approach separates potentially difficult proof production from simpler proof validation and binds proofs to program semantics and policy.","Reported applications included resource bounds and proofs that mobile agents terminate within a specified instruction count.","The source identifies proof size, proof checking, code-proof binding, semantics, and checker correctness as implementation difficulties."]},{"source_id":"S5","title":"Computability and Complexity","publisher":"Stanford Encyclopedia of Philosophy","url":"https://plato.stanford.edu/entries/computability/","source_class":"AUTHORITATIVE_SECONDARY","publication_date":"2021-10-18","accessed_at":"2026-08-03","claims_supported":["The halting problem for arbitrary programs and inputs is undecidable by a diagonal argument.","A decidable set requires a total procedure that returns the correct yes-or-no answer for every input.","Undecidability of the unrestricted problem coexists with useful, feasible restricted subproblems.","Computability and practical complexity are separate classifications."]},{"source_id":"S6","title":"IsaFoR/CeTA: An Isabelle/HOL Formalization of Rewriting for Certified Tool Assertions","publisher":"University of Innsbruck IsaFoR/CeTA Project","url":"https://isafor-ceta.uibk.ac.at/","source_class":"OFFICIAL_PRODUCT_DOCUMENTATION","publication_date":"2026-06-16","accessed_at":"2026-08-03","claims_supported":["CeTA is an implemented checker for producer-generated termination, nontermination, complexity, safety, and related proof certificates.","Its supported methods include lexicographic ranking functions, size-change termination, program-graph decomposition, and complexity techniques.","Its checker is generated from an Isabelle/HOL formalization, directly demonstrating that certified termination-proof checking is established practice rather than a new intervention.","The tool covers specified formalisms and certificate formats, not arbitrary production veterinary workflow semantics."]},{"source_id":"S7","title":"AProVE: Automated Program Verification Environment","publisher":"RWTH Aachen University AProVE Team","url":"https://aprove.informatik.rwth-aachen.de/","source_class":"OFFICIAL_PRODUCT_DOCUMENTATION","publication_date":"2026","accessed_at":"2026-08-03","claims_supported":["A maintained tool already performs automated termination, complexity, and safety proof generation for rewriting systems and imperative, functional, logic, probabilistic, and integer-transition programs.","AProVE is a relevant comparator for certificate discovery and termination analysis, while CeTA is a relevant independent-certification comparator.","Existing support for several languages does not establish applicability to the candidate's unspecified surveillance workflow interpreter."]},{"source_id":"S8","title":"National Employment and Wage Data by Occupation, May 2025","publisher":"U.S. Bureau of Labor Statistics","url":"https://www.bls.gov/news.release/ocwage.t01.htm?mod=article_inline","source_class":"GOVERNMENT_OR_REGULATOR","publication_date":"2026-05","accessed_at":"2026-08-03","claims_supported":["The May 2025 national mean annual wage for software developers was $148,100 and the median hourly wage was $65.38.","These labor benchmarks support resource-equivalent order-of-magnitude cost estimates, but not vendor quotations or a production-system budget."]}],"problem_evidence":{"support":"WEAK","rationale":"Animal-health surveillance clearly exists, matters, uses multi-source electronic systems, and is subject to documentation, quality, and authority requirements. Computability sources establish that universal termination prediction is impossible for an unrestricted computational model. However, no source found evidence that an actual veterinary surveillance platform accepts the hypothesized arbitrary user-authored language, labels timeouts as nontermination, has suffered delayed surveillance outputs from such workflows, or is currently funding a universal predictor. The domain importance and mathematical possibility of the failure mode therefore do not verify the candidate's specific operational problem.","source_ids":["S1","S2","S3","S5"]},"stakeholder_evidence":{"support":"MODERATE","rationale":"APHIS Veterinary Services is an identifiable surveillance authority operating relevant data and reporting applications, and WOAH assigns surveillance-system control and follow-up responsibility to Veterinary Authorities. These sources establish credible authorizer classes and a need for reliable, documented surveillance analytics, but neither APHIS nor WOAH expresses demand for proof-carrying workflow admission or confirms authority over the hypothesized platform.","source_ids":["S1","S2","S3"]},"prior_art":{"proximity":"ESTABLISHED_PRACTICE","closest_analogues":[{"name":"Proof-Carrying Code","similarity":"Nearly identical producer/consumer architecture: a code producer supplies a formal proof, a receiving system checks it against formal semantics and policy, and accepted code may execute without trusting proof generation. The documented work also includes termination and resource-bound properties.","remaining_difference":"The candidate applies the architecture to recurring veterinary surveillance workflows and adds domain labels, schema/capability versioning, and a post-termination scheduling gate; these are deployment adaptations rather than a demonstrated new verification method.","source_ids":["S4"]},{"name":"IsaFoR/CeTA certified termination analysis","similarity":"Directly checks machine-readable termination certificates using a checker derived from formally proved Isabelle/HOL results; it supports ranking functions, size-change methods, program graphs, and complexity certificates.","remaining_difference":"The candidate proposes a small custom certificate language and checker tied to a veterinary workflow interpreter, data-schema contract, external-service capabilities, and admission workflow. No technical reason is shown that this is more than adapting existing certified termination infrastructure.","source_ids":["S6"]},{"name":"AProVE automated termination and complexity analysis","similarity":"Already generates termination, complexity, and safety proofs across several programming formalisms and can serve as an automatic proof-discovery comparator upstream of certificate checking.","remaining_difference":"The candidate intentionally permits author-supplied certificates and does not require complete proof discovery; production veterinary workflow semantics and supported evidence constructs remain unspecified.","source_ids":["S7"]}],"distinctive_claim_remaining":"A veterinary surveillance platform can operationally integrate an enforceable, version-linked proof-carrying termination-admission contract—plus explicit uncertified/model-mismatch states and a separate capacity gate—in a way that is sound with respect to its production interpreter and useful enough to outperform a restricted workflow language, existing termination-prover/certifier tooling, and timeout-based containment. This is a contrastive deployment claim, not a new computability or certificate-checking principle.","confidence":"HIGH"},"implementation_evidence":{"support":"MODERATE","rationale":"Proof-carrying code, AProVE, and CeTA demonstrate the generic technical feasibility of separating proof generation from certificate checking and of checking ranking-function and termination certificates. They also expose the main engineering burdens: formal semantics, code-proof binding, certificate format, a small trusted checker, and supported proof-method coverage. Feasibility is not strong for the proposed deployment because the production workflow language, interpreter, external-call semantics, capability enforcement, data-schema evolution, identity/hashing mechanism, and integration points were not externally identified. Legal and clinical risk can be bounded initially by keeping the checker offline and prohibiting outputs from changing animal-level action; production scheduling would require the platform owner and Veterinary Authority to authorize the gate.","source_ids":["S3","S4","S6","S7"]},"scores":{"meaningful_impact":{"score":3,"rationale":"Timely and reliable surveillance matters substantially, but the prevalence and consequence of nonterminating user-authored surveillance workflows are unverified.","source_ids":["S1","S3"]},"stakeholder_pull":{"score":2,"rationale":"Credible surveillance authorities and application operators exist, but no source expresses demand for this intervention or confirms the hypothesized workflow capability.","source_ids":["S1","S2","S3"]},"incremental_advantage":{"score":2,"rationale":"Sound certificate checking would make a stronger claim than finite tests or timeouts, but its practical advantage over a terminating DSL, AProVE/CeTA integration, sandboxing, and ordinary quotas has not been measured.","source_ids":["S4","S6","S7"]},"distinctiveness_plausibility":{"score":1,"rationale":"The core producer-supplied-proof/consumer-checker architecture and certified termination checking are established prior art; the remaining difference is domain-specific governance and integration.","source_ids":["S4","S6"]},"technical_implementability":{"score":4,"rationale":"A toy checker for structural recursion and lexicographic ranking functions is technically credible given functioning proof-carrying and termination-certification systems. Production semantic fidelity and external-call enforcement remain substantial unresolved work.","source_ids":["S4","S6","S7"]},"adoption_authority_feasibility":{"score":2,"rationale":"APHIS and Veterinary Authorities are identifiable authority classes, but no owner of the hypothesized execution platform, procurement path, or approval chain was verified.","source_ids":["S1","S2","S3"]},"evidence_readiness":{"score":3,"rationale":"An offline soundness and negative-test study is bounded and auditable, but it would mostly reproduce established methods and would not answer production fit or demand.","source_ids":["S4","S6","S7"]},"safety_net_benefit":{"score":4,"rationale":"An offline checker, explicit rejection and unknown states, preserved quotas, and a separate veterinary-review boundary can reduce overclaiming without affecting animals during initial evaluation.","source_ids":["S3","S4"]},"scalability":{"score":2,"rationale":"Checker execution can be fast and reusable, but certificate authoring, proof-language coverage, evolving schemas, external-service contracts, and production-semantics maintenance can constrain adoption.","source_ids":["S4","S6"]}},"score_confidence":"MODERATE","costs":{"first_evidence":{"band_2026_usd":"10K_TO_50K","scope":"A two- to six-week offline replication: define toy semantics, implement a small checker, create at most twelve positive and adversarial workflow-certificate pairs, compare with CeTA/AProVE where encodings permit, and obtain an independent proof review.","confidence":"MODERATE","assumptions":["Approximately 0.1-0.25 software/formal-methods FTE-year plus limited independent review.","Existing open-source theorem-proving and termination tools are reused without license or procurement expense.","No live data, production integration, animal-level action, security accreditation, or formal procurement is included.","BLS software-developer wages are used only as a labor-cost anchor; loaded specialist costs may be higher."],"source_ids":["S6","S7","S8"]},"initial_deployment_startup":{"band_2026_usd":"250K_TO_1M","scope":"Formalize one bounded production-like workflow subset, implement certificate parsing/checking and workflow-hash binding, build a sandbox and capability manifest, add explicit admission states, and conduct independent security and proof review without enabling recurring live scheduling.","confidence":"LOW","assumptions":["A team equivalent to roughly two to five specialist FTE-years, using the BLS mean wage as a base before overhead and specialist premiums.","A production interpreter and test environment are accessible and stable.","The proof language remains narrow; major legacy-workflow conversion and enterprise accreditation are excluded.","Existing CeTA/AProVE concepts or components can be reused where technically and legally suitable."],"source_ids":["S4","S6","S7","S8"]},"operational_launch":{"band_2026_usd":"1M_TO_5M","scope":"Production semantic model and validation, runtime capability enforcement, certificate lifecycle and audit records, identity/access controls, integration with surveillance scheduling and data systems, author tooling, training, independent assurance, staged rollout, and rollback controls.","confidence":"LOW","assumptions":["Roughly five to twenty specialist FTE-years across formal methods, platform engineering, security, veterinary epidemiology, quality assurance, training, and program governance.","Deployment occurs in an enterprise surveillance environment comparable in organizational complexity to the multiple applications listed by APHIS.","No national replacement of existing surveillance applications is included.","Authority review and security accreditation are required, but clinical efficacy trials and animal interventions are excluded."],"source_ids":["S2","S3","S4","S6","S8"]},"annual_recurring":{"band_2026_usd":"250K_TO_1M","scope":"Checker and semantics maintenance, certificate revalidation after code/schema/capability changes, author support, audit, incident response, independent periodic review, and capacity-gate operations for one organizational deployment.","confidence":"LOW","assumptions":["Approximately two to six continuing specialist FTE equivalents plus infrastructure and periodic external review.","Workflow volume is moderate and certificate checking is computationally inexpensive relative to proof production.","Major interpreter rewrites, nationwide expansion, and new proof-language research are treated as separate projects.","The BLS wage benchmark is escalated qualitatively for overhead and scarce formal-methods expertise."],"source_ids":["S2","S4","S6","S8"]}},"verified_pipeline_gates":{"externally_supported_problem":{"status":"NO","reason":"Sources verify important surveillance systems and the mathematical impossibility of universal halting prediction, but not the candidate's key empirical premise that a veterinary platform exposes unrestricted user-authored workflows, misuses timeouts, or experiences consequential nontermination.","source_ids":["S1","S2","S3","S5"]},"externally_credible_adopter_or_authorizer":{"status":"UNCERTAIN","reason":"APHIS Veterinary Services and national Veterinary Authorities are credible authority classes, but no source links them to the proposed admission mechanism or confirms control of the hypothesized workflow runtime.","source_ids":["S1","S2","S3"]},"distinct_testable_incremental_claim":{"status":"NO","reason":"The method-level claim substantially collides with proof-carrying code and certified termination checkers. A testable domain-integration claim remains, but no distinctive technical mechanism or externally evidenced veterinary requirement separates it from adaptation of established practice.","source_ids":["S4","S6","S7"]},"bounded_next_evidence_step":{"status":"YES","reason":"A small offline checker evaluation with explicit comparators, adversarial certificates, semantic-mismatch cases, and prespecified falsifiers can be completed without live surveillance use.","source_ids":["S4","S6","S7"]},"no_unresolved_safety_or_authority_stop":{"status":"YES","reason":"The next step can remain offline with synthetic data and no scheduling, clinical interpretation, movement, testing, or treatment effects. Production use would require new platform-owner and Veterinary Authority authorization.","source_ids":["S3"]},"credible_cost_scope_and_range":{"status":"YES","reason":"The four bands are transparent resource-equivalent estimates anchored to current BLS software-developer wages and scoped by increasing integration and assurance obligations; startup and production estimates remain low-confidence because the target platform is unidentified.","source_ids":["S2","S3","S8"]}},"next_evidence_step":"Do not build a new general termination-certification stack as the first move. Run a bounded four-week replication-and-differentiation study on one toy workflow language and no more than twelve synthetic packages. Compare: (A) the proposed structural-recursion/lexicographic-certificate checker, (B) direct use or translation to CeTA-backed certificates, (C) AProVE-assisted proof generation followed by certification where supported, (D) a syntactically terminating restricted DSL, and (E) timeout-only containment. Measure checker totality, valid-proof acceptance, rejection of subtle invalid descent claims, stale-hash and external-contract mismatch detection, proof-author effort, certificate/checking cost, and the share of terminating examples admitted. Prespecified falsifiers are: any invalid certificate is accepted; an accepted package diverges in the toy semantics; workflow or capability changes retain certification; certificate validity itself cannot be decided; or the proposed checker has no material coverage, usability, or integration advantage over CeTA/AProVE or a terminating DSL. This step tests only adaptation mechanics; evidence of production prevalence, stakeholder pull, semantic fidelity, and workflow-author burden would require proprietary inspection or fieldwork.","blocking_evidence":["No external evidence that a veterinary surveillance platform currently accepts unrestricted user-authored loops, recursion, contact-chain traversals, or uncontracted external calls.","No documented veterinary surveillance incident, delay, or resource loss attributable to admitting a workflow on finite runs or misclassifying a timeout.","No first-party expression of demand for proof-carrying admission from APHIS, another Veterinary Authority, a platform owner, or a funder.","No identified production workflow language, interpreter semantics, data-schema contract, external-service contract, or enforceable capability model.","No demonstrated advantage over established proof-carrying code, CeTA/AProVE, or a syntactically terminating workflow language.","No evidence about certificate-author expertise, workflow coverage, false-rejection burden, operational latency, security accreditation, or lifecycle governance in veterinary surveillance.","World novelty, patentability, freedom to operate, market size, and realized impact remain unmeasured."],"research_disposition":"KNOWN_PRACTICE_DIFFUSION","world_novelty_boundary":"World novelty is unmeasured. The search establishes only that the central producer-supplied-proof/consumer-checker architecture and machine-certified termination certificates predate this proposal and remain implemented in current tools. It does not establish whether the exact combination of veterinary surveillance scheduling, schema/capability binding, explicit admission states, and a separate capacity gate has previously been deployed, patented, or published.","arm":"COMPLETE_PROPOSAL_PORTFOLIO","candidate_version":0,"controller_recommendation":{"action":"STOP_DIFFUSION","repairable":false,"material_progress_observed":false,"progress_targets":["Identify a named surveillance-platform owner and obtain first-party confirmation of unrestricted workflow features, timeout semantics, and consequential termination-related incidents.","Specify the actual production interpreter, workflow encoding, dataset quantifiers, external-call semantics, and enforceable capability boundary before making any soundness claim.","Demonstrate a measurable adoption or assurance advantage over CeTA/AProVE integration and a syntactically terminating restricted DSL, not merely over finite testing and timeouts.","Obtain written interest and authority for an offline evaluation from the platform owner and relevant Veterinary Authority, with veterinary outputs explicitly excluded from animal-level decisions.","Report proof-author effort, admission coverage, invalid-certificate rejection, stale-artifact detection, checker trusted-base size, and independent semantic-review results."],"reason":"The core intervention is established formal-verification practice: proof-carrying code already assigns proof production to the producer and validation to the consumer, and CeTA currently certifies termination proofs using formally verified checkers while AProVE supplies relevant proof-generation capabilities. The veterinary-specific problem and adopter pull were not externally verified, and the remaining claim is a domain-integration and diffusion question rather than a distinctive research contribution. The evaluation therefore stops as known-practice diffusion; this STOP is terminal and non-repairable under the controller rules."},"proposal_index":4}