Unit 8: Verification lab

Reading time: about 26 minutes. Activity: about 27 minutes.

1. What this unit is for

In Unit 7 you asked for a routine that computes Bernoulli numbers, and you got one. It looked like Python. It read like Python. It probably ran without complaint. None of that is a result.

This unit turns "it looks right" into "here is what I checked, and here is what the check said". That move — from impression to evidence — is the single most transferable thing in the course, and it applies far beyond Bernoulli numbers.

2. Five ideas, named

Two of the first four are standard terms in software engineering: test oracle and differential testing. The other two are this course's names for standard ideas: property-based checking is a simple form of what testers call property-based testing (Unit 7), and the first divergence is what they call the first failing input. The fifth comes from mathematics and computer science, and it is what the other four produce. They are worth learning by name, because once you have the names you can ask for the thing.

Test oracle. A source of correct answers that you trust independently of the thing you are testing. A second opinion from the same source is not an oracle. In this lab the oracle is ../lab/reference_bernoulli.py.

Differential testing. Running two implementations of the same specification on the same inputs and comparing the outputs. Here the two implementations are your generated routine and the oracle.

Property-based checking. Instead of asserting individual values, you assert a statement that must hold across a whole class of inputs — for example, every odd Bernoulli number above B1 is exactly zero.

First divergence. The lowest input at which two implementations disagree. It gives a precise starting point for debugging; it does not establish the cause of later disagreements.

Certificate. Evidence that lets someone else repeat a check and get the same result, without trusting whoever produced it: test results against an independent reference, values that can be substituted back into their defining identity, a quotation with its locator. Checking a certificate is usually far cheaper than producing the result. Your checker report -- the command, the oracle and where its values were confirmed, and either PASS over 0 to 30 or the first divergence -- is a certificate. "I checked it" is not.

3. Why this oracle deserves to be trusted

An oracle that you simply declare trustworthy is not an oracle; it is a second guess with better branding. Here is the actual case for this one, and you can verify every part of it in about a minute.

It uses exact rational arithmetic. Every value is a fractions.Fraction. Bernoulli numbers have large numerators and denominators — B12 is -691/2730, B30 is 8615841276005/14322 — and binary floating point cannot represent them. The oracle never rounds, so any disagreement it reports is a genuine disagreement, never a rounding artefact. This is also why the checker compares values exactly rather than "to within a small tolerance".

It is checked against values it did not compute. The oracle carries a table of values transcribed from published Bernoulli-number tables. Before it prints anything, it computes every value from B0 to B31 through the recurrence, compares them with every one of those published values, and confirms that every odd term from B3 to B31 is exactly zero -- computed, rather than taking the zero for granted. (check.py then compares a candidate with the oracle from B0 to B30.) Run it (code route; the table route below uses the same values by hand):

cd course/lab
python3 reference_bernoulli.py

The last line of a healthy run reads:

OK: oracle agrees with all 22 published values, odd terms are zero.

Twenty-two values transcribed from published tables, including odd entries that are zero. The table they came from is recorded at References and source policy [M2]: the NIST Digital Library of Mathematical Functions, §24.2, Tables 24.2.1 and 24.2.3, checked value by value on 2026-07-24, all twenty-two agreeing and no correction needed. If any entry disagreed, the program would print FAIL and exit with an error status, and nothing else in the lab would mean anything until that was resolved.

It is checked at a large index. B30 = 8615841276005/14322 (about 602 million: 601,580,873.9 to one decimal place) is in that table deliberately. Small indices hide bugs: a routine with a subtle ordering mistake in the recurrence can agree perfectly with the published values from B0 to B12 and still be wrong. If you only ever check small cases, you only ever catch large mistakes.

Float routines are different: their errors are tiny but real. The supplied float routine is wrong from B2 on, though only after about the fourteenth digit. Because the values grow, the size of the error grows too, to about 0.0000012 (1.2e-6) at B30. So a test that allows an error of up to 0.000000001 (1e-9) first fails only at B24. Only an exact comparison catches it at B2.

It states its convention out loud. The oracle prints first Bernoulli numbers (B_n^-), B1 = -1/2 at the top of every report. B_n^- is the usual name for the first convention's values, and B_n^+ for the second's. A reference that does not say which convention it uses cannot settle a disagreement about conventions.

A second implementation using a different algorithm agrees with it. The file ../lab/examples/correct_example.py computes the same values by the Akiyama–Tanigawa transform, which is a different algorithm from the oracle's binomial recurrence. Agreement between separately implemented algorithms is stronger evidence than one routine agreeing with a copy of itself, although both implementations still belong to this course and require human review.

4. The property check, and what it catches that a table cannot

Every odd Bernoulli number above B1 is exactly zero. That is a mathematical fact about the whole sequence, and the lab checks it as a property, not as a list of entries.

The difference is not cosmetic.

• A table check asks: does index 4 return -1/30? It is a list of facts, and it covers exactly the rows you wrote down.
• A property check asks: is it true, for every odd index above 1 in this range, that the result is exactly zero? It covers indices you never thought about.

An implementation can match every value in your table and be wrong everywhere else — for instance, one that returns correct values for the indices it was shown and something arbitrary elsewhere.

There is a sharper case. Here is real output from the supplied float-based example:

[odd-terms] Odd-index Bernoulli numbers above B1 must be exactly zero.
    Non-zero odd terms found: B3=-1.1102230246251565e-16,
    B5=-6.938893903907228e-17, B7=-6.938893903907228e-17.

Those numbers are, to any human eye, zero. A comparison with an absolute tolerance -- abs(x) < 1e-9, numpy.isclose, pytest.approx, assertAlmostEqual -- accepts them as zero. Python's math.isclose with its defaults does not, because its tolerance is relative, and nothing is relatively close to zero; that is one more reason a tolerance is a decision, not a default. The checker compares each float as the exact rational it stores, so the property check demands exact zero and fails. Tolerances are precisely where inexact arithmetic hides, and a property stated exactly gives it nowhere to hide.

5. Running the checker

This section is the code route; the table route below does the same comparison by hand. The tool is ../lab/check.py. It runs the file you give it in a separate process (see the safety section below), calls its bernoulli function for every index from 0 to 30, compares each result exactly against the oracle, reports the first divergence, and names the failure mode.

cd course/lab
python3 check.py examples/wrong_b1_sign.py

It exits with status 0 on a pass and 1 on a failure, so it can be used in a script. Useful options:

python3 check.py --help
python3 check.py examples/float_output.py --max-n 12 --verbose

Do not invent other flags; those are the ones that exist.

6. Reading the diagnoses

The checker does not stop at "wrong". It names the failure mode, using this fixed set of codes:

A report also carries a [divergence] line, which states the first index where your routine and the oracle disagree. That line locates the fault; the named code identifies what kind of fault it is.

check.py can also report that the comparison did not happen: timeout (the routine never returned, or was stopped at a resource limit), no-result (it ended abruptly without a result), not-callable and no-file.

Five wrong implementations are supplied so you can see each diagnosis before you meet it in your own work. Four show named failure modes; the fifth has a single wrong value that no named mode describes.

examples/wrong_b1_sign.py -> b1-sign. First divergence at n=1: expected -1/2, got 1/2. Nothing in this file is mathematically wrong; it is correct under the second Bernoulli convention. It is wrong for this specification. As the checker puts it, this is a specification failure rather than an arithmetic failure, which is the sentence Unit 10 is built on.

examples/ada_indexing.py -> odd-terms, ada-indexing, off-by-one and one-observation. First divergence at n=1: expected -1/2, got 1/6. This routine uses Lovelace's Note G labels — only the non-zero terms are numbered, and they take the odd integers, so her B1, B3, B5, B7 are the modern B2, B4, B6, B8, and her labels include no B2. Against the modern convention that is inverted: the odd indices carry the numbers and the even ones are empty. Every value it returns is a genuine Bernoulli number; every one is filed under another century's label.

The last two diagnoses are the interesting ones. A plain off-by-one shift produces identical output at every index except B0, because her B_n at odd n is the modern B_(n+1) and both schemes give zero at the even indices from 2 up. So the checker reports both readings, ada-indexing and off-by-one, and one-observation names B0 as the whole of the evidence separating them -- 1 here, where a shift would have put -1/2. One value is thin evidence, and settling it means reading the source. A comparison tells you where to look; it does not always tell you what you are looking at.

examples/float_output.py -> not-fraction and odd-terms. The type fault is reported at n=0. The checker compares each float as the exact rational it stores, so 1.0 and -0.5 match B0 and B1, and the first value divergence appears at n=2, where the exact 1/6 arrives instead as the float 0.16666666666666674.

examples/off_by_one_range.py -> off-by-one, odd-terms, ada-indexing and one-observation. First divergence at n=0: expected 1, got -1/2. Here B0 = -1/2 is the evidence for the shift reading. The code is clean, the arithmetic is exact, and every value is a real Bernoulli number shifted one place. The shift is in the source to be read -- bernoulli returns _b(n + 1) -- but nothing around it looks wrong, so a reader checking the arithmetic can pass over it. Comparison against a reference finds it at once.

examples/wrong_b4_sign.py -> no named code. First divergence at n=4: expected -1/30, got 1/30. One sign slip in a hand-typed table of small values; every other index is right. The report carries the [divergence] line and nothing else, because no named mode describes one wrong value. The codes are a vocabulary for faults that recur, not a list of every fault there can be; the first divergence still tells you exactly where to look.

examples/correct_example.py -> PASS.

7. Safety: the checker executes what you give it

Stop before you run anything. (Code route; the table route executes nothing, but the rules below hold for any generated code you run elsewhere.)

check.py executes the file you hand it. That is the only way it can test the code. It does not run the file inside itself. The file runs as a separate program, with a time limit and resource limits, without your environment variables (settings that can include stored keys), and only data comes back.

That limits the damage; it does not make the code safe. The file still runs as you, and can read what you can read. It buys you two things: an accident becomes a report rather than a frozen terminal, and keys stored in your settings are not handed to code you did not write.

AI-generated code is code from an untrusted source. "Untrusted" is a statement about what you know, not an accusation about anyone's intent. You did not write it, you have not read it, and polished formatting does not establish what the code does.

So, before you run generated code — here or anywhere:

• Read it. All of it, including anything above and below the function you asked for.
• Look for file writes and deletions, network access, subprocess, os.system, eval, exec, decoded or obfuscated strings, and anything that installs packages.
• Check the imports. A Bernoulli routine needs fractions and possibly math. It does not need os, socket, requests or shutil.
• For anything you have not read, or that came from a source you have no reason to trust — a container, a virtual machine, or a throwaway account. The table route below completes this unit without executing anything.
• Do not run it as an administrator.

If you would not paste an unknown script from an internet forum straight into your terminal, apply the same rule here. The fact that you asked for it does not change where it came from.

None of this is special to AI. The same rules apply to code a person wrote, a classmate's or a stranger's. Closed-source software, whose source you cannot read at all, can only be run on trust or in isolation; being able to read the source is one reason open source makes this kind of checking possible.

Treat this as part of the lesson rather than a warning notice. A verification tool that has to execute untrusted input is a real engineering trade-off, and you have just met one.

8. Table-based verification

There is a second complete route through this lab that runs no code at all. It is the same method, performed by hand, and it is not a lesser route.

1. Get the reference values. Either run python3 reference_bernoulli.py, or use the table below, which is the same data.
2. Ask the AI system for the values rather than the program: "list B0 to B12 as exact fractions, and give B30".
3. Write the two columns side by side, in index order.
4. Go down the rows in order and stop at the first row that differs. You have just found the first divergence by hand, using the tool's own method.
5. Check B30 even if the small values matched.

All odd B_n for n > 1 are exactly zero.

What the table route catches: wrong signs (B1 = +1/2 instead of -1/2); missing or non-zero odd terms; values shifted by an index; decimals such as -0.0333... offered where an exact fraction was required; and an error at B30, provided you include it.

Checks that need no reference table. Three facts about the sequence let you test a pasted table before you compare it with anything:

• Signs. From B2 on, the even-indexed values alternate in sign: B2 positive, B4 negative, B6 positive, and so on [M5, eq. 24.2.2].
• Denominators. 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 (the von Staudt-Clausen theorem [M4, eq. 24.10.1]). For B12, adding 1 to each divisor of 12 (1, 2, 3, 4, 6, 12) gives 2, 3, 4, 5, 7 and 13. Only primes count, and 4 = 2*2 is not one, so it drops out; the primes 2, 3, 5, 7 and 13 multiply to 2*3*5*7*13 = 2730, the denominator in the table.
• Size. For large even n, |B_n| is asymptotic to 2 * n! / (2*pi)^n (their ratio tends to 1) [M5, eq. 24.11.1]. For B30 that gives about 602 million (601,580,873.3), and the exact value is about 602 million too (601,580,873.9): the two agree in their first nine digits.

A wrong sign, a prime in a denominator that does not belong there, or a B30 out by orders of magnitude fails one of these at once. Each is necessary, but none is enough on its own: a wrong numerator over the right denominator passes the denominator check.

What it misses: whether the program actually produces the table it printed — a table in a chat window may be generated text rather than program output, and those are different claims; what happens at indices you did not compare; and it does not re-run itself when you change something.

What the automated route misses: it checks agreement with the oracle's stated convention, not whether that convention is the one your task requires; it says nothing about comments, historical claims, licensing or readability; and it cannot on its own tell you whether you understand the code.

Neither route is complete. Both are real verification. If you have Python available, doing the table comparison for B0 to B12 and running the checker takes about five minutes together and covers more than either alone.

9. Where this leaves you

When the checker passes, you have established one thing precisely: your routine agrees with a verified oracle for every index from 0 to 30, returns exact fractions, and satisfies the zero-odd-terms property.

That is evidence. It is not an explanation. Unit 17 will ask you to write two sentences saying why your answer is correct, citing what you checked rather than what produced it.

What you hand on is the certificate, not a declaration. "AI was used" or "I verified it" gives a reader nothing to check. The command, the oracle's provenance and the output let them rerun your check in a minute.

There is also a check that needs no oracle at all, and it shows why checking is cheaper than producing. Unit 6's identity, sum_{j=0}^{n} C(n+1, j) * B_j = 0, can be used the other way round: instead of solving each row for B_n, substitute all the claimed values and see whether every row sums to exactly zero. No solving, any row, in any order. And because each row fixes its B_n uniquely once the earlier values are known, a list that starts at B0 = 1 and passes every row from n = 1 to n = 30 is the sequence up to B30. It is the same identity that settles the convention: the n = 1 row reads 1 + 2*B1 = 0, which forces B1 = -1/2. Applying this check to the oracle itself only confirms that it applies the identity correctly: the oracle is built from that identity, so the independent evidence for it is still the published values.

A check of this kind has a name in software testing: metamorphic testing [E13, sec. 3.3], [E20, sec. 2.2]. Instead of comparing each output with a known answer, it checks a relation that the outputs must satisfy among themselves, so it needs no oracle. It works on both routes: a routine's values, or a table pasted from a chat window, can be substituted into the identity, the table by hand for the first few rows.

A second relation links the two conventions: B_n^+ = (-1)^n B_n^-. In words, each second-convention value is the first-convention value multiplied by (-1)^n, which is +1 when n is even and -1 when n is odd. Every odd B_n above B1 is zero, so the two tables differ only at n = 1; the oracle's values confirm it over 0 to 30. Output that matches (-1)^n B_n^- over the tested indices is consistent with the other convention (b1-sign); whether that is the choice someone made or a bug that lands on the same value, the specification or the source has to say. wrong_b4_sign.py, which differs at n = 4, matches neither convention.

Most relations are necessary, but not enough on their own. A routine that returns zero at every index above 1 satisfies the odd-terms property and is still wrong at every even index: a relation that holds rules out only what would break it. The recurrence is the rare complete one: from B0 = 1 it fixes every value, which is why passing every row establishes the values themselves.

10. The external-reference principle

Behind everything this lab does is a single rule worth naming.

The external-reference principle. A check has to come from a reference the thing being checked does not control. Here that is the oracle: exact, sitting outside the submitted routine, and confirmed against values it did not compute. Asking the same source again is not a check — it is the same source again. (Whether no system can ever fully certify itself from the inside is the larger question Unit 18 takes up; the working rule you need here is the concrete one above.)

This is not a new lesson; it is the name for what you have just done. The oracle earns its place precisely because it sits outside the submitted routine, states its convention out loud, and is checked against values it did not compute. Asking the same source again can help you revise an answer, but it does not give you the independence that a separate method or reference does.

The now-common version of asking the same source again is a coding tool that writes the routine, writes its own tests, runs them and reports "all tests pass". The report is the producer's claim, and the tests are generated from the same prompt as the code, so they carry the same unstated defaults: a generated test that asserts B1 = +1/2 passes the b1-sign routine. Rerunning those tests shows that they pass, not that they test the right thing. The independent reference is still yours to supply.

None of this was invented for AI. Oracles, differential testing and independent re-implementation are how human code has always been checked, because human code has always had bugs, and Note G went to press with errors made by people. What AI changes is how fast plausible code arrives. The check slows you down again, and that is the responsible part.

This is how real work stays honest, not a classroom simplification. In research and engineering the same rule is enforced by machinery.

Take BabaYaga, a reasoning-systems project we are building. It is not released, so you cannot check what follows — notice that, and treat the claim accordingly. In it, no number is typed into the prose of a paper. A build step reads each one out of the files the code produced, and if a quoted value and its source no longer agree it refuses to build, printing undefined rather than a stale figure.

Trusting a computation goes further. Results are recomputed into a separate tree and compared field by field against a reference kept read-only, so a reproduction can never quietly become its own authority.

The strongest form of the differential testing you just did — which other work of ours uses in earnest — is to implement the same method twice, in two different languages, and compare the answers row by row. The first row that disagrees is the first divergence, exactly as here.

None of this is special to Bernoulli numbers. It is the ordinary discipline of never letting the thing being checked certify itself.

That discipline is also the honest reason to trust this course. The course was made with AI assistance, the lab's oracle and checker included, and the oracle is not trusted on that account: every run checks it against published values it did not compute, as you saw above. The figures quoted in these pages are compared against the lab's own output by the build that assembles them. If you would rather see the habit in a full, public codebase than take our word for it, look at the Lucifuge scheduler, published at https://dev.astarte.org/tdl/Lucifuge (the code is on its test branch; checked 2026-10-24). Its test suite parses every example configuration and job specification it ships (tests/examples_validate.rs), so a published example cannot silently stop working. And unlike the BabaYaga claim above, this one you can go and check. You are not rehearsing a toy version of a professional habit; you are using the habit the material itself was made with.

A more general question sits behind this: can anything fully check itself from the inside? It is much older than language models, and this lab does not answer it. It is a way of looking at the lab, not something the lab proves. The closing unit develops it through the published work on second-order reasoning set out in Second-Order Reasoning: The Lens Behind The Course, which the closing Unit 18 teaches from; nothing in this unit, its activity, or its checkpoints depends on either.

11. 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. Not is this answer right but how often does this go wrong, is this version better than that one, what kinds of error does it make. One comparison does not settle any of those. They need a sample, a measure, and a protocol.

That is an evaluation, and it rests on the same principle as the check you have just run: the measure has to come from somewhere the thing being evaluated does not control. Scale is where that gets hard to honour, because at scale it is tempting to let the system under test supply the examples, the metric or the judgement.

Six moves, in this order, and the order is the part that matters.

1. State the question so that an answer could disappoint you. "Does it summarise well?" cannot disappoint anyone. "Do at least 90% of these 50 summaries avoid stating a finding the paper does not contain?" can.
2. Choose the measure before you see any output. A measure chosen after looking is a measure chosen to give the result you already saw.
3. Pilot small. Five to ten items. The pilot is for finding out that your instrument is broken, not for finding out the answer — then discard its data, because it was collected under a design you have since changed.
4. Freeze. Write down the question, the measure, the sample, the threshold and what counts as failure. Date it. This costs ten minutes and is the only thing that makes it impossible to move the goalposts later without leaving a record — including impossible for you, honestly, without noticing.
5. Run it without adjusting. Changing something mid-run starts a new evaluation; say so, and report both.
6. Score and report, including the uncertainty and the result you would have accepted as the opposite finding.

The failure you should expect is at step 2, and this course has an example of its own. One generated clip had to show exactly five illuminated regions, one per diagnostic code. The first measures used were motion and mean brightness, because those were easy to compute; they preferred a clip with sixteen regions over one with five. The measure was not inaccurate — it measured motion and brightness correctly — it simply did not measure the brief. Counting the regions settled it in a line. It was caught only because the brief had been written down first, which is step 4 doing its job for step 2.

Evaluating, when one check is not enough carries the rest: which approach suits which question, the standard software tests for cases that do have a decidable answer, quantitative and qualitative protocols for cases that do not, and the failure modes worth recognising before you meet them.

Checkpoints

Complete this unit at cp08-diagnose and cp08-what-it-shows plus the checkpoint for your route. cp08-diagnose and cp08-what-it-shows run by either route. The browser/table route uses cp08-table-evidence to assess conclusions from manual comparison. cp08-bernoulli needs Python and check.py and establishes executable behaviour over the checker's stated range. Neither route claims evidence it did not collect.

python3 selfcheck.py run cp08-diagnose  # or in the browser
python3 selfcheck.py run cp08-what-it-shows  # or in the browser
python3 selfcheck.py run cp08-bernoulli          # Python route only
python3 selfcheck.py run cp08-table-evidence  # table route