{"schema_version":1,"research_id":"eoa_inverse_innovation_exp04_external_evaluation_20260802","source_assessment_id":"computability_boundary_mapping__engineering_design:PROPOSAL_FIRST:v0","cell_id":"computability_boundary_mapping__engineering_design","search_queries":["site:nasa.gov software formal methods safety critical verification state explosion unknown timeout","site:faa.gov software assurance formal methods DO-333 safety critical software verification","site:iec.ch IEC 61508 software safety lifecycle formal methods programmable electronic safety systems","site:nist.gov formal methods software assurance model checking safety critical","site:hse.gov.uk programmable electronic safety systems software verification formal methods assessor guidance","site:nrc.gov digital instrumentation control formal methods safety verification software","site:gov.uk safety critical software programmable systems formal methods assurance guidance","site:mitre.org model checking unknown timeout safety assurance three-valued results","software model checker result UNKNOWN timeout SAFE UNSAFE formal verification official documentation","CBMC official documentation unwinding assertions bounded model checking completeness threshold","Astrée static analyzer sound alarms false alarms official","UPPAAL model checker unknown out of memory result official documentation","site:nasa.gov formal methods assurance case safety critical software scope assumptions verification evidence","site:faa.gov DO-333 formal methods assumptions verification evidence tool qualification PDF","site:sei.cmu.edu assurance case claims evidence safety critical software formal methods","site:iso.org ISO 26262 software tools confidence formal verification model checking","site:bls.gov occupational employment wages software developers May 2025 median annual wage","site:bls.gov employer costs employee compensation professional technical occupations December 2025 total compensation per hour","site:gsa.gov 2026 engineering labor rates software engineer verification validation","site:nasa.gov cost formal methods safety critical software labor assurance","\"Evidence Arguments for Using Formal Methods in Software Certification\" PDF NASA","site:inria.fr Astrée static analyzer sound false alarms Airbus official","site:absint.com Astrée sound static analyzer safety critical false alarms"],"sources":[{"source_id":"S1","title":"IEC 61508-3:2010 — Functional safety of electrical/electronic/programmable electronic safety-related systems, Part 3: Software requirements","publisher":"International Electrotechnical Commission","url":"https://webstore.iec.ch/en/publication/5517","source_class":"STANDARD","publication_date":"2010-04-30","accessed_at":"2026-08-02","claims_supported":["Safety-related programmable software is subject to specified safety functions, systematic capability, lifecycle activities, validation information, modification controls, and support-tool requirements.","A boundary gate could be embedded in an existing functional-safety lifecycle, but it would not replace IEC 61508 compliance, validation, or tool controls."]},{"source_id":"S2","title":"Digital Instrumentation and Controls Research","publisher":"U.S. Nuclear Regulatory Commission","url":"https://www.nrc.gov/about-nrc/regulatory/research/digital","source_class":"GOVERNMENT_OR_REGULATOR","publication_date":"2026 (current page; exact update date not displayed)","accessed_at":"2026-08-02","claims_supported":["NRC research develops tools, methods, procedures, acceptance criteria, and guidance supporting digital I&C licensing decisions.","NRC identifies digital-system complexity, unanticipated interactions, and emergent behavior as continuing safety-assurance challenges.","NRC is an identifiable authorizer and research stakeholder pursuing assurance-case criteria, high-assurance digital engineering, and methods to support regulatory review."]},{"source_id":"S3","title":"DOT/FAA/TC-19/22: Use of Virtual Machines in Avionics Systems and Assurance Concerns","publisher":"Federal Aviation Administration","url":"https://www.faa.gov/sites/faa.gov/files/aircraft/air_cert/design_approvals/air_software/TC-19-22.pdf","source_class":"GOVERNMENT_OR_REGULATOR","publication_date":"2019-10","accessed_at":"2026-08-02","claims_supported":["FAA-sponsored guidance describes theorem proving, finite-state model checking, and abstract interpretation as distinct formal-method classes.","The report says potentially infinite software state spaces prevent direct finite-state model checking and describes abstraction as a way to obtain finite models.","DO-333-derived practice requires formal-analysis assumptions, including target-computer and data-range assumptions, to be described and justified.","Formal analysis does not eliminate target testing or review obligations, establishing a safety and authority limit on the proposed gate."]},{"source_id":"S4","title":"Explainable Verification for Rapid Certification","publisher":"Carnegie Mellon University Software Engineering Institute","url":"https://www.sei.cmu.edu/annual-reviews/2024-research-review/explainable-verification-for-rapid-certification/","source_class":"PRIMARY_RESEARCH","publication_date":"2024","accessed_at":"2026-08-02","claims_supported":["Exhaustive safety-critical testing is impeded by exponential test growth, while non-exhaustive testing may be unsafe.","Formal-method tools can produce wrong outputs, tool qualification can be expensive, and unexplained Boolean outputs impede practitioner trust.","The U.S. Army Aviation and Missile Center collaborated on work intended to improve certification speed and assurance, demonstrating institutional demand for better verification evidence and explanations."]},{"source_id":"S5","title":"What is Formal Methods?","publisher":"NASA Langley Research Center Formal Methods Program","url":"https://shemesh.larc.nasa.gov/fm/fm-what.html","source_class":"OFFICIAL_GUIDANCE","publication_date":"2024-03-12","accessed_at":"2026-08-02","claims_supported":["Formal verification can establish properties over an entire represented state space, but whole-system use is constrained by enormous complexity.","NASA lists abstraction, restriction to critical components, discretized or reduced ranges, hierarchical analysis, and multiple tools as practical responses.","There is no single best formal method; tool and proof choices depend on application domain and lifecycle phase."]},{"source_id":"S6","title":"CBMC: What is loop unwinding?","publisher":"CBMC Project","url":"https://model-checking.github.io/cbmc-training/faq/loop-unwinding.html","source_class":"OFFICIAL_PRODUCT_DOCUMENTATION","publication_date":"Undated documentation","accessed_at":"2026-08-02","claims_supported":["CBMC performs bounded symbolic execution and requires explicit bounds where loops cannot be proved finite automatically.","A defect beyond bound K can be missed unless completeness is checked.","Unwinding assertions provide a mechanically checkable condition that a chosen bound covers every relevant loop execution, exemplifying an existing bounded-guarantee contract."]},{"source_id":"S7","title":"SV-COMP 2013 Competition Procedure and Verification Result Definitions","publisher":"Software Verification Competition / TACAS","url":"https://sv-comp.sosy-lab.org/2013/rules.php","source_class":"OFFICIAL_ORGANIZATION_DATA","publication_date":"2013-03-21","accessed_at":"2026-08-02","claims_supported":["Established verifier practice already distinguishes TRUE/SAFE, FALSE/UNSAFE with an error-path witness, and UNKNOWN.","Timeout, crash, and out-of-memory are explicitly interpreted as UNKNOWN rather than SAFE or UNSAFE.","Typed outputs, witnesses, resource limits, and category-specific property definitions are therefore mature adjacent prior art, not novel elements."]},{"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":"OFFICIAL_ORGANIZATION_DATA","publication_date":"2026-05-15","accessed_at":"2026-08-02","claims_supported":["May 2025 mean annual wages were $148,100 for software developers, $111,490 for software QA analysts/testers, $119,640 for engineers overall, and $119,770 for health and safety engineers.","These wage levels support labor-based 2026 resource-equivalent estimates, subject to explicit overhead, specialist-premium, tooling, and procurement assumptions."]}],"problem_evidence":{"support":"MODERATE","rationale":"The underlying problem is visible and consequential: regulators and safety organizations report growing digital-control complexity, exponential state/test growth, formal-tool trust problems, qualification expense, and the need to make assumptions and finite abstractions explicit. However, no opened source measures how often real design organizations demand one total Boolean verifier for unrestricted supplier scripts or misreport timeouts as safety verdicts. The candidate's exact organizational failure mode therefore remains plausible but prevalence-unverified.","source_ids":["S2","S3","S4","S5","S6","S7"]},"stakeholder_evidence":{"support":"MODERATE","rationale":"The NRC is an identifiable safety authorizer developing acceptance criteria and assurance-case methods for digital I&C licensing, and the Army Aviation and Missile Center is an identifiable collaborator seeking faster, more trustworthy certification. IEC and FAA materials establish organizations that must authorize lifecycle evidence and certification credit. None explicitly requests a computability-boundary gate under that name or commits to adopt this proposed workflow.","source_ids":["S1","S2","S3","S4"]},"prior_art":{"proximity":"ADJACENT_PRIOR_ART","closest_analogues":[{"name":"DO-333-style formal-method assurance within an avionics certification workflow","similarity":"Already requires justified analysis assumptions, distinguishes theorem proving, finite-state model checking and abstract interpretation, links formal results to traceability, and retains testing and review where formal analysis is insufficient.","remaining_difference":"The opened FAA material does not describe a mandatory pre-tool computability classification or one cross-tool routing record with enforceable UNKNOWN, OUT_OF_SCOPE, TIMEOUT, and TOOL_FAILURE semantics.","source_ids":["S3"]},{"name":"NASA scope-restricted, multi-method formal verification practice","similarity":"Addresses state explosion by abstraction, critical-component restriction, reduced ranges, hierarchical analysis, and application-specific selection among verification methods.","remaining_difference":"It is guidance on selecting and scoping formal methods, not a release gate that first classifies total solvability and attaches a versioned guarantee label to every routed result.","source_ids":["S5"]},{"name":"SV-COMP typed verifier outcomes","similarity":"Operationally separates SAFE, UNSAFE with witness, and UNKNOWN; timeout, crash, and resource exhaustion are not interpreted as semantic verdicts.","remaining_difference":"It is a benchmark protocol, not an engineering-design assurance workflow; it lacks physical-system semantic fidelity, release authority, fragment admission, expert escalation, and lifecycle recheck triggers.","source_ids":["S7"]},{"name":"CBMC bounded verification with unwinding assertions","similarity":"Implements explicit bounded reasoning and a mechanical check that a bound is complete for represented loops, preventing a bounded run from silently inheriting an unbounded guarantee.","remaining_difference":"It covers one bounded-analysis mechanism and does not classify unrestricted solvability, select among exact/abstract/manual modes, or govern release language.","source_ids":["S6"]},{"name":"IEC 61508 software safety lifecycle and tool controls","similarity":"Provides the established lifecycle, specification, validation, modification, and support-tool governance into which the candidate would have to fit.","remaining_difference":"The public abstract does not prescribe the candidate's computability-status lattice, pre-verification classification, or typed fallback router.","source_ids":["S1"]}],"distinctive_claim_remaining":"For heterogeneous programmable safety-control submissions, adding a mandatory model-relative solvability/scope classification and machine-enforced guarantee/status schema before an otherwise standards-conformant verification workflow will reduce over-strong or semantically mislabeled verdicts and improve independent reviewers' routing agreement, while decreasing the number of conclusive within-scope decisions by no more than one case in a 12-model pilot. This is contrastive and falsifiable; the individual mechanisms and several output distinctions are already established practice.","confidence":"HIGH"},"implementation_evidence":{"support":"MODERATE","rationale":"Every principal technical component is credible: syntactic restriction and finite-state analysis are recognized approaches; CBMC shows enforceable bounded completeness checks; SV-COMP shows typed UNKNOWN handling; IEC/FAA practice provides lifecycle, assumption, testing, review, and authority constraints. Integration is still untested. The largest risks are a formally valid but physically unfaithful model, unsound abstractions or adapters, unenforceable supplier-language membership, stale boundary records, excessive UNKNOWN rates, and expert escalation that lacks explicit accountability. Legal feasibility is domain-specific: the gate can support but cannot replace certification, statutory licensing, IEC lifecycle obligations, independent review, or the chief engineer/regulator's release authority.","source_ids":["S1","S2","S3","S5","S6","S7"]},"scores":{"meaningful_impact":{"score":4,"rationale":"Avoiding unsupported safety verdicts or futile universal-verifier programs could materially reduce safety and schedule risk, although incidence and realized effect are unmeasured.","source_ids":["S2","S4","S5"]},"stakeholder_pull":{"score":4,"rationale":"Regulators and defense/aviation assurance stakeholders visibly seek better digital-system assurance, acceptance criteria, explainability, and certification efficiency; pull for this exact gate is not yet demonstrated.","source_ids":["S2","S3","S4"]},"incremental_advantage":{"score":3,"rationale":"Mandatory preclassification and unified guarantee labels could improve consistency over conventional tool-by-tool assurance, but most component practices already exist and no comparative effect has been measured.","source_ids":["S3","S5","S6","S7"]},"distinctiveness_plausibility":{"score":2,"rationale":"The remaining distinction is primarily a governed combination and ordering of mature practices; no close source showed the full bundle, but the novelty margin is narrow.","source_ids":["S1","S3","S5","S6","S7"]},"technical_implementability":{"score":4,"rationale":"Parsers, bounded model checking, abstractions, typed result schemas, routing rules, and versioned records are implementable; semantic fidelity and sound integration remain substantial engineering obligations.","source_ids":["S3","S5","S6","S7"]},"adoption_authority_feasibility":{"score":4,"rationale":"A chief engineer or design-assurance board can authorize a non-release pilot, and regulators already evaluate comparable evidence. Production use would still require domain-specific certification and independent review.","source_ids":["S1","S2","S3"]},"evidence_readiness":{"score":3,"rationale":"Standards, official guidance, tool documentation, and a precise frozen-set test are available, but the decisive baseline data and controller models require an organizational partner.","source_ids":["S1","S2","S3","S6","S7"]},"safety_net_benefit":{"score":5,"rationale":"Preserving UNKNOWN, bounds, witnesses, assumptions, and non-release rollback directly limits false reassurance and leaves existing release authority intact.","source_ids":["S1","S3","S6","S7"]},"scalability":{"score":3,"rationale":"The status schema and record template can scale across projects, but each controller language, property, physical environment, and certification regime requires specialist formalization and revalidation.","source_ids":["S1","S2","S3","S5"]}},"score_confidence":"MODERATE","costs":{"first_evidence":{"band_2026_usd":"10K_TO_50K","scope":"Prepare and run the non-release 12-model comparison: freeze artifacts, specify grammar/bounds/properties, configure the gate and baseline, conduct two independent reviews, adjudicate labels, and report disagreements.","confidence":"MODERATE","assumptions":["Approximately 160-360 combined specialist hours across control engineering, formal verification, independent safety review, and analysis.","Loaded internal labor is estimated from 2025 BLS wages with benefits, overhead, and specialist premiums added.","Existing models, computing infrastructure, and open-source or already licensed verification tools are available.","The band excludes remediation of the controller models and any change to release decisions."],"source_ids":["S4","S6","S7","S8"]},"initial_deployment_startup":{"band_2026_usd":"250K_TO_1M","scope":"Develop a production-quality input contract, fragment checker, routing/status service, evidence schema, adapters to existing verification tools, audit trail, assurance-case template, security controls, and change/recheck workflow.","confidence":"LOW","assumptions":["Two to five specialist FTE-equivalents for roughly 6-12 months.","At least one control engineer, formal-methods engineer, safety-assurance reviewer, and software/integration engineer participate.","Existing verification engines are integrated rather than developed from scratch.","Domain-specific tool qualification, procurement, and proprietary supplier-language work could move cost above the band."],"source_ids":["S1","S3","S4","S8"]},"operational_launch":{"band_2026_usd":"250K_TO_1M","scope":"Validate and qualify the integrated workflow for its intended use, conduct an independent safety/security assessment, train reviewers, run a parallel-production period, migrate records, establish governance, and obtain design-authority or regulator acceptance where required.","confidence":"LOW","assumptions":["Launch covers one organization, one main controller-language family, and one assurance regime.","No automatic release authorization is delegated to the gate.","Formal results are supplemented by required testing, review, and target-environment evidence.","External certification or regulator fees and major controller redesigns are excluded."],"source_ids":["S1","S2","S3","S4","S8"]},"annual_recurring":{"band_2026_usd":"250K_TO_1M","scope":"Operate the gate, review escalations, maintain tool and language adapters, audit labels and assumptions, reclassify after changes, preserve evidence, train staff, and support authority reviews.","confidence":"LOW","assumptions":["Two to five FTE-equivalents plus ordinary compute and tooling.","Submission volume is moderate and most models reuse established fragments and properties.","Major new languages, certification regimes, or custom proofs are separately funded.","The estimate is resource-equivalent and is not a vendor quote."],"source_ids":["S1","S2","S3","S8"]}},"verified_pipeline_gates":{"externally_supported_problem":{"status":"YES","reason":"Official and primary sources establish consequential digital-control complexity, state-space limits, non-exhaustive evidence risk, and formal-tool trust and qualification problems. Exact prevalence of timeout mislabeling remains unknown but does not negate the externally supported underlying problem.","source_ids":["S2","S3","S4","S5"]},"externally_credible_adopter_or_authorizer":{"status":"YES","reason":"The NRC is a regulatory authorizer researching assurance cases and acceptance methods for digital I&C, while FAA/Army aviation stakeholders provide additional credible assurance users. No source establishes a purchase or adoption commitment.","source_ids":["S2","S3","S4"]},"distinct_testable_incremental_claim":{"status":"YES","reason":"The claim can be tested against a standards-conformant baseline using mislabeled-verdict rate, reviewer routing agreement, and loss of conclusive within-scope decisions. Existing prior art narrows the claim to the mandatory ordering and integrated enforcement rather than the component mechanisms.","source_ids":["S3","S5","S6","S7"]},"bounded_next_evidence_step":{"status":"YES","reason":"A frozen 12-model, non-release, comparator-controlled pilot has a fixed sample, roles, endpoints, cost ceiling, halt conditions, and explicit falsifiers.","source_ids":["S4","S6","S7","S8"]},"no_unresolved_safety_or_authority_stop":{"status":"YES","reason":"The next step changes no deployed controller or release decision, preserves existing authority, and halts on any loss of scope enforcement or guarantee labels. Production deployment would require additional certification and authority approval.","source_ids":["S1","S2","S3"]},"credible_cost_scope_and_range":{"status":"YES","reason":"All four estimates specify included work and major exclusions, and labor assumptions are anchored to current BLS occupational wages. Confidence is low beyond the pilot because tool qualification, procurement, model complexity, and regulatory effort are organization-specific.","source_ids":["S4","S8"]}},"next_evidence_step":"With an NRC licensee, aerospace assurance organization, or comparable safety-control design partner, freeze 12 previously adjudicated models spanning finite-state, bounded-loop, abstractable, unrestricted-extension, known unsafe, and prior-timeout cases. Randomize and blind two independent reviewer pairs to apply: (A) the strongest existing standards-conformant workflow using the same tools, evidence, and time budget but without the new pre-gate or enforced result schema; and (B) the proposed gate. Primary endpoints are independently adjudicated over-strong/mislabeled verdict rate and inter-reviewer agreement on route and guarantee. Secondary endpoints are analyst hours, UNKNOWN/OUT_OF_SCOPE rate, and the number of conclusive within-scope decisions. Require intervention-arm mislabeled verdicts to be zero, improvement over baseline on mislabeled verdicts or routing agreement, no more than one lost conclusive decision out of 12, fragment-membership disagreement on no more than one model, and total cost below $50,000. Falsify the intervention claim if any UNKNOWN, OUT_OF_SCOPE, TIMEOUT, TOOL_FAILURE, incomplete bound, or spurious abstract counterexample becomes unqualified SAFE/UNSAFE; if the baseline already achieves identical labels and traceability; if routing agreement does not improve; if the conclusive-result noninferiority margin is exceeded; or if reviewers cannot reproduce the physical/environmental semantics. Stop without changing release status.","blocking_evidence":["No external prevalence estimate was found for organizations demanding total Boolean verification over unrestricted controller extensions or treating timeouts as semantic verdicts.","No partner-supplied controller corpus or baseline workflow data were available, so incremental effect and operational burden cannot be estimated from web evidence.","No live test establishes that fragment membership, environment assumptions, abstraction soundness, and guarantee labels survive real tool adapters and supplier extensions.","No chief engineer, design-assurance board, licensee, or regulator has accepted the proposed gate as release evidence.","The opened public IEC page is an abstract, not the complete paid normative text; a deployment-specific standards traceability review remains necessary.","Tool licensing, qualification, cybersecurity, procurement, and regulator-review costs are organization-specific and unquoted.","World novelty, patentability, freedom to operate, market size, and realized safety or schedule impact remain unmeasured."],"research_disposition":"PILOT_OR_ADOPTION_INQUIRY","world_novelty_boundary":"The search found mature adjacent standards and practices covering scoped assumptions, finite-state model checking, abstraction, bounded-completeness checks, typed UNKNOWN/timeout results, lifecycle governance, and assurance evidence. It did not establish an identical mandatory pre-tool computability-classification gate with machine-enforced cross-mode guarantee labels and release-linked recheck records. This is only a search-bounded differentiation statement, not a finding of world novelty, patentability, freedom to operate, market size, or realized impact.","arm":"PROPOSAL_FIRST","candidate_version":0,"controller_recommendation":{"action":"STOP_EMPIRICAL_RESEARCH_NEEDED","repairable":true,"material_progress_observed":true,"progress_targets":["Secure an authorized non-release partner and frozen 12-model corpus representing all proposed routes.","Run the blinded comparator-controlled pilot and measure mislabeled verdicts, routing agreement, conclusive-result retention, analyst time, and UNKNOWN burden.","Demonstrate conservative fragment-membership enforcement and end-to-end preservation of bounds, assumptions, witnesses, and status labels through real tool adapters.","Obtain independent review of semantic fidelity between formal controller/environment models and the physical safety claim.","Produce a clause-level traceability and authority analysis for the applicable full standards and certification regime.","Replace resource-equivalent estimates with partner labor records, tool-qualification scope, vendor quotes, and regulator-review assumptions."],"reason":"Web evidence establishes the problem family, credible authorizers, implementable component mechanisms, adjacent prior art, and a bounded safe test. The remaining contrastive claim is an operational comparative-effect claim requiring proprietary controller artifacts, independent reviewers, workflow observation, and live integration testing; it cannot be resolved by further bounded web search alone."}}