What verification does not give you

The argument here, trusting arithmetic instead of people, has limits.

It does not verify the operating system. The manifest covers the application. The card's operating system is Debian, built with mmdebstrap; if the image you flashed was backdoored, the root hash it displays is whatever the backdoor wants. Half the usual answer exists: make image builds a card from this repository, and CI builds the system partition and checks the unit hardening assertions (INV-PROV-18, INV-PROV-19) against it. The other half does not: no image is published or signed, and Raspberry Pi bring-up is the next milestone. Until both are done, this is the largest gap in what this document promises. Verification defends the application and cannot bootstrap trust in what runs it.

It does not verify the hardware. We check the software supply chain. We cannot check that your Pi is a real Pi.

It does not prove the specs are the right specs. make verify proves the code does what the specifications say. Whether they describe a secure design is for human review, which the readable spec format exists to allow.

It does not prove the dependencies are correct. Cross-checking against an independent implementation catches disagreement, not both being wrong the same way.

It does not prove the absence of bugs. It proves the absence of one class of drift: code that no longer matches its documented behaviour, and builds that no longer match their sources.

---