2026 04 26 llm verifiability asymmetry code world action

What is the precise technical distinction between code generation and other Large Language Model outputs in terms of external verifiability, and what does this asymmetry imply for safe deployment boundaries in a regulated financial institution?

Research Question

What is the precise technical distinction between code generation and other Large Language Model (LLM)-generated outputs in terms of external verifiability, specifically, that code operates in a formal system with deterministic external verifiers (compilers, type checkers, test suites, linters, formal proof assistants) that can confirm or refute correctness independently of the LLM's confidence, whereas world actions (updating records, triggering workflows, sending communications, making judgments about customer situations) have no equivalent external verifier and therefore produce outputs that are indistinguishable from correct outputs until consequence lands, and what does this asymmetry imply for the boundary between safe and unsafe LLM deployment in a regulated financial institution; specifically, does this asymmetry constitute a principled technical basis for the claim that Artificial Intelligence (AI)-assisted software engineering is the highest-confidence LLM deployment domain, while LLM-based agents taking consequential world actions are operating in a domain where errors are structurally undetectable before harm occurs?

Scope

In scope:

The formal definition of external verifiers: what makes a verifier "external" (operates independently of the LLM's internal confidence), "deterministic" (produces a binary or graded verdict that is reproducible), and "domain-complete" (covers the relevant correctness criteria for the output type)
The category of formal systems with external verifiers: compilers, type checkers, test suites, linters, static analysis tools, formal proof assistants (Coq, Isabelle, Lean), contract checkers, and the conditions under which code output can be verified using them
The category of world actions without external verifiers: database updates, workflow triggers, outbound communications, customer-facing decisions, financial transactions, case handling decisions, and why no equivalent formal verifier exists for these
The structural consequence of the verifiability asymmetry: that errors in unverifiable outputs are indistinguishable from correct outputs until downstream harm occurs, and what this means for pre-deployment quality assurance
Empirical evidence on the reliability of AI-assisted code generation with and without verification pipelines (GitHub Copilot studies, DeepMind AlphaCode results, formal verification research)
Regulatory implications in financial services: FCA (Financial Conduct Authority), PRA (Prudential Regulation Authority), and Basel frameworks on model risk and operational risk that bear on the use of unverifiable AI outputs in consequential decisions

Out of scope:

General AI safety theory beyond the verifiability argument
The specific content of LeCun's critique (covered by Q1, 2026-04-26-lecun-llm-critique-primary-sources)
Governance frameworks for managing the risk once identified (covered by Q3 and Q4)
Formal methods research not directly relevant to LLM output verification

Constraints:

The verifiability distinction must be stated precisely enough to be operationally useful: it must be possible to classify any proposed LLM use case as "verifiable" or "unverifiable" using the framework produced
Regulatory references must cite specific rules or guidance, not just name frameworks
Empirical evidence on code generation reliability must come from peer-reviewed or independently published studies, not vendor marketing material

Context

[inference; source: https://davidamitchell.github.io/Research/research/2026-04-26-access-control-amplification-agentic-operations.html; https://davidamitchell.github.io/Research/research/2026-04-26-implicit-rate-limiting-controls-agentic-ai-removal.html; https://davidamitchell.github.io/Research/research/2026-04-26-agentic-ai-regulatory-preconditions-control-failure-assessment.html] Prior completed repository work already established that consequential agent deployment amplifies access misuse, removes human-speed buffers, and turns unresolved governance weaknesses into current or foreseeable control failures.
[inference; source: https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence; https://www.bankofengland.co.uk/prudential-regulation/publication/2023/may/model-risk-management-principles-for-banks] This item narrows that broader governance problem to a technical boundary question: whether code is categorically different because formal external verifiers can reject or accept outputs before deployment, while most world actions require governance, monitoring, and post hoc review because no equivalent pre-consequence oracle exists.

Cross-references:

Q1: 2026-04-26-lecun-llm-critique-primary-sources (prerequisite: establishes LeCun's architectural framework)
Q3: 2026-04-26-lecun-critique-citizen-development-enterprise-risk
Q4: 2026-04-26-software-engineering-investment-case-llm

Approach

Formal verifier taxonomy: Define and characterise the class of formal external verifiers available for code outputs, compilers, type systems, test frameworks, linters, static analysis, formal proof assistants. For each, specify what property of the code it verifies, what its verdict means (pass/fail, error, warning), and whether it is independent of the LLM's confidence score.
World action non-verifiability analysis: For each category of world action relevant to financial services (record updates, workflow triggers, outbound communications, customer decisions, financial calculations, compliance assessments), establish why no equivalent formal verifier exists and characterise the detection latency, how long after the action is taken an error becomes visible.
Structural undetectability argument: Construct the formal argument that unverifiable LLM outputs are structurally indistinguishable from correct outputs until consequence lands, drawing on the absence of a confidence-correctness correlation in LLM outputs and the absence of an external oracle.
Empirical evidence review: Review published empirical evidence on AI-assisted code generation quality with and without verification pipelines, GitHub Copilot user studies, DeepMind AlphaCode, formal methods integration research. Establish whether the verifier pipeline materially reduces error rates, and what residual risk remains.
Regulatory mapping: Map the verifiability asymmetry to specific regulatory obligations in UK financial services, FCA model risk guidance, PRA SS1/23, Basel model risk management principles, and assess whether unverifiable LLM outputs in consequential decisions constitute a model risk management gap.
Deployment boundary derivation: Synthesise the technical and regulatory analysis into a principled deployment boundary, a clear criterion for classifying LLM use cases as high-confidence (formal system, external verifier available) or structurally unsafe (world action, no pre-consequence detection).

Sources

Research Skill Output

(Full output from running the research skill, retained verbatim in the completed item. Sections 0-5 are the investigation, and section 6 seeds the Findings section below.)

§0 Initialise

[fact; source: https://github.blog/2022-09-07-research-quantifying-github-copilots-impact-on-developer-productivity-and-happiness/; https://arxiv.org/abs/2107.03374; https://arxiv.org/abs/2203.07814; https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/; https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html] Research question restated: what precisely distinguishes code-generation outputs from other LLM outputs is not that code is always correct, but that code can enter a verifier pipeline whose accept-or-reject decision is computed outside the model by compilers, type checkers, tests, analyzers, and proof tools, whereas world actions generally cannot be accepted by any comparable domain-complete oracle before effects occur.
[fact; source: https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence; https://www.bankofengland.co.uk/prudential-regulation/publication/2023/may/model-risk-management-principles-for-banks; https://www.nist.gov/publications/artificial-intelligence-risk-management-framework-ai-rmf-10] Scope confirmed: the investigation focuses on verifier classes, empirical code-generation evidence, limits of formal verification, and regulated-financial-services implications for deployment boundaries.
[fact; source: https://arxiv.org/abs/2107.03374; https://arxiv.org/abs/2203.07814; https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/; https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html] Constraint confirmed: code is treated as conditionally verifiable rather than inherently safe, because every verifier only certifies the properties it is specified to check.
[fact; source: https://davidamitchell.github.io/Research/research/2026-04-26-access-control-amplification-agentic-operations.html; https://davidamitchell.github.io/Research/research/2026-04-26-implicit-rate-limiting-controls-agentic-ai-removal.html; https://davidamitchell.github.io/Research/research/2026-04-26-agentic-ai-regulatory-preconditions-control-failure-assessment.html] Prior work cross-reference: adjacent completed items already showed that access-control amplification, machine-speed execution, and unresolved governance debt make consequential agent deployment fragile, so this item narrows the question to the more basic asymmetry in pre-consequence verifiability.
[fact; source: https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence; https://www.bankofengland.co.uk/prudential-regulation/publication/2023/may/model-risk-management-principles-for-banks] Output format confirmed: knowledge, specifically a deployment-boundary test that distinguishes verifier-gated LLM use from consequential world-action use.

§1 Question Decomposition

Root question: when can an LLM output be accepted by an external decision procedure before deployment or execution, rather than only being judged after effects occur?
A. Verifier taxonomy
- A1. What properties do compilers verify?
- A2. What properties do static type checkers verify?
- A3. What properties do linters and static analyzers verify?
- A4. What properties do test suites and program judges verify?
- A5. What properties do formal proof assistants and program verifiers verify?
B. Verifier conditions
- B1. What makes a verifier external to the LLM?
- B2. What makes a verifier deterministic enough to be operationally useful?
- B3. When is a verifier domain-complete, and when is it only partial?
C. Code-generation evidence
- C1. What do HumanEval and AlphaCode show about verifier-gated acceptance?
- C2. What does the GitHub Copilot study show about productivity under a test-gated task?
D. Limits of verification
- D1. What does Dafny show about the strongest available assurance for code?
- D2. What does neural-network specification research show about why world-model outputs are harder to verify?
E. World-action non-verifiability
- E1. Why do database writes, workflow triggers, communications, and customer decisions lack domain-complete external verifiers?
- E2. How does error detection latency differ across those action types?
- E3. Why is model confidence not an adequate substitute for an external verifier?
F. Regulatory synthesis
- F1. What do United Kingdom supervisory materials say about AI governance, model risk, and monitoring?
- F2. What deployment boundary follows for regulated financial institutions?

§2 Investigation

Source access and replacement notes

[fact; source: https://github.com/davidamitchell/Research/blob/main/research-prompt.md] Access note: .github/skills/research/SKILL.md was absent in this runtime, so the repository fallback process from research-prompt.md was used.
[fact; source: https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html] Failed primary-source search record: query Seshia Formal Specification for Deep Neural Networks 2018 arXiv did not locate a matching arXiv preprint; the seeded https://arxiv.org/abs/1801.09604 resolved to an unrelated evacuation-simulation paper, so the official author page and DOI-backed conference citation were used instead.
[fact; source: https://www.nist.gov/publications/towards-standard-identifying-and-managing-bias-artificial-intelligence] Access note: the seeded NIST SP 1270 PDF URL was machine-accessible only as raw PDF bytes in this runtime, so the official NIST publication page was used as the accessible citation surface.
[fact; source: https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence; https://www.bankofengland.co.uk/prudential-regulation/publication/2023/october/artificial-intelligence-and-machine-learning] Access note: the seeded FCA discussion-paper URL now resolves to feedback and summary content, so the joint official Bank of England page for DP5/22 was used for the primary discussion-paper text and FS2/23 was used for the feedback-statement layer.

A. What external verifiers for code actually do

[fact; source: https://gcc.gnu.org/onlinedocs/gcc-14.3.0/gcc/Warnings-and-Errors.html] GCC reports errors for problems that make it impossible to compile a program and reports warnings for unusual conditions that may indicate a problem while still allowing compilation to proceed.
[fact; source: https://www.typescriptlang.org/docs/handbook/2/basic-types.html] TypeScript describes static type-checking as finding bugs before code runs by using a static type system to predict how code is expected to behave.
[fact; source: https://mypy.readthedocs.io/en/stable/getting_started.html] mypy states that it type-checks code statically, without ever running the code, and reports type errors from annotations and inferred relationships.
[fact; source: https://docs.astral.sh/ruff/] Ruff is a rule-based linter and formatter that diagnoses code against a large set of predefined rules and can automatically fix some violations.
[fact; source: https://codeql.github.com/docs/codeql-overview/about-codeql/] CodeQL is a language and toolchain for code analysis that automates security checks, extracts syntactic and semantic information from codebases, and runs queries whose results highlight potential issues in source code.
[fact; source: https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/] Dafny exposes preconditions, postconditions, loop invariants, and termination metrics, and its verifier attempts to prove that an implementation satisfies those specifications for all inputs meeting the preconditions.
[inference; source: https://gcc.gnu.org/onlinedocs/gcc-14.3.0/gcc/Warnings-and-Errors.html; https://www.typescriptlang.org/docs/handbook/2/basic-types.html; https://mypy.readthedocs.io/en/stable/getting_started.html; https://docs.astral.sh/ruff/; https://codeql.github.com/docs/codeql-overview/about-codeql/; https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/] These tools are external verifiers because their verdict is computed by procedures outside the LLM and does not depend on the model's self-reported confidence, but they are not all equally strong because each checks a different property class.
[inference; source: https://gcc.gnu.org/onlinedocs/gcc-14.3.0/gcc/Warnings-and-Errors.html; https://www.typescriptlang.org/docs/handbook/2/basic-types.html; https://mypy.readthedocs.io/en/stable/getting_started.html; https://docs.astral.sh/ruff/; https://codeql.github.com/docs/codeql-overview/about-codeql/; https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/] A code output is only operationally verifiable when the acceptance gate is explicit, reproducible, and bound to properties that matter for release, such as successful compilation, type soundness, passing tests, absence of flagged vulnerabilities, or proof obligations.

B. Empirical evidence that verifier pipelines materially change code-generation reliability

[fact; source: https://arxiv.org/abs/2107.03374] HumanEval measures functional correctness for program synthesis from docstrings using unit tests, and the Codex model solved 28.8% of problems at one sample and 70.2% with 100 samples and repeated selection.
[fact; source: https://arxiv.org/abs/2203.07814] AlphaCode reports that reliable performance depended on large-scale model sampling followed by filtering based on program behavior to a small set of submissions.
[fact; source: https://github.blog/2022-09-07-research-quantifying-github-copilots-impact-on-developer-productivity-and-happiness/] GitHub's controlled study of 95 professional developers used a JavaScript Hypertext Transfer Protocol (HTTP) server task whose submissions were scored for correctness and completeness with a test suite, and the Copilot group completed the task faster and with a higher completion rate.
[inference; source: https://arxiv.org/abs/2107.03374; https://arxiv.org/abs/2203.07814; https://github.blog/2022-09-07-research-quantifying-github-copilots-impact-on-developer-productivity-and-happiness/] The common pattern across these studies is not that the model is intrinsically trustworthy, but that generated code becomes operationally usable when an external acceptance mechanism filters candidate outputs before human or production acceptance.

C. Why even the strongest code verification remains conditional

[fact; source: https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/] Dafny's strongest guarantee is bounded by the programmer's formal specification, because the verifier proves conformance to the annotated contract rather than to every unstated property a stakeholder might care about.
[fact; source: https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html] Seshia et al. state that verification of deep neural networks is most meaningful only when performed with high-quality formal specifications and identify specification quality as the central challenge.
[inference; source: https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/; https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html] The relevant asymmetry is therefore conditional rather than absolute: code sits in a domain where useful formal specifications and external checkers often exist, while world-action tasks usually do not expose correctness in a compact, machine-checkable form.

D. Why world actions lack equivalent external verifiers

[fact; source: https://www.nist.gov/publications/towards-standard-identifying-and-managing-bias-artificial-intelligence] NIST SP 1270 states that ambiguous concepts and behavior are quantified and then used to categorize, sort, recommend, or make decisions about people's lives, and that harmful impacts can arise regardless of intent.
[fact; source: https://www.nist.gov/publications/artificial-intelligence-risk-management-framework-ai-rmf-10] AI RMF 1.0 presents AI risk management as a lifecycle governance problem for organizations designing, developing, deploying, or using AI systems, rather than as a purely formal verification problem.
[inference; source: https://www.nist.gov/publications/towards-standard-identifying-and-managing-bias-artificial-intelligence; https://www.nist.gov/publications/artificial-intelligence-risk-management-framework-ai-rmf-10; https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html] Database writes, workflow triggers, outbound communications, customer judgments, and compliance assessments do not usually admit domain-complete formal specifications because correctness depends on latent world state, policy interpretation, authorization context, fairness considerations, and future consequences that are not exhaustively machine-represented.
[inference; source: https://www.nist.gov/publications/towards-standard-identifying-and-managing-bias-artificial-intelligence; https://davidamitchell.github.io/Research/research/2026-04-26-access-control-amplification-agentic-operations.html; https://davidamitchell.github.io/Research/research/2026-04-26-implicit-rate-limiting-controls-agentic-ai-removal.html] A database update can be schema-validated and permission-checked, but those checks do not prove that the update is semantically correct, appropriately authorized in business terms, or harmless in downstream reconciliation.
[inference; source: https://www.nist.gov/publications/towards-standard-identifying-and-managing-bias-artificial-intelligence; https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence] A workflow trigger can be syntactically valid and technically authorized while still being contextually wrong, such as launching a collection process, case escalation, or funds movement on a false premise.
[inference; source: https://www.nist.gov/publications/towards-standard-identifying-and-managing-bias-artificial-intelligence; https://www.nature.com/articles/s42256-024-00976-7] An outbound communication can be grammatically fluent and persuasive while still being factually wrong, misleading, mistimed, or harmful to a customer relationship, and those failures are typically discovered only after delivery.
[inference; source: https://www.nist.gov/publications/towards-standard-identifying-and-managing-bias-artificial-intelligence; https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence] Customer decisions and compliance assessments are the least verifiable class because they combine factual uncertainty, ambiguous concepts, normative judgment, and regulatory interpretation in ways that no single pre-execution oracle can settle.
[inference; source: https://www.nist.gov/publications/towards-standard-identifying-and-managing-bias-artificial-intelligence; https://davidamitchell.github.io/Research/research/2026-04-26-implicit-rate-limiting-controls-agentic-ai-removal.html] Detection latency for these world actions is therefore post hoc by design, surfacing through reconciliation, customer complaint, exception handling, audit, incident review, or supervisory challenge rather than through an immediate deterministic accept-reject gate.

E. Why LLM confidence is not a substitute for an external verifier

[fact; source: https://aclanthology.org/2024.naacl-long.366/] Geng et al. state that LLMs are unreliable due to factual errors in their generations and present calibration as a still-active research problem.
[fact; source: https://www.nature.com/articles/s42256-024-00976-7] Steyvers et al. state that humans usually do not observe a model's internal confidence and instead infer confidence from the language produced by the model.
[fact; source: https://www.nature.com/articles/s42256-024-00976-7] The same study defines a calibration gap between model confidence and human confidence and treats that gap as consequential for reliable assistants.
[inference; source: https://aclanthology.org/2024.naacl-long.366/; https://www.nature.com/articles/s42256-024-00976-7] Even where internal calibration has some value for ranking answers, confidence remains an inadequate release criterion for world actions because the relevant acceptance question is not only "is the string probably correct" but "is the action correct, allowed, fair, and reversible in this concrete context."

F. Regulatory implications for a regulated financial institution

[fact; source: https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence] DP5/22 states that AI may pose novel challenges and amplify existing risks to consumers, firms, market integrity, and financial stability, and says the supervisory authorities are interested in additional challenges and risks that AI brings to firms' decision-making and governance processes.
[fact; source: https://www.bankofengland.co.uk/prudential-regulation/publication/2023/october/artificial-intelligence-and-machine-learning] FS2/23 says respondents highlighted governance, accountability, data risk, third-party dependencies, and ongoing monitoring as central themes for AI in financial services.
[fact; source: https://www.bankofengland.co.uk/prudential-regulation/publication/2023/may/model-risk-management-principles-for-banks] PS6/23 states that the PRA's principles are intended to help firms identify, manage, monitor, and control risks associated with models that have a material impact on business decisions and notes that firms should identify and manage risks associated with AI and machine-learning models to the extent they apply to models more generally.
[fact; source: https://www.nist.gov/publications/artificial-intelligence-risk-management-framework-ai-rmf-10] AI RMF 1.0 is explicitly aimed at helping organizations manage AI risks across design, development, deployment, and use.
[inference; source: https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence; https://www.bankofengland.co.uk/prudential-regulation/publication/2023/october/artificial-intelligence-and-machine-learning; https://www.bankofengland.co.uk/prudential-regulation/publication/2023/may/model-risk-management-principles-for-banks; https://www.nist.gov/publications/artificial-intelligence-risk-management-framework-ai-rmf-10] These regulatory materials do not provide a deterministic verifier for consequential AI outputs; instead they demand governance, accountability, monitoring, and challenge, which is consistent with a world-action domain where correctness cannot be conclusively certified before effects occur.
[assumption; source: https://www.nist.gov/publications/artificial-intelligence-risk-management-framework-ai-rmf-10; https://davidamitchell.github.io/Research/research/2026-04-26-agentic-ai-regulatory-preconditions-control-failure-assessment.html] When a workflow mixes verifier-gated code production with consequential write actions, the safe deployment classification should be set by the least verifiable consequential step. Justification: the reviewed governance sources and adjacent repository work treat residual risk at the action boundary, not at the most easily tested intermediate artifact.

§3 Reasoning

[inference; source: https://gcc.gnu.org/onlinedocs/gcc-14.3.0/gcc/Warnings-and-Errors.html; https://www.typescriptlang.org/docs/handbook/2/basic-types.html; https://mypy.readthedocs.io/en/stable/getting_started.html; https://docs.astral.sh/ruff/; https://codeql.github.com/docs/codeql-overview/about-codeql/; https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/] The operational definition that fits the evidence is: an LLM use case is externally verifiable when acceptance depends on an independently computed verdict over a formal artifact and a pre-specified property set before release or execution.
[inference; source: https://www.nist.gov/publications/towards-standard-identifying-and-managing-bias-artificial-intelligence; https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html; https://aclanthology.org/2024.naacl-long.366/; https://www.nature.com/articles/s42256-024-00976-7] A use case is externally unverifiable when correctness depends on open-world facts, ambiguous human categories, policy interpretation, or downstream consequences that cannot be compactly encoded into a decisive pre-execution oracle.
[inference; source: https://arxiv.org/abs/2107.03374; https://arxiv.org/abs/2203.07814; https://github.blog/2022-09-07-research-quantifying-github-copilots-impact-on-developer-productivity-and-happiness/; https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/] Code generation falls on the high-confidence side only when the organization actually enforces verifier gates; raw code text emitted by an LLM without compilation, testing, review, or proof is still just probabilistic output.
[inference; source: https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence; https://www.bankofengland.co.uk/prudential-regulation/publication/2023/may/model-risk-management-principles-for-banks] World-action agents fall on the low-confidence side because the regulator-facing controls available are challenge, monitoring, accountability, and post hoc remediation rather than decisive pre-action certification.

§4 Consistency Check

[fact; source: https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/; https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html] No contradiction remains between "code is verifiable" and "verification is limited," because the former is a conditional claim about the existence of useful verifier classes and the latter is a claim about specification coverage and property scope.
[fact; source: https://aclanthology.org/2024.naacl-long.366/; https://www.nature.com/articles/s42256-024-00976-7] No contradiction remains between "models may have some internal calibration" and "confidence is not an external verifier," because calibration helps ranking but does not provide an independent accept-reject oracle over consequential actions.
[inference; source: https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence; https://www.bankofengland.co.uk/prudential-regulation/publication/2023/may/model-risk-management-principles-for-banks; https://www.nist.gov/publications/artificial-intelligence-risk-management-framework-ai-rmf-10] The regulatory conclusion is consistent with the technical conclusion because the need for monitoring and governance is strongest exactly where external pre-consequence verification is weakest.

§5 Depth and Breadth Expansion

[inference; source: https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/; https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html] Technical lens: the strongest practical deployment boundary is not "code versus not code" but "formal artifact with enforceable verifier gate versus open-world action without one."
[inference; source: https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence; https://www.bankofengland.co.uk/prudential-regulation/publication/2023/may/model-risk-management-principles-for-banks; https://www.nist.gov/publications/artificial-intelligence-risk-management-framework-ai-rmf-10] Regulatory lens: governance obligations intensify as verifiability weakens, because firms move from provable property checks to procedural controls, challenge functions, and consequence management.
[inference; source: https://github.blog/2022-09-07-research-quantifying-github-copilots-impact-on-developer-productivity-and-happiness/; https://arxiv.org/abs/2107.03374; https://arxiv.org/abs/2203.07814] Economic lens: verifier-gated code generation scales because candidate outputs can be filtered cheaply by automation before scarce human review, while world-action outputs demand heavier human oversight precisely because cheap automated rejection is unavailable.
[inference; source: https://www.nature.com/articles/s42256-024-00976-7; https://aclanthology.org/2024.naacl-long.366/] Behavioral lens: fluent language increases the risk that humans mistake confidence cues for correctness, which further weakens any attempt to use human impression as a substitute acceptance mechanism for consequential actions.

§6 Synthesis

(This section seeds the Findings below.)

Executive summary:

[inference; source: https://gcc.gnu.org/onlinedocs/gcc-14.3.0/gcc/Warnings-and-Errors.html; https://www.typescriptlang.org/docs/handbook/2/basic-types.html; https://mypy.readthedocs.io/en/stable/getting_started.html; https://docs.astral.sh/ruff/; https://codeql.github.com/docs/codeql-overview/about-codeql/; https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/; https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html] The best-supported technical boundary is that LLM-assisted software engineering is the highest-confidence deployment domain only when generated artifacts are accepted through external verifier gates, while consequential world actions remain structurally lower-confidence because no comparable domain-complete pre-consequence verifier exists.
[inference; source: https://arxiv.org/abs/2107.03374; https://arxiv.org/abs/2203.07814; https://github.blog/2022-09-07-research-quantifying-github-copilots-impact-on-developer-productivity-and-happiness/] Empirical code-generation benchmarks and studies evaluate outputs with external tests, program judges, or behavior-based tasks, which is consistent with accepting code through verifier-gated workflows rather than through model confidence alone.
[inference; source: https://aclanthology.org/2024.naacl-long.366/; https://www.nature.com/articles/s42256-024-00976-7; https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence; https://www.bankofengland.co.uk/prudential-regulation/publication/2023/may/model-risk-management-principles-for-banks] Regulated financial institutions should therefore treat verifier-gated coding assistance as conditionally acceptable, but should require explicit human approval or deterministic non-LLM controls for consequential write actions and other impact-bearing decisions.
[inference; source: https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/; https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html] This is not an absolute safety claim about code, because assurance still depends on specification quality, environment, and the exact verifier stack, but it is a principled asymmetry that explains why software engineering currently offers the strongest LLM deployment surface.

Key findings:

[inference; source: https://gcc.gnu.org/onlinedocs/gcc-14.3.0/gcc/Warnings-and-Errors.html; https://www.typescriptlang.org/docs/handbook/2/basic-types.html; https://mypy.readthedocs.io/en/stable/getting_started.html; https://docs.astral.sh/ruff/; https://codeql.github.com/docs/codeql-overview/about-codeql/; https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/] Confidence: high. Code generation admits multiple independent verifier classes that can compute reproducible pre-release judgments over formal artifacts before software is accepted for release.
[inference; source: https://gcc.gnu.org/onlinedocs/gcc-14.3.0/gcc/Warnings-and-Errors.html; https://www.typescriptlang.org/docs/handbook/2/basic-types.html; https://mypy.readthedocs.io/en/stable/getting_started.html; https://docs.astral.sh/ruff/; https://codeql.github.com/docs/codeql-overview/about-codeql/; https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/; https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html] Confidence: high. Code is only conditionally verifiable rather than absolutely verifiable, because every compiler, analyzer, test suite, or proof tool certifies only the specific properties represented in its rules or formal specification.
[inference; source: https://arxiv.org/abs/2107.03374; https://arxiv.org/abs/2203.07814; https://github.blog/2022-09-07-research-quantifying-github-copilots-impact-on-developer-productivity-and-happiness/] Confidence: high. HumanEval, AlphaCode, and GitHub's controlled Copilot study all operationalize code quality through external tests or behavior-based evaluation, which shows that published code-generation performance is assessed through verifier-style gates rather than through model confidence alone.
[inference; source: https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/; https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html] Confidence: high. Formal methods strengthen the case for software engineering as a comparatively safe LLM domain, but they also show that assurance collapses when the specification is incomplete, wrong, or unavailable.
[inference; source: https://www.nist.gov/publications/towards-standard-identifying-and-managing-bias-artificial-intelligence; https://www.nist.gov/publications/artificial-intelligence-risk-management-framework-ai-rmf-10; https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence] Confidence: medium. Database writes, workflow triggers, outbound communications, customer decisions, and compliance judgments lack domain-complete external verifiers because their correctness depends on open-world facts, authorization context, ambiguity, and downstream effects.
[inference; source: https://aclanthology.org/2024.naacl-long.366/; https://www.nature.com/articles/s42256-024-00976-7] Confidence: high. LLM confidence cannot substitute for an external verifier in consequential domains because calibration remains imperfect and human users typically infer confidence from persuasive language rather than from the model's internal probabilities.
[inference; source: https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence; https://www.bankofengland.co.uk/prudential-regulation/publication/2023/october/artificial-intelligence-and-machine-learning; https://www.bankofengland.co.uk/prudential-regulation/publication/2023/may/model-risk-management-principles-for-banks; https://www.nist.gov/publications/artificial-intelligence-risk-management-framework-ai-rmf-10] Confidence: high. United Kingdom supervisory and NIST materials treat consequential AI primarily as a governance, monitoring, and model-risk problem, which is consistent with a domain where correctness cannot be mechanically certified before impact.
[inference; source: https://arxiv.org/abs/2107.03374; https://arxiv.org/abs/2203.07814; https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence; https://davidamitchell.github.io/Research/research/2026-04-26-access-control-amplification-agentic-operations.html; https://davidamitchell.github.io/Research/research/2026-04-26-implicit-rate-limiting-controls-agentic-ai-removal.html; https://davidamitchell.github.io/Research/research/2026-04-26-agentic-ai-regulatory-preconditions-control-failure-assessment.html] Confidence: medium. A regulated financial institution should place its default LLM deployment boundary at verifier-gated coding assistance and should require explicit human approval or deterministic non-LLM controls for consequential write actions.

Evidence map:

Claim	Source	Confidence	Notes
[inference] Code generation admits independent verifier classes that can compute pre-release judgments over formal artifacts.	https://gcc.gnu.org/onlinedocs/gcc-14.3.0/gcc/Warnings-and-Errors.html; https://www.typescriptlang.org/docs/handbook/2/basic-types.html; https://mypy.readthedocs.io/en/stable/getting_started.html; https://docs.astral.sh/ruff/; https://codeql.github.com/docs/codeql-overview/about-codeql/; https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/	high	The claim is about the existence of verifier classes, not about universal code safety.
[inference] Code remains only conditionally verifiable because each verifier checks only the properties encoded in its rules or specification.	https://gcc.gnu.org/onlinedocs/gcc-14.3.0/gcc/Warnings-and-Errors.html; https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/; https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html	high	This resolves the apparent tension between strong and weak claims about code safety.
[fact] Code-generation performance is operationalized through external tests, judges, and correctness suites.	https://arxiv.org/abs/2107.03374; https://arxiv.org/abs/2203.07814; https://github.blog/2022-09-07-research-quantifying-github-copilots-impact-on-developer-productivity-and-happiness/	high	HumanEval uses unit tests, AlphaCode uses behavior-based filtering, and GitHub's study scored correctness with a test suite.
[inference] Formal methods strengthen software-engineering assurance but expose the same specification bottleneck that limits verification in harder domains.	https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/; https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html	high	The distinction is strongest where specifications are crisp and enforceable.
[inference] Consequential world actions lack domain-complete external verifiers because correctness depends on open-world facts, ambiguity, and downstream effects.	https://www.nist.gov/publications/towards-standard-identifying-and-managing-bias-artificial-intelligence; https://www.nist.gov/publications/artificial-intelligence-risk-management-framework-ai-rmf-10; https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence	medium	Schema checks and authorization checks are partial, not domain-complete.
[inference] LLM confidence is not an adequate release criterion for consequential actions.	https://aclanthology.org/2024.naacl-long.366/; https://www.nature.com/articles/s42256-024-00976-7	high	Human users see language, not internal confidence, and calibration remains imperfect.
[inference] Regulatory texts frame consequential AI as a governance and model-risk problem rather than a mechanically verified one.	https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence; https://www.bankofengland.co.uk/prudential-regulation/publication/2023/october/artificial-intelligence-and-machine-learning; https://www.bankofengland.co.uk/prudential-regulation/publication/2023/may/model-risk-management-principles-for-banks; https://www.nist.gov/publications/artificial-intelligence-risk-management-framework-ai-rmf-10	high	This aligns with the absence of decisive pre-consequence verifiers for world actions.
[inference] The safe default deployment boundary in regulated finance is verifier-gated coding assistance, not autonomous consequential write action.	https://arxiv.org/abs/2107.03374; https://arxiv.org/abs/2203.07814; https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence; https://davidamitchell.github.io/Research/research/2026-04-26-access-control-amplification-agentic-operations.html; https://davidamitchell.github.io/Research/research/2026-04-26-implicit-rate-limiting-controls-agentic-ai-removal.html; https://davidamitchell.github.io/Research/research/2026-04-26-agentic-ai-regulatory-preconditions-control-failure-assessment.html	medium	Adjacent completed items sharpen the access, rate, and governance consequences once actions cross into the world.

Assumptions:

[assumption; source: https://www.nist.gov/publications/artificial-intelligence-risk-management-framework-ai-rmf-10; https://davidamitchell.github.io/Research/research/2026-04-26-agentic-ai-regulatory-preconditions-control-failure-assessment.html] When a workflow mixes verifier-gated code production with consequential write actions, the overall deployment classification should follow the least verifiable consequential step. Justification: the reviewed governance evidence evaluates risk at the boundary where harm can occur, not at the most testable upstream artifact.

Analysis:

[inference; source: https://arxiv.org/abs/2107.03374; https://arxiv.org/abs/2203.07814; https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/] The evidence supports a layered view of code assurance, where compilers and type checkers provide low-cost syntactic and semantic rejection, tests and program judges provide behavioral rejection, and formal methods provide the strongest but most specification-dependent guarantees.
[inference; source: https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html; https://www.nist.gov/publications/towards-standard-identifying-and-managing-bias-artificial-intelligence] The decisive contrast with world actions is the specification bottleneck: enterprise actions embed ambiguity, policy, entitlement, and real-world context that institutions usually cannot reduce to complete machine-checkable contracts.
[inference; source: https://aclanthology.org/2024.naacl-long.366/; https://www.nature.com/articles/s42256-024-00976-7] Confidence calibration evidence weakens any counterargument that internal model probabilities or fluent uncertainty language can stand in for external verification.
[inference; source: https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence; https://www.bankofengland.co.uk/prudential-regulation/publication/2023/may/model-risk-management-principles-for-banks; https://www.nist.gov/publications/artificial-intelligence-risk-management-framework-ai-rmf-10] The regulatory material does not prove the technical asymmetry directly, but it fits it closely: where pre-consequence verification is weak, firms are expected to compensate with governance, monitoring, accountability, and human challenge rather than with automated acceptance.

Risks, gaps, uncertainties:

[fact; source: https://github.blog/2022-09-07-research-quantifying-github-copilots-impact-on-developer-productivity-and-happiness/] The GitHub Copilot study is strongest on productivity under a test-gated task and weaker on long-run defect rates or production incident rates.
[fact; source: https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html] The neural-network verification source is about formal specification limits rather than about LLM world-action agents specifically, so part of the asymmetry argument remains an inference from specification theory.
[inference; source: https://www.nist.gov/publications/towards-standard-identifying-and-managing-bias-artificial-intelligence; https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence] Some narrow world actions may admit partial machine-checkable contracts, such as field-level validation, deterministic policy rules, or dual-control approval gates, so "unverifiable" here means "not domain-completely externally verifiable" rather than "completely unconstrained."
[inference; source: https://aclanthology.org/2024.naacl-long.366/; https://www.nature.com/articles/s42256-024-00976-7] Calibration research is evolving, and future models may express uncertainty better than current ones, but that would still not by itself solve the open-world oracle problem for consequential actions.

Open questions:

[inference; source: https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html] Which regulated workflow classes can realistically be reduced to machine-checkable contracts strong enough to create a narrow external verifier for a consequential step?
[inference; source: https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/] What minimum verifier stack, compilation, type-checking, testing, static analysis, human review, and rollback, is sufficient for regulated institutions to classify AI-assisted software engineering as operationally acceptable?
[inference; source: https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence; https://www.bankofengland.co.uk/prudential-regulation/publication/2023/may/model-risk-management-principles-for-banks] How should a firm evidence to supervisors that a mixed workflow's consequential step is still human-controlled when upstream drafting or coding was LLM-assisted?

§7 Recursive Review

[inference; source: https://davidamitchell.github.io/Research/research/2026-04-26-access-control-amplification-agentic-operations.html; https://davidamitchell.github.io/Research/research/2026-04-26-implicit-rate-limiting-controls-agentic-ai-removal.html; https://davidamitchell.github.io/Research/research/2026-04-26-agentic-ai-regulatory-preconditions-control-failure-assessment.html] Review result: repository cross-references were added for adjacent governance surfaces that qualify the deployment-boundary conclusion.
[inference; source: https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html; https://aclanthology.org/2024.naacl-long.366/] Residual uncertainty remains around how far narrow world-action contracts can be formalized, but that uncertainty weakens the strength of the boundary only at the margin and does not overturn the main asymmetry.

Findings

(Populated from §6 Synthesis above.)

Executive Summary

[inference; source: https://gcc.gnu.org/onlinedocs/gcc-14.3.0/gcc/Warnings-and-Errors.html; https://www.typescriptlang.org/docs/handbook/2/basic-types.html; https://mypy.readthedocs.io/en/stable/getting_started.html; https://docs.astral.sh/ruff/; https://codeql.github.com/docs/codeql-overview/about-codeql/; https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/; https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html] The best-supported technical boundary is that LLM-assisted software engineering is the highest-confidence deployment domain only when generated artifacts are accepted through external verifier gates, while consequential world actions remain structurally lower-confidence because no comparable domain-complete pre-consequence verifier exists. [inference; source: https://arxiv.org/abs/2107.03374; https://arxiv.org/abs/2203.07814; https://github.blog/2022-09-07-research-quantifying-github-copilots-impact-on-developer-productivity-and-happiness/] Empirical code-generation benchmarks and studies evaluate outputs with external tests, program judges, or behavior-based tasks, which is consistent with accepting code through verifier-gated workflows rather than through model confidence alone. [inference; source: https://aclanthology.org/2024.naacl-long.366/; https://www.nature.com/articles/s42256-024-00976-7; https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence; https://www.bankofengland.co.uk/prudential-regulation/publication/2023/may/model-risk-management-principles-for-banks] Regulated financial institutions should therefore treat verifier-gated coding assistance as conditionally acceptable, but should require explicit human approval or deterministic non-LLM controls for consequential write actions and other impact-bearing decisions. [inference; source: https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/; https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html] This is not an absolute safety claim about code, because assurance still depends on specification quality, environment, and the exact verifier stack, but it is a principled asymmetry that explains why software engineering currently offers the strongest LLM deployment surface.

Key Findings

[inference; source: https://gcc.gnu.org/onlinedocs/gcc-14.3.0/gcc/Warnings-and-Errors.html; https://www.typescriptlang.org/docs/handbook/2/basic-types.html; https://mypy.readthedocs.io/en/stable/getting_started.html; https://docs.astral.sh/ruff/; https://codeql.github.com/docs/codeql-overview/about-codeql/; https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/] Confidence: high. Code generation admits multiple independent verifier classes that can compute reproducible pre-release judgments over formal artifacts before software is accepted for release.
[inference; source: https://gcc.gnu.org/onlinedocs/gcc-14.3.0/gcc/Warnings-and-Errors.html; https://www.typescriptlang.org/docs/handbook/2/basic-types.html; https://mypy.readthedocs.io/en/stable/getting_started.html; https://docs.astral.sh/ruff/; https://codeql.github.com/docs/codeql-overview/about-codeql/; https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/; https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html] Confidence: high. Code is only conditionally verifiable rather than absolutely verifiable, because every compiler, analyzer, test suite, or proof tool certifies only the specific properties represented in its rules or formal specification.
[inference; source: https://arxiv.org/abs/2107.03374; https://arxiv.org/abs/2203.07814; https://github.blog/2022-09-07-research-quantifying-github-copilots-impact-on-developer-productivity-and-happiness/] Confidence: high. HumanEval, AlphaCode, and GitHub's controlled Copilot study all operationalize code quality through external tests or behavior-based evaluation, which shows that published code-generation performance is assessed through verifier-style gates rather than through model confidence alone.
[inference; source: https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/; https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html] Confidence: high. Formal methods strengthen the case for software engineering as a comparatively safe LLM domain, but they also show that assurance collapses when the specification is incomplete, wrong, or unavailable.
[inference; source: https://www.nist.gov/publications/towards-standard-identifying-and-managing-bias-artificial-intelligence; https://www.nist.gov/publications/artificial-intelligence-risk-management-framework-ai-rmf-10; https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence] Confidence: medium. Database writes, workflow triggers, outbound communications, customer decisions, and compliance judgments lack domain-complete external verifiers because their correctness depends on open-world facts, authorization context, ambiguity, and downstream effects.
[inference; source: https://aclanthology.org/2024.naacl-long.366/; https://www.nature.com/articles/s42256-024-00976-7] Confidence: high. LLM confidence cannot substitute for an external verifier in consequential domains because calibration remains imperfect and human users typically infer confidence from persuasive language rather than from the model's internal probabilities.
[inference; source: https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence; https://www.bankofengland.co.uk/prudential-regulation/publication/2023/october/artificial-intelligence-and-machine-learning; https://www.bankofengland.co.uk/prudential-regulation/publication/2023/may/model-risk-management-principles-for-banks; https://www.nist.gov/publications/artificial-intelligence-risk-management-framework-ai-rmf-10] Confidence: high. United Kingdom supervisory and NIST materials treat consequential AI primarily as a governance, monitoring, and model-risk problem, which is consistent with a domain where correctness cannot be mechanically certified before impact.
[inference; source: https://arxiv.org/abs/2107.03374; https://arxiv.org/abs/2203.07814; https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence; https://davidamitchell.github.io/Research/research/2026-04-26-access-control-amplification-agentic-operations.html; https://davidamitchell.github.io/Research/research/2026-04-26-implicit-rate-limiting-controls-agentic-ai-removal.html; https://davidamitchell.github.io/Research/research/2026-04-26-agentic-ai-regulatory-preconditions-control-failure-assessment.html] Confidence: medium. A regulated financial institution should place its default LLM deployment boundary at verifier-gated coding assistance and should require explicit human approval or deterministic non-LLM controls for consequential write actions.

Evidence Map

Claim	Source	Confidence	Notes
[inference] Code generation admits independent verifier classes that can compute pre-release judgments over formal artifacts.	https://gcc.gnu.org/onlinedocs/gcc-14.3.0/gcc/Warnings-and-Errors.html; https://www.typescriptlang.org/docs/handbook/2/basic-types.html; https://mypy.readthedocs.io/en/stable/getting_started.html; https://docs.astral.sh/ruff/; https://codeql.github.com/docs/codeql-overview/about-codeql/; https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/	high	The claim is about the existence of verifier classes, not about universal code safety.
[inference] Code remains only conditionally verifiable because each verifier checks only the properties encoded in its rules or specification.	https://gcc.gnu.org/onlinedocs/gcc-14.3.0/gcc/Warnings-and-Errors.html; https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/; https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html	high	This resolves the apparent tension between strong and weak claims about code safety.
[fact] Code-generation performance is operationalized through external tests, judges, and correctness suites.	https://arxiv.org/abs/2107.03374; https://arxiv.org/abs/2203.07814; https://github.blog/2022-09-07-research-quantifying-github-copilots-impact-on-developer-productivity-and-happiness/	high	HumanEval uses unit tests, AlphaCode uses behavior-based filtering, and GitHub's study scored correctness with a test suite.
[inference] Formal methods strengthen software-engineering assurance but expose the same specification bottleneck that limits verification in harder domains.	https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/; https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html	high	The distinction is strongest where specifications are crisp and enforceable.
[inference] Consequential world actions lack domain-complete external verifiers because correctness depends on open-world facts, ambiguity, and downstream effects.	https://www.nist.gov/publications/towards-standard-identifying-and-managing-bias-artificial-intelligence; https://www.nist.gov/publications/artificial-intelligence-risk-management-framework-ai-rmf-10; https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence	medium	Schema checks and authorization checks are partial, not domain-complete.
[inference] LLM confidence is not an adequate release criterion for consequential actions.	https://aclanthology.org/2024.naacl-long.366/; https://www.nature.com/articles/s42256-024-00976-7	high	Human users see language, not internal confidence, and calibration remains imperfect.
[inference] Regulatory texts frame consequential AI as a governance and model-risk problem rather than a mechanically verified one.	https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence; https://www.bankofengland.co.uk/prudential-regulation/publication/2023/october/artificial-intelligence-and-machine-learning; https://www.bankofengland.co.uk/prudential-regulation/publication/2023/may/model-risk-management-principles-for-banks; https://www.nist.gov/publications/artificial-intelligence-risk-management-framework-ai-rmf-10	high	This aligns with the absence of decisive pre-consequence verifiers for world actions.
[inference] The safe default deployment boundary in regulated finance is verifier-gated coding assistance, not autonomous consequential write action.	https://arxiv.org/abs/2107.03374; https://arxiv.org/abs/2203.07814; https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence; https://davidamitchell.github.io/Research/research/2026-04-26-access-control-amplification-agentic-operations.html; https://davidamitchell.github.io/Research/research/2026-04-26-implicit-rate-limiting-controls-agentic-ai-removal.html; https://davidamitchell.github.io/Research/research/2026-04-26-agentic-ai-regulatory-preconditions-control-failure-assessment.html	medium	Adjacent completed items sharpen the access, rate, and governance consequences once actions cross into the world.

Assumptions

[assumption; source: https://www.nist.gov/publications/artificial-intelligence-risk-management-framework-ai-rmf-10; https://davidamitchell.github.io/Research/research/2026-04-26-agentic-ai-regulatory-preconditions-control-failure-assessment.html] Assumption: When a workflow mixes verifier-gated code production with consequential write actions, the overall deployment classification should follow the least verifiable consequential step. Justification: The reviewed governance evidence evaluates risk at the boundary where harm can occur, not at the most testable upstream artifact.

Analysis

[inference; source: https://arxiv.org/abs/2107.03374; https://arxiv.org/abs/2203.07814; https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/] The evidence supports a layered view of code assurance, where compilers and type checkers provide low-cost syntactic and semantic rejection, tests and program judges provide behavioral rejection, and formal methods provide the strongest but most specification-dependent guarantees.
[inference; source: https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html; https://www.nist.gov/publications/towards-standard-identifying-and-managing-bias-artificial-intelligence] The decisive contrast with world actions is the specification bottleneck: enterprise actions embed ambiguity, policy, entitlement, and real-world context that institutions usually cannot reduce to complete machine-checkable contracts.
[inference; source: https://aclanthology.org/2024.naacl-long.366/; https://www.nature.com/articles/s42256-024-00976-7] Confidence calibration evidence weakens any counterargument that internal model probabilities or fluent uncertainty language can stand in for external verification.
[inference; source: https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence; https://www.bankofengland.co.uk/prudential-regulation/publication/2023/may/model-risk-management-principles-for-banks; https://www.nist.gov/publications/artificial-intelligence-risk-management-framework-ai-rmf-10] The regulatory material does not prove the technical asymmetry directly, but it fits it closely: where pre-consequence verification is weak, firms are expected to compensate with governance, monitoring, accountability, and human challenge rather than with automated acceptance.

Risks, Gaps, and Uncertainties

[fact; source: https://github.blog/2022-09-07-research-quantifying-github-copilots-impact-on-developer-productivity-and-happiness/] The GitHub Copilot study is strongest on productivity under a test-gated task and weaker on long-run defect rates or production incident rates.
[fact; source: https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html] The neural-network verification source is about formal specification limits rather than about LLM world-action agents specifically, so part of the asymmetry argument remains an inference from specification theory.
[inference; source: https://www.nist.gov/publications/towards-standard-identifying-and-managing-bias-artificial-intelligence; https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence] Some narrow world actions may admit partial machine-checkable contracts, such as field-level validation, deterministic policy rules, or dual-control approval gates, so "unverifiable" here means "not domain-completely externally verifiable" rather than "completely unconstrained."
[inference; source: https://aclanthology.org/2024.naacl-long.366/; https://www.nature.com/articles/s42256-024-00976-7] Calibration research is evolving, and future models may express uncertainty better than current ones, but that would still not by itself solve the open-world oracle problem for consequential actions.

Open Questions

[inference; source: https://people.eecs.berkeley.edu/~sseshia/pubs/b2hd-seshia-atva18.html] Which regulated workflow classes can realistically be reduced to machine-checkable contracts strong enough to create a narrow external verifier for a consequential step?
[inference; source: https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/] What minimum verifier stack, compilation, type-checking, testing, static analysis, human review, and rollback, is sufficient for regulated institutions to classify AI-assisted software engineering as operationally acceptable?
[inference; source: https://www.bankofengland.co.uk/prudential-regulation/publication/2022/october/artificial-intelligence; https://www.bankofengland.co.uk/prudential-regulation/publication/2023/may/model-risk-management-principles-for-banks] How should a firm evidence to supervisors that a mixed workflow's consequential step is still human-controlled when upstream drafting or coding was LLM-assisted?