The words spoken in the Unit 8 video, scene by scene, as its captions show them, with what the animations show marked [On screen: ...] where they play. Each speaker is named where the speaker changes. The Unit 8 reading covers the same material.
The narration is spoken by synthetic voices made for this course, each shown on screen as a drawn robot. No person is speaking.
Unit 8 — Verification lab
Narrator: This is the centre of the course: turning "it looks right" into "here is what I checked, and here is what the check said".
You have a routine. You have no evidence.
In Unit 7 you asked for a routine and you got one. It looked like Python, read like Python, and probably ran. What you did not get was any evidence that it was right. This unit is about producing that evidence — the part that transfers to everything else you will ever generate.
A test oracle
Start with a piece of vocabulary computer scientists have used for decades. A test oracle is a source of correct answers you trust independently of the thing you are testing — not a second opinion, a reference.
[On screen: The frame is split into two panels. The left panel, headed 'internal recursion', shows a single box labelled 'the system' with an arrow that leaves it and curves straight back into the same box. A marker travels round that loop three times, and the loop tightens on each pass while a counter reads pass one, pass two, pass three, each time noting that the source and assumptions are shared. The panel ends with the words 'not independently verified' in red. The right panel, headed 'external check', shows the same box, but here the arrow labelled 'claim' leaves the system altogether and reaches a second box labelled 'independent reference: published values, or independently derived code'. A second arrow labelled 'verdict' returns, and a result appears above the system reading 'verdict: differs at n = 1'. The closing text states that same-source revision may help but is not independent verification, that shared assumptions can persist, and that a separate method or source provides stronger evidence.]
Name the rule the lab rests on: the external-reference principle. A check has to come from a reference the thing being checked does not control. Whether anything can fully certify itself from the inside is for Unit 18; here the working rule is the concrete one.
A certificate
One more term, and it is what the others produce. A certificate is evidence that lets someone else repeat a check and get the same result, without trusting whoever produced it. Your checker report is one: the command, the oracle, the range, and either a pass or the first divergence. Anyone can rerun it in a minute. "I checked it" is not a certificate, and neither is a coding tool's report that its own tests pass: those tests are generated from the same prompt as the code, so they carry the same unstated defaults. Checking a certificate is usually far cheaper than producing the result. Unit 6's identity shows it.
[On screen: A strip shows the claimed values B0 to B6: 1, minus one half, one sixth, 0, minus one thirtieth, 0, one forty-second. Below it, the terms n plus 1 choose j, times B_j, are written out row by row. Row 1: 1 and minus 1. Row 2: 1, minus three halves, one half. Row 3: 1, minus 2, 1, 0. Row 4: 1, minus five halves, five thirds, 0, minus one sixth. Row 5: 1, minus 3, five halves, 0, minus one half, 0. Row 6: 1, minus seven halves, seven halves, 0, minus seven sixths, 0, one sixth. Each row is marked as summing to exactly zero. Nothing is solved and no oracle is consulted: a list that starts at B0 = 1 and passes every row is the sequence.]
Instead of solving each row for the next value, substitute all the claimed values and see whether every row sums to exactly zero. A list that starts at one and passes every row to thirty is the sequence. No solving needed. Software testers call this a metamorphic check. It tests a relation the outputs must satisfy among themselves, so it needs no oracle, and it works on both routes: on a routine's values, or by hand on a pasted table.
Checker: Substituting the oracle's values into every row from one to thirty: every row sums to exactly zero. The oracle is built from this identity, so that shows only that it applies it correctly. The independent evidence is still the published values.
Two relations, one complete
Narrator: The recurrence is one relation. It is unusually strong: from B-zero equals one, it fixes every value, so passing every row establishes the values themselves.
[On screen: A row of first-convention Bernoulli numbers for n = 0 to 8: 1, minus one half, one sixth, 0, minus one thirtieth, 0, one forty-second, 0, minus one thirtieth. The relation B_n plus equals minus one to the power n times B_n minus appears, then a row of multipliers, plus 1 at even n and minus 1 at odd n. A highlight sweeps across the indices and fills a second row, the second convention, one value at a time: 1, one half, one sixth, 0, minus one thirtieth, 0, one forty-second, 0, minus one thirtieth. The odd indices above 1 are marked the same, because 0 times minus 1 is still 0; the even indices are marked the same, because the multiplier is plus 1. Only n = 1 is marked as differing: minus one half becomes plus one half. Only indices 0 to 8 are drawn.]
The convention relation is another. A second-convention value is the first-convention value times minus one to the power n. Every odd value above B-one is zero, so the two tables differ only at n equals one. Output that matches the second convention everywhere is consistent with it; whether that was a choice or a bug, the specification has to say.
Checker: Over indices zero to thirty, the oracle's two tables differ at n equals one and nowhere else.
Narrator: Most relations are necessary, but not enough on their own. A routine that returns zero at every index above one passes the odd-terms property. It is still wrong at every even index. A relation that holds rules out only what would break it.
Why trust this oracle?
Questioner: Why should anyone trust the oracle?
Narrator: An oracle you merely assert is trustworthy is not an oracle; it is a second guess. First, exact arithmetic: a disagreement is always real, never a rounding artefact. Second, independent confirmation: it is checked against twenty-two published values it did not compute. Third, a large index: B-thirty is in that table deliberately, because small indices hide bugs. Fourth, a property: every odd Bernoulli number above B-one is exactly zero. And it states its convention, B-one equals minus one half, at the top of every report.
The oracle checks itself — against outside values
Checker: Run the file and it checks itself before it prints anything. It computes every value from B-zero to B-thirty-one through the recurrence, compares them with all twenty-two published values, and confirms that every odd term from B-three to B-thirty-one is exactly zero. The B-thirty on the screen is the largest of those published values. If that last line said FAIL, nothing else in the lab would mean anything.
Narrator: This is not a counterexample to the external-reference principle: the oracle checks its answers against values it did not compute.
Differential testing
Differential testing means running two implementations of the same specification on the same inputs and comparing the results — your generated routine and the oracle, over every index from zero to thirty. This is a general method, not something specific to Bernoulli numbers.
First divergence
[On screen: Headed 'Comparing index by index', two rows of Bernoulli values, the oracle and your routine, are compared from n=0 to n=6. At n=0 both read 1 and the column is marked same. At n=1 the oracle reads minus one half and your routine reads plus one half; this is the first divergence, and the column is outlined in red and labelled diverges. The scan stops there: the later cells are shown but not marked, and their values agree, including n=4, where both read minus one thirtieth. A red line reads: first divergence at n=1, expected -1/2, got +1/2. Below it: the specification fixes B1 = -1/2, so this routine fails it. Start here, then test the cause of any later mismatch.]
check.py reports the first divergence — the lowest index where the two disagree. The first failing input gives you a reproducible boundary and a place to begin. It can suggest the kind of mistake, but does not prove every later difference has the same cause.
Two different kinds of check
[On screen: A row of indices runs from B0 to B11, then an ellipsis, then B29 and B30. Under it, the table check marks only the rows written down: B0 = 1, B1 = -1/2 and B4 = -1/30, with B4 emphasised. Under that, the property check sweeps across every odd index above 1 -- B3, B5, B7, B9, B11, the ellipsis and B29 -- marking each with '0?'. Captions read: a list of facts that covers the rows you wrote, and a statement about a whole class of inputs. Then every row the table did not write, B3 among them, is marked with a question mark: never looked at. The float routine's output arrives: B3 = -1.1102230246251565e-16. On a number line, not to scale, it sits on 0. The property check's mark at B3 turns to a red cross with the words: not exactly 0, property check fails; the marks at B5 and B7, the other non-zero odd terms the checker lists, turn to crosses too, and the later marks dim. A band is drawn around 0 for an absolute tolerance, with no value given; the point lies inside it, and the words read: absolute tolerance, called zero, pass.]
Alongside the value-by-value comparison there is a second kind of check. A table check asks: does index four give minus one over thirty? A property check asks: for every odd index above one in the range, is the result exactly zero? One is a list of facts; the other is a statement about a whole class of inputs.
Why the property check earns its place
[On screen: A row of indices runs from B0 to B11, then an ellipsis, then B29 and B30. Under it, the table check marks only the rows written down: B0 = 1, B1 = -1/2 and B4 = -1/30, with B4 emphasised. Under that, the property check sweeps across every odd index above 1 -- B3, B5, B7, B9, B11, the ellipsis and B29 -- marking each with '0?'. Captions read: a list of facts that covers the rows you wrote, and a statement about a whole class of inputs. Then every row the table did not write, B3 among them, is marked with a question mark: never looked at. The float routine's output arrives: B3 = -1.1102230246251565e-16. On a number line, not to scale, it sits on 0. The property check's mark at B3 turns to a red cross with the words: not exactly 0, property check fails; the marks at B5 and B7, the other non-zero odd terms the checker lists, turn to crosses too, and the later marks dim. A band is drawn around 0 for an absolute tolerance, with no value given; the point lies inside it, and the words read: absolute tolerance, called zero, pass.]
A table only covers its own rows. An implementation can match every value you wrote down and still be wrong everywhere else.
Checker: Run on the float example, B-three comes back as a tiny number, not zero: minus one point one times ten to the minus sixteen. The property check demands exact zero, and fails.
Narrator: A comparison with an absolute tolerance would have called that zero.
The named failure modes
check.py does not stop at "wrong". It names the failure mode, using a fixed set of codes. Naming a fault is what turns a failed test into a diagnosis. Five of these you met in Unit 7: b1-sign, odd-terms, ada-indexing, off-by-one and not-fraction. Three are for code that fails or does not run: raises, import-error and no-function. One is new: one-observation. It appears when ada-indexing and off-by-one both match. Note G's numbering and a one-place shift give the same values at every index except B-zero, so one value is all that tells them apart. To settle which it is, you read the source.
A real diagnosis
Questioner: What does it say about a routine that is nearly right?
Checker: Run it against the supplied wrong-B1-sign example and you get b1-sign: the routine is correct under the second Bernoulli convention, B-one equals plus one half.
Narrator: Nothing about it is mathematically wrong; it is wrong for this specification, and that distinction is the whole lesson.
Five examples, five diagnoses
Checker: The wrong B-one sign example is the report you just saw: first divergence at one, and b1-sign. The other examples, run the same way. The Note G example and the off-by-one example get the same four codes: odd-terms, ada-indexing, off-by-one and one-observation. B-zero tells them apart. In the off-by-one example it is minus one half, which points at the shift. The float example gives not-fraction and odd-terms. Its first divergence is at two, not zero. A float can store one and minus a half exactly, so B-zero and B-one match. One sixth is the first value a float cannot store exactly. The correct example passes.
Narrator: The off-by-one example is clean code with every value shifted a place; comparison finds it at once. The correct example uses a different algorithm from the oracle: stronger than a routine agreeing with a copy of itself.
Checker: And one more wrong example, wrong-B-four-sign. The first divergence is at four, where it gives plus one thirtieth, and there is no named code. One wrong value is located, not named: the codes describe faults that recur, not every fault there can be.
Safety — read before you run
Questioner: Is it safe to run code I have not read?
Narrator: Stop before you run anything. The checker executes the file you hand it. That is the only way to find out what a routine returns. It runs the file apart from itself, stops it if it runs too long, limits what it can use, and does not pass on your settings, such as stored keys. So if something goes wrong, you get a report instead of a frozen screen. That means less damage. It does not mean safety: the code still runs as you, and can read your files. Read it first. That holds for code a person wrote, too, not only for code a model produced. And code you cannot read at all, such as closed-source software, you run on trust or in isolation. So being able to read the source is one reason open source helps checking. For anything you have not read, use a container or a virtual machine, or take the table route, which executes nothing.
Table-based verification — an equal route
Questioner: And if I would rather not run any code at all?
Narrator: There is a second route that runs no code at all, and it is not a lesser one. Ask for the values rather than the program, put them beside the printed reference table, and stop at the first row that differs. You have found the first divergence by hand, using the same method the tool uses. Include B-thirty, as an exact fraction, because small indices hide bugs.
Checks without a reference table
A pasted table can be tested before you compare it with anything. Three facts about the sequence do it. Signs: from B-two on, the even-indexed values alternate, positive, negative, positive.
[On screen: A rule appears: for even n of 2 or more, the denominator of B_n is the product of the primes p for which p - 1 divides n (von Staudt-Clausen theorem [M4]). At the right, the table's value B12 = -691/2730. Below the rule, the divisors of 12 appear in a row: 1, 2, 3, 4, 6, 12. Each has 1 added, giving 2, 3, 4, 5, 7, 13. These are marked in turn: 2, 3 prime; 4 struck out, not prime; 5, 7 and 13 prime. The primes are multiplied: 2 times 3 times 5 times 7 times 13 equals 2730. The 2730 moves under the table's denominator, which is also 2730, and is marked as matching. A closing line says the check is necessary, not sufficient: a wrong numerator over the right denominator passes.]
Denominators: for an even index of two or more, the denominator is the product of the primes p for which p minus one divides the index. For B-twelve, add one to each divisor of twelve. Two and three are prime. Four is not: it is two times two, and only primes count, so it is crossed out. Five, seven and thirteen are prime, and their product is two thousand seven hundred and thirty, the denominator in the table. Size: for large indices, a formula predicts the magnitude. For B-thirty it gives about six hundred and two million, and so does the exact value: the two agree in their first nine digits. Each is necessary, but none is enough on its own. A wrong numerator over the right denominator passes the denominator check.
What each route misses
Each route has blind spots. By hand, you cannot tell whether the code actually produces the table it printed, and you only cover the rows you compared. Automated, you check agreement with the oracle's convention rather than that it is the one you wanted, and it says nothing about comments or historical claims. Neither route is complete. Both are real verification.
Your turn
Take what you saved in Unit 7. Read it, then check it by whichever route you are working in. Record the first divergence and the diagnosis, repair either the code or the prompt, and run the check again. Then finish with the three checkpoints for your route, in a terminal, or in the browser on the table route — both routes are equal.
Passing is not the end
Questioner: So a pass means the routine is right?
Narrator: Passing the checker is not the end of the job. It tells you your routine agrees with the oracle for thirty-one indices. It does not tell you why — and being able to say why is what Unit 17 will ask for. None of this was invented for AI. Oracles and differential testing are how human code has always been checked, because human code has always had bugs. What AI changes is how fast plausible code arrives. The check slows you down again, and that is the responsible part.
From a check to an evaluation
This unit gets a decidable answer because an exact oracle exists. Much of the work you will do has no oracle, and then the question changes shape: how often does this go wrong, is this version better than that one? One comparison does not settle those. They need a sample, a measure and a protocol. That is an evaluation, and it rests on the same principle as your check: the measure has to come from somewhere the thing being evaluated does not control. Six moves, in this order. State the question so that an answer could disappoint you. Choose the measure before you see any output. Pilot small: a small trial shows whether your method works, and then you discard its data. Freeze: write down the question, the measure, the sample, the threshold and what counts as failure, and date it. Run it without adjusting. Score and report, including the uncertainty.
Closing, 20 seconds, no speech. A candidate record on the left, a check against an independent reference in the middle, and a bracketed claim on the right fade in side by side. Below them: Continue with the course material, ai.qyber.dev/edu-ai-literacy-ada-verification/, Course playlist: youtube.com/playlist?list=PLPsBWTfgvakM, All links are also in the description, and Keep your record. Check the next claim.