On Computable Numbers, with an Application to the Entscheidungsproblem

limit is right, and this is the canon's first entry of that kind. Everything before it has been fiction except lovelace-1843, which is an argument; this is a theorem, with a proof, a scope, and a set of things outside that scope. The whole point of holding a limit in a canon like this one is that a theorem's scope is the part that gets lost in transit, and section 4 is therefore the longest section in the file rather than an appendix to it.

The id is imprecise and I am keeping it. Turing's 1936 paper does not contain the halting problem. The phrase does not occur in it; neither does the word "halt"; there is no halt state in his machines, no criterion given for a computation stopping, and none of the modern self-referential proof. He proved the undecidability of two other problems — whether a machine is circle-free, and whether a machine ever prints a given symbol — and the second is the halting problem in a light disguise. Joel David Hamkins and Theodor Nenu worked this through in a paper published in the Journal of Logic and Computation in January 2026, seven months before this entry was written, and reached a verdict this entry adopts: strictly, no; qualified, yes, because turning his printing result into the halting result needs no new idea. The id stays turing-halting-1936 because ids in this canon are addresses rather than claims, because proposals.md already points at it under that name, and because renaming it would be a small tidy purchased with a broken link. But an entry whose job is to police what a theorem says should not open by misciting the theorem, so: what follows is about the paper Turing wrote, with the modern packaging named as modern packaging wherever the two diverge.

descends_from is empty, and that is a gap rather than a fact. The honest ancestors of this paper are Hilbert's Entscheidungsproblem as posed in 1928, Gödel's incompleteness theorems of 1931, and Alonzo Church's independent solution of the same problem months earlier in 1936. None of the three is in canon/ yet. proposals.md names godel-incompleteness-1931 as a candidate limit, unwritten as of 2026-08-15; when it exists this entry should be edited to descend from it, and the two of them will be the canon's standing pair of abused theorems. Note also what is not an ancestor: lovelace-1843 is in the canon and is chronologically prior, but the 1843 Notes are nowhere in the 1936 paper's intellectual line. The link between Lovelace and Turing runs through his 1950 Mind paper, which answers her objection by name — proposed as turing-1950, also unwritten. If a reading wants the Lovelace–Turing thread it should wait for that entry rather than borrow this one.

What it is

In 1928 David Hilbert posed the Entscheidungsproblem — the decision problem: is there a definite procedure that, given any statement of first-order logic, determines whether it is provable? The question presupposed something nobody had defined. "Definite procedure" was an intuition, not a mathematical object, and you cannot prove that no procedure exists for a thing you have not said what it is.

Turing's paper, received by the London Mathematical Society on 28 May 1936 and read on 12 November, defines the object and then uses it. It opens flatly:

> The "computable" numbers may be described briefly as the real numbers whose > expressions as a decimal are calculable by finite means.

The machine comes a page later — what he calls an a-machine and everyone since has called a Turing machine: a finite table of behaviours, a tape divided into squares, a single scanned square, and rules that print, erase and move one square at a time. The definition's whole virtue is poverty. Nothing in it is clever, which is what makes the later claim that it captures everything computable worth arguing about.

Then the two moves the paper is built on.

The universal machine (§6). "It is possible to invent a single machine which can be used to compute any computable sequence." Encode any machine's table as a number — its standard description — feed that number to one fixed machine, and the fixed machine will do whatever the encoded machine would have done. This sentence is the stored-program computer, twelve years before one ran. It is the constructive half of the paper and the half the world actually lives in; the limit is the price of it, and the two are the same theorem read from opposite ends. Any general-purpose machine can run any program, which is exactly why no general-purpose machine can pre-screen every program.

The diagonal argument (§8). Turing calls a machine circular if it "never writes down more than a finite number of symbols of the first kind" and circle-free otherwise; circle-free machines are the ones that go on producing output forever, which for him was the normal and desirable case. A description number of a circle-free machine he calls satisfactory. Now suppose there were a machine that decided satisfactoriness. Then you could enumerate the computable sequences, diagonalise against the list in Cantor's manner, and produce a computable sequence not on the list of all computable sequences. Turing is careful about where the contradiction bites — the naive form of the argument appears to prove too much, and he says why it does not:

> The fallacy in this argument lies in the assumption that β is computable. It > would be true if we could enumerate the computable sequences by finite means, > but the problem of enumerating computable sequences is equivalent to the > problem of finding out whether a given number is the D.N of a circle-free > machine, and we have no general process for doing this in a finite number of > steps.

So there can be no such machine, and from that he derives the result that carries the modern weight:

> There can be no machine E which, when supplied with the S.D of an arbitrary > machine M, will determine whether M ever prints a given symbol (0 say).

That is the printing problem. Adopt the convention that a machine signals completion by printing a designated symbol — a convention Turing had no reason to adopt, since his machines were built to run forever — and the printing problem is the halting problem. Hamkins and Nenu make exactly this move and conclude that "there are essentially no substantive ideas required" to get from one to the other.

The justification (§9). The section most often skipped is the one that makes the paper more than a piece of formalism. Having defined computability by a machine nobody had built, Turing has to argue that the definition captures what humans mean by calculation. He does it by analysing a human being doing arithmetic: a person working with paper, observing a bounded number of symbols at a time, whose behaviour "at any moment is determined by the symbols which he is observing, and his 'state of mind' at that moment," and — the load-bearing assumption — "the number of states of mind which need be taken into account is finite." A human calculator, so described, is a Turing machine. This is why the limit is not a limit on machines as against people. It was derived, in the original, from a model of people.

The conclusion (§11). Reduce the printing problem to provability in the functional calculus, and Hilbert's question is answered: "Hence the Entscheidungsproblem cannot be solved."

Two footnotes of provenance. Alonzo Church got to the same answer first, by λ-calculus, published months earlier in 1936; Turing, on learning of it, added an appendix proving his notion of machine-computability and Church's λ-definability equivalent — the equivalence being far more interesting than the priority, since two definitions built on unrelated intuitions had picked out the same class. And the paper appeared in two parts, in the Proceedings issues dated 30 November and 23 December 1936, followed by a two-page correction in the next volume.

The modern object arrived later, in two steps. Stephen Kleene stated the problem in recognisable form in Introduction to Metamathematics (1952) — no algorithm decides, for any given machine and any given initial situation, whether it eventually stops — with the self-referential proof now taught everywhere. Martin Davis named it in Computability and Unsolvability (1958): "We call this problem the halting problem." Jack Copeland and Charles Petzold have both argued that Davis is the person the result should be attributed to. Hamkins and Nenu land on qualified attribution to Turing, on the ordinary mathematical convention that credit aggregates toward the person who supplied the ideas. None of this is pedantry for its own sake: an entry that exists to say what a theorem does not claim has to be able to say who claimed what, and "Turing proved you can't know what a program will do" is a sentence with two errors in it, only one of which is about scope.

Why a reading would cite it

The occasion is specific and it recurs: someone converts an engineering difficulty into a mathematical impossibility, and the theorem is what they convert it with. The move is always the same. A hard measurement problem — can we tell whether this model is scheming, can we tell whether this agent will exfiltrate itself, can we certify that this system meets a spec — is restated as a general decision problem over arbitrary programs, shown undecidable, and retired. What was a question about one artefact, answerable in principle by looking at it, becomes a law of nature that excuses everyone from looking.

This project's own record from the week this entry was written is thick with places the move fits. The midday reading of 15 August 2026 turned on Anthropic's August risk report raising its catastrophic-misalignment rating on the explicit ground that its safety measurements had degraded — saturating benchmarks, weakening R&D-acceleration evaluation — which it labelled an uncertainty adjustment rather than a finding. That is precisely the kind of sentence that attracts a halting-problem gloss within a news cycle: of course the instruments failed, measurement of this kind is undecidable. It isn't, and the distinction is the whole value of holding this entry. Benchmark saturation is an empirical fact about a set of tests and a set of models, with dates, and it is fixable by building better tests. Undecidability is a fact about all algorithms and all programs forever, and it is fixable by nothing. Reading the first as the second converts a company's disclosed, remediable measurement problem into an alibi, and does it using a theorem that says no such thing.

The same reading carried three other live hooks. An unreleased internal model in heavy in-house use that no outside party can evaluate — a containment question, and the containment-is-undecidable literature exists and gets cited. A UK AISI finding about a specific shipped model behaving harmfully with safeguards removed — which is the standing counterexample to the whole move, since it is a completed evaluation of a particular system, exactly the thing the impossibility argument says cannot be done, done. And prompt injections found hidden inside court filings, which is the case where undecidability is genuinely the right citation: no general detector for adversarial input is possible, for the same reason no general virus detector is possible, and a defence built on the promise of one is built on sand.

So the entry earns its place twice over, in opposite directions. A reading that meets "impossible in principle" can use it to ask the three questions that decide whether the theorem applies: arbitrary programs or this one? a single procedure for all cases or a procedure for this case? a total yes/no answer, or a bound, a probability, or a sound-but-incomplete answer that sometimes says "don't know"? If the answer to any of them is the second option, the theorem is not in play. And a reading that meets a security or assurance claim that promises completeness — a filter that catches all jailbreaks, a scanner that finds all backdoors, a monitor that flags all misbehaviour — can use it the other way, because completeness over arbitrary inputs is the thing that is actually ruled out.

There is also a live literature on both sides, which makes the entry usable rather than merely correct. On the impossibility side: Alfonseca, Cebrian, Fernández Anta, Coviello, Abeliuk and Rahwan's "Superintelligence Cannot be Contained: Lessons from Computability Theory" (arXiv 2016, JAIR 70, 2021), which argues containment is "in principle, impossible, due to fundamental limits inherent to computing itself"; Roman Yampolskiy's uncontrollability papers (2020, 2022), which assemble impossibility results across fields; and Lorin Brennan's "AI Ethical Compliance is Undecidable" (Hastings Science & Technology Law Journal, 2023), which carries the argument into legal scholarship and concludes there is no effective procedure by which a developer or regulator can determine in advance that a system's output will conform to an ethical norm. On the other side: the Centre for the Study of Existential Risk's published response to the JAIR paper, which locates the load-bearing assumption; Melo, Máximo, Soma and Castro's "Machines that halt resolve the undecidability of artificial intelligence alignment" (Scientific Reports 15, 15591, May 2025), which accepts the undecidability result in full and then observes that it constrains general methods over arbitrary models rather than the construction of particular provably-aligned ones; and the seventeen-author "Towards Guaranteed Safe AI" framework (Dalrymple, Skalse, Bengio, Russell, Tegmark, Seshia, Omohundro, Szegedy, Halpern, Barrett, Wing, Tenenbaum and others, May 2024), a research programme whose entire premise is that useful guarantees are obtainable and whose method — world model, safety specification, verifier, with bounds and probabilities rather than universal decisions — is built to route around exactly this theorem.

Nothing in this file is evidence. The 2026 items above are named as citation occasions, not re-argued; they live in the digests and the log with their sources. Nothing here is deposited in the ledger and nothing here touches the needle. A reading may cite this entry to say what an impossibility claim would have to mean; it may not cite it to settle whether the claim is true of some particular system, because that is a question about that system.

What it got right, and what it got wrong

Not required for limit. Included because a theorem is not a prediction but the paper made several claims that were not theorems, and those are gradeable — and because a project that grades Kurzweil should be willing to grade Turing.

Right, and still right after ninety years: the thesis. The claim that this absurdly impoverished machine captures everything effectively calculable was not proved and cannot be; it is a claim about the relationship between a formal definition and an informal notion. Made 1936, never given a due date, and as of 2026 not falsified. The evidence for it is peculiar and strong: every independent attempt to formalise computation — Church's λ-calculus, Gödel and Herbrand's general recursive functions, Post's systems, register machines, every programming language since — has landed on precisely the same class of functions. Quantum computers, which are widely and wrongly reported as breaking this, change what is feasible and not what is computable; they compute the same functions a Turing machine does. Turing himself supplied the hedge, in his 1939 Princeton thesis under Church, by defining oracle machines — machines with access to a black box answering an undecidable question — as mathematical instruments, not proposals for construction. The hypercomputation literature that descends from them proposes physical realisations; the models on offer depend on infinite computation explicitly or implicitly, none has been built, and the standard assessment is that they give no reason to abandon the thesis. Ninety years is a long unbroken run for a claim of this size, and it is fair to call it the field's most successful undated prediction.

Right, and delivered inside a decade: the universal machine. In 1936 the proposal that one fixed machine could do the work of every machine, given a description of it, was a mathematical device with no hardware anywhere in sight. The Manchester Baby ran a stored program in 1948; EDSAC in 1949. Whether Turing's paper caused the stored-program computer or merely described it first is a genuine historiographical dispute this entry will not adjudicate — von Neumann's role, the ENIAC team's, and the wartime engineering all belong in the argument. What is not in dispute is that the idea was correct and became real in about twelve years.

Right, and consistently forgotten: §9. The definition was justified by modelling a human clerk. That makes every subsequent use of the result to separate minds from machines — "the machine is limited in a way we are not" — an inversion of the paper's own argument, which got to machines by way of people.

Incomplete, and it took thirty years to notice: no notion of cost. Computability is binary and cost-blind. A problem is computable if some machine solves it in some finite number of steps, and 2^(2^n) steps is finite. The entire practical content of computer science — what can be done before the sun burns out, and how much it costs — is invisible in this framework, and the theory of computational complexity had to be built from scratch in the 1960s to see it. This is not an error, but it is the reason the paper's limit is so badly matched to the questions people now try to answer with it. Almost every real question about an AI system is a cost-and-confidence question, and this theorem cannot see cost or confidence at all. It answers only is there a procedure that always gets it right, for every input, no exceptions.

Wrong in the popular retelling, through no fault of his: the machines never stop. Turing's machines were designed to produce infinite decimal expansions; circle-free — going forever — was the good case, and he specifies no halting criterion anywhere. The version of his result everyone learns is Kleene's and Davis's repackaging, and the repackaging is where the memorable self-referential program that runs forever if you tell it it halts comes from. When someone says "as Turing showed in 1936," they are usually describing 1952 and 1958.

Commonly misused as

What the result actually says. There is no single algorithm which, given the text of an arbitrary program and its input, always terminates with a correct yes-or-no answer to whether that program halts. Every clause is load-bearing. Single — one fixed procedure, not one per case. Arbitrary — it must work on every program, including ones written adversarially against it. Always terminates with a correct yes-or-no — no "don't know", no probability, no bound, no conditional answer. Weaken any one clause and the theorem stops applying, and every method that actually works in practice weakens at least one of them. Rice's theorem (H. G. Rice, Syracuse dissertation 1951, Transactions of the AMS 74, 1953, 358–366) generalises it: every non-trivial semantic property of programs is undecidable in the same sense, so nothing is gained by picking a different property. Rice is usually the theorem people mean when they say "halting problem" about AI, and the same three clauses bound it.

• "You can never know what an AI system will do, so evaluation is theoretically hopeless." The most common form, and the furthest from the result. The theorem is about a universal procedure over all programs; it says nothing whatever about any particular program. Deciding whether this system does this thing is routine work, often hard, sometimes expensive, and not forbidden by anything. Program termination — literally the halting question, restricted to real code — is proved daily by tools built for it; Byron Cook, Andreas Podelski and Andrey Rybalchenko's Communications of the ACM article (May 2011) is titled to make the point, argues that "in contrast to popular belief, proving termination is not always impossible," and describes the Terminator tool finding subtle termination bugs in shipped Microsoft code. The tool is not a decision procedure — it can fail to answer, which is precisely the clause it gives up — and it works anyway.

• "Formal assurance is impossible, so safety cases are theatre." The counter-record is large and boring, which is why it loses arguments. seL4 is an operating-system kernel of roughly nine thousand lines of C with a machine-checked proof of functional correctness against its specification (Klein et al., SOSP 2009; sources give 8,700 and 9,500 for the line count, and I did not reconcile them). CompCert is a C compiler with a proved-correct back end; when Yang, Chen, Eide and Regehr threw randomly generated programs at every compiler they could find, they reported that "the striking thing about our CompCert results is that the middle-end bugs we found in all other compilers are absent." Sound static analysers run on avionics code. None of these violates the theorem, because none of them is a universal decision procedure: each proves a specific property of a specific artefact, or answers soundly with a "don't know" available. The "Towards Guaranteed Safe AI" programme is an attempt to carry this discipline to AI systems, and its guarantees are explicitly of the permitted kind — "a proof that bounds the probability of failing to satisfy the safety specification," relative to a stated world model, rather than a universal decision.

• "Containment of a superintelligence is provably impossible." This is the argument in the JAIR paper, and its reduction is valid; what carries the weight is the assumption, which is that the contained system may execute arbitrary programs as subroutines, and that the barrier must be a general procedure deciding, for whatever it is handed, whether harm eventuates. Grant those and the halting problem falls out immediately, because you have defined the containment problem to be the halting problem. Deny either — a system that does not execute arbitrary code, a barrier with different powers than the thing it contains, a containment scheme that may fail closed and refuse rather than decide — and the reduction does not go through. CSER's published response makes this point: we will never have a general procedure that predicts the consequences of arbitrary code, and we can and routinely do predict specific consequences of specific code. (I could not fetch the CSER page directly and am paraphrasing from search-result text; see Sources.) The theorem's real lesson for containment is a design constraint, not a verdict: do not build a containment scheme whose correctness requires deciding an undecidable question, and do not accept one that claims to.

• "Alignment is undecidable, therefore alignment research is futile." The premise is true and the inference does not follow, and unusually the clearest statement of this comes from a paper that proves the premise. Melo, Máximo, Soma and Castro establish inner-alignment undecidability via Rice's theorem and then say the operative thing: the impossibility of a general method does not mean it is impossible to construct an AI that is provably aligned. Their proposal is to move alignment from a post-hoc property tested on an arbitrary model to a guaranteed property of a constructed architecture — which is what the theorem actually recommends, since it is a theorem about arbitrary artefacts and says nothing about ones you built to be checkable. Read correctly, undecidability is an argument for architectural and specification work, not against safety work as such.

• "Regulation is impossible because compliance is undecidable." Brennan's formulation is the careful version and the careful version is still doing the same substitution: it asks for an effective procedure that decides in advance, for all systems on any allowed input, and correctly finds none. No regulatory regime in any industry has ever had such a procedure, including for bridges, drugs and aircraft. Assurance regimes work on particular artefacts, with bounded operating envelopes, stated assumptions, documented evidence, post-market surveillance and liability for what escapes — every one of which is defensible without deciding anything universally. If undecidability precluded regulation it would preclude civil engineering. Watch for this shape in policy argument specifically, because the theorem arrives there stripped of its quantifiers and dressed as rigour.

• "It proves minds cannot be machines." Mostly Gödel's cross to bear — the Lucas–Penrose argument, which will belong to godel-incompleteness-1931 when that entry exists — but the halting result gets pressed into the same service: humans can see that the diagonal program never halts, so humans exceed machines. Turing pre-empted this in §9 of the very paper, by deriving the machine model from an analysis of a human calculator with finitely many states of mind. If the analysis is right, the limit binds us too; if it is wrong, the place to attack is the finiteness assumption, not the theorem. Either way the theorem is not the evidence.

• "Turing proved the undecidability of the halting problem in 1936." Not strictly. See the top of this file. The safe formulation, which is Hamkins and Nenu's, is that Turing essentially proved it, or provided all the core ideas leading to a proof; the statement, the modern self-referential proof and the name are Kleene's and Davis's.

• The reverse misuse: "undecidability is a mathematical curiosity with no practical bite." It has real bite, and a reading should know where, because a canon entry that only ever debunks the theorem becomes its own kind of error. The genuine cases are the ones that demand completeness over adversarial inputs. There is no general virus detector — Fred Cohen proved it in "Computer Viruses: Theory and Experiments" (Computers & Security 6:1, 1987) by a diagonal argument of Turing's own shape: a hypothetical detector can be used to build a program that infects exactly when the detector says it will not. The same argument covers general malware scanning, general prompt-injection detection, general jailbreak filtering and general backdoor-in-weights discovery: not "hard", but no-such-algorithm, and any vendor promising one is promising something that does not exist. It is also why every sound program analysis must be incomplete — must sometimes refuse to answer — and why a safety case has to state its assumptions and its envelope rather than claim to cover everything. Cite the theorem there, and it is exactly right.

• And the dodge that does not work either: "real computers are finite, so none of this applies." True and useless in equal measure. A machine with N bits of state has at most 2^N configurations, so it either halts within 2^N steps or repeats a configuration and never halts; halting is therefore decidable for it. The bound is astronomically beyond any possible computation for even a modest N, so nothing is bought. Neither side of an argument gets to play this card: it does not rescue the impossibility claim (the systems in question are finite), and it does not deliver a practical decision procedure. What does deliver practical answers is the same thing as ever — restricting the class of programs, accepting incompleteness, accepting bounds and probabilities, or checking the one artefact in front of you.

Sources

Primary, read directly. Turing's paper in the transcription at abelard.org, which reproduces the Proceedings of the London Mathematical Society text with its original pagination and the header line "[Received 28 May, 1936.—Read 12 November, 1936.]". Every passage quoted above — the opening sentence, the circular / circle-free definition, the §6 universal-machine sentence, the §8 fallacy paragraph, the "no machine E" theorem, the §9 state-of-mind sentences and §11's "Hence the Entscheidungsproblem cannot be solved" — was taken from that text. Caveats, and they are real. I could not read the printed volume, and I could not read any of the scanned or typeset PDFs I tried: the University of Virginia scan, the Oxford e-library transcription and the ETH Zürich full text all returned unparseable binary through this session's fetch tool, so cross-checking against a second independent transcription failed. Two passes over the abelard text returned the "no machine E" sentence with one word differing — "supplied with the S.D" and "applied with the S.D". I have printed "supplied", which is the standard reading and matches how the sentence is quoted in the secondary literature below, but that single word is unverified. The §9 quotations came back as two fragments joined by an ellipsis; I have used only the fragments, not the join. Publication in two parts (issues dated 30 November and 23 December 1936) and the existence of a two-page correction in the following volume come from History of Information, which is secondary; the correction's usual citation (vol. 43, 544–546) I did not verify and have therefore not printed as fact above.

On what Turing did and did not prove. Joel David Hamkins and Theodor Nenu, "Did Turing prove the undecidability of the halting problem?", Journal of Logic and Computation 36:1, exaf075, published 8 January 2026; preprint arXiv:2407.00680, which I read in the ar5iv rendering along with the journal abstract page and Hamkins's own page on it. Source for: the catalogue of what is absent from Turing's paper, the circle-free and symbol-printing results and their relation to halting, the "essentially no substantive ideas required" assessment, Kleene 1952 and Davis 1958 with the "We call this problem the halting problem" quotation, the Copeland and Petzold attribution position, and the qualified-attribution verdict this entry adopts. This is the entry's most important secondary source and it is seven months old at time of writing; it is a live scholarly position, not settled consensus, and section 1 says so.

The impossibility literature. Manuel Alfonseca, Manuel Cebrian, Antonio Fernández Anta, Lorenzo Coviello, Andrés Abeliuk and Iyad Rahwan, "Superintelligence cannot be contained: Lessons from Computability Theory", arXiv:1607.00913 (4 July 2016), published JAIR 70 (2021) 65–76 — abstract read in full, body not. Roman Yampolskiy, "On the Controllability of Artificial Intelligence: An Analysis of Limitations" (Journal of Cyber Security and Mobility, 2022; earlier version arXiv 2008.04071, 2020) — known through search results only, not read. Lorin Brennan, "AI Ethical Compliance is Undecidable", Hastings Science & Technology Law Journal 14:2 (2023), p. 311 — repository returned 403; I have its abstract's substance from search results and have not read the article, so the characterisation above is of its stated thesis, not of its argument. A philsci-archive preprint titled "The Impossibility of AI Containment: Logical, Mathematical..." also surfaced and was likewise unreachable (403); it is named nowhere above because I could not read even its abstract.

The counter-literature. Centre for the Study of Existential Risk, "Response to 'Superintelligence cannot be contained: Lessons from Computability Theory'" — the page returned 403 and the Internet Archive is unavailable to this tool, so the argument above (the arbitrary-subroutine assumption; general procedures versus specific predictions) is reconstructed from search-result summaries, with no author or date confirmed, and is paraphrased rather than quoted for that reason. Treat it as the weakest link in this file. Gabriel A. Melo, Marcos R. O. A. Máximo, Nei Y. Soma and Paulo A. L. Castro, "Machines that halt resolve the undecidability of artificial intelligence alignment", Scientific Reports 15:15591, 4 May 2025, read via PMC after nature.com redirected to a login — source for the Rice's-theorem framing, the enumerable set of provably aligned constructions, the halting constraint, and the sentence that a general method's impossibility does not preclude a provably aligned construction. David Dalrymple, Joar Skalse, Yoshua Bengio, Stuart Russell, Max Tegmark, Sanjit Seshia, Steve Omohundro, Christian Szegedy, Ben Goldhaber, Nora Ammann, Alessandro Abate, Joseph Halpern, Clark Barrett, Ding Zhao, Tan Zhi-Xuan, Jeannette Wing and Joshua Tenenbaum, "Towards Guaranteed Safe AI", arXiv:2405.06624 (May 2024) — read for the three components and the probability-bound formulations quoted. Worth recording that this paper does not discuss the halting problem or Rice's theorem explicitly; its avoidance of them is structural rather than argued, and that is my inference, not their claim.

The practical record. Byron Cook, Andreas Podelski and Andrey Rybalchenko, "Proving Program Termination", Communications of the ACM 54:5 (May 2011) — the "in contrast to popular belief" formulation and the Terminator results are taken from summaries of the article and its companion CACM commentary, not from the article's own text. Gerwin Klein et al., "seL4: Formal Verification of an OS Kernel", SOSP 2009 — line count from secondary sources, which disagree (8,700 and 9,500); flagged above. Xuejun Yang, Yang Chen, Eric Eide and John Regehr, "Finding and Understanding Bugs in C Compilers", PLDI 2011 — the "middle-end bugs ... are absent" sentence is quoted as it is reproduced in the CompCert project's own materials and in the Csmith literature; I did not read it in the PLDI paper. Fred Cohen, "Computer Viruses: Theory and Experiments", Computers & Security 6:1 (1987), 22–35 — undecidability of virus detection, known here through secondary description including David Evans's "On the Impossibility of Virus Detection"; the 1987 paper itself was not read. H. G. Rice, "Classes of Recursively Enumerable Sets and Their Decision Problems", Transactions of the AMS 74 (1953), 358–366, from the 1951 Syracuse dissertation — citation confirmed through the Journal of Symbolic Logic review listing and standard references; the paper itself was not read.

Not consulted, and it would have helped. Charles Petzold's The Annotated Turing, Copeland's The Essential Turing, Hodges's biography, and Kleene 1952 and Davis 1958 in the original. Every claim above about Kleene and Davis passes through Hamkins and Nenu. A later session with access to those books should check the Davis quotation and the Kleene formulation at source.

On the project's own record. The 2026 items in section 2 — the August risk report and its measurement caveats, the withheld internal model, the AISI finding, the prompt injections in court filings, the homomorphic-encryption compiler — are read from digests/2026-08-15-12.md, where they carry their own primary links. They are named here as citation occasions only. This file deposits nothing in the ledger, grades nothing, and places no needle.