twenty-four embedded projects that prove without revealing
A zero-knowledge proof is a way for one computer to convince another that a statement about its own private data is true, while handing over nothing except the statement and a short proof. Model checking is a way of settling whether a piece of control logic always obeys a stated rule, over every run it could ever have rather than over the runs somebody thought to test. One paper, Berrang, Giacobbe, Swales and Yang, Zero-Knowledge Model Checking, arXiv:2605.00487v2, puts the two together so that a device can establish that its hidden control logic obeys a public rule. This volume takes that paper apart into the primitives it is built from and asks what each one costs on hardware this small.
Two words recur on every page. The prover is the side that holds something private and wants to be believed; here it is almost always a board with a sensor on it. The verifier is the side that will not take the prover's word for it and checks a proof instead; here it is almost always a Raspberry Pi on the same desk.
Twenty-four projects, each on hardware that is already on one bench: three Raspberry Pis, a
NanoPi, a NUCLEO-H7A3ZI-Q, an ESP32, an ESP8266, three cellular HATs, a CAN and RS485 HAT, a
DAQ HAT, two ST sensor shields, an STWIN.box, a time-of-flight sensor, a display and four
LEDs. Nothing here needs to be bought, and nothing here has yet been run on any of it: every
number in the volume is a prediction and says so. For a reader with no background in any of
this, BROCHURE.md says what the work is in plain words first.
24 chapters, 99 figures, 156 numbered statements, 67 proofs. The statements are the theorems, lemmas, corollaries, propositions, definitions, examples and remarks, counted across the chapter sources on Friday 6 November 2026; the figures are four per chapter plus three in the companion. Those four numbers measure how much has been written down, not how much has been run: see What is not claimed. Each chapter stands on its own: it names a secret, a public statement and the relation between them as a set, proves the property of the primitive it uses with every step written, gives the protocol, shows the code, and prices it on the board with an instrument that is named.
Read it. The whole volume is in chapters/ as Markdown with its figures
beside it. Start with
About this volume, or take a chapter from the table
below.
Or start further back. docs/ is the companion. It assumes school algebra and
that you have seen a computer program, and nothing of cryptography, formal methods or
embedded hardware: the prerequisites, with a self-check and two
short routes for whoever misses it, the foundations from a state
machine to a proof, a tutorial that works one proof end to end by hand,
and a guide to all twenty-four projects.
There is deliberately no assembled volume to download. The PDF and the single-file HTML are the author's proofreading editions and stay on the authoring machine; what this repository offers is one chapter at a time.
Contents Read it · The through-line · The twenty-four chapters · The companion · What is not claimed · Checks · Layout · Requirements · Licence
One question runs through the volume and is instanced at the head of every chapter:
What can a verifier learn from a device without the device revealing itself, and what does it cost on this board?
A state transition system is secret. A temporal specification is public. The owner wants to convince a verifier that the system satisfies the specification without revealing the system. The paper's answer has three parts: a public certificate that is checkable in polynomial time, a commitment that hides the system and binds the prover to it, and a zero-knowledge proof that the committed system satisfies the certificate's conditions. Two schemes realise it, an explicit-state one built on polynomial commitments and a symbolic one built on Farkas witnesses and folding, and the chapters take them apart one primitive at a time.
CONTENTS.md is the generated version of this table, and
PITFALLS.md indexes all 152 pitfalls across the chapters.
Four chapters are worth reading as a set. Chapter 1 is the price list and every later cost claim is a count of operations multiplied by one of its numbers. Chapters 3, 4 and 18 are the explicit-state pipeline, from encoding through verification to carrying a 192-byte proof over a CAN bus. Chapters 5, 6, 9 and 16 are the symbolic one. Chapters 4, 13 and 21 prove one statement three ways, as a tailored protocol, as a domain-specific circuit and as a program inside a zero-knowledge virtual machine, which is the one comparison here worth having.
docs/prerequisites.md says what a reader must know and must have,
with a self-check. docs/foundations.md runs once from a state
machine to a proof. docs/tutorial.md works one proof end to end on a
four-state machine, computes its three violation sets by hand, and then introduces a
deliberate error so that the verifier can be seen refusing it.
docs/guide.md gives one page per chapter: what it assumes, the one idea,
what to read first, the trap, and its acceptance test.
Nothing here has been run on this bench. Every timing and every agreement rate reads "not measured" and names the instrument that would fill it and the reason it is empty. The only measured timings in the volume are the source paper's own, and they are attributed to the paper's machine, a 32-core AWS instance, never to a board here. A number this volume derives says "computed" and shows its arithmetic.
No chapter claims a scheme is secure beyond what its cited paper proves. Where a theorem is stated it is either the paper's with its number, a textbook result with its citation, or a short lemma proved in full on the page. No chapter claims that a language model contributes soundness: a model appears in four chapters, it proposes and never decides, and each of those chapters carries the theorem saying a wrong proposal cannot cost soundness. Where a chapter uses a trusted setup it says so and marks the ceremony as something this bench cannot run.
Lean 4 appears wherever the volume states something a machine could check rather than something a board could measure. Two different things carry that name here, and a reader who runs them together will think one of them is lying.
The development at lean/ builds. It is 561 lines, it carries no sorry in any
proof, it depends on no Mathlib, and it is pinned to leanprover/lean4:v4.35.0. A workflow runs
lake build on it on every push that touches it, and that build passes, so a kernel has
accepted every declaration in it. That is a verdict about elaboration and not about meaning.
The theorems still have to state what they should, which is settled by reading: a review of this
development found one that compiled and proved nothing, because it assumed its own conclusion.
lean/STATUS.md records that, names the run, and says plainly which parts of
the paper's Theorem 3.2 are formalised and which are not.
The listing printed inside chapter 14 is a different development, and it has not been
checked. It declares one gap with a sorry, it builds against Mathlib, and no kernel has read
it. The chapter says so in its own key facts. Where the two differ, lean/STATUS.md is the file
that explains which is which.
| Where | What Lean carries there |
|---|---|
| Project 14 | The whole chapter. The paper's Theorem 3.2, the fair-termination rule, written as four structures, a descent lemma and the rule itself. This is the only chapter whose language is Lean. |
| Project 13 | Named among the languages not chosen, as the route that would prove the program implies the obligation rather than proving one instance of it. |
| Project 16 | Cites Project 14 for the rule the certifier relies on, and names a checked proof of the certifier's own soundness as the step after this one. |
| Project 17 | Cites Project 14 for the machine-readable statement of the conclusion its automaton feeds. |
| Foundations | Explains that the volume carries the fair-termination proof twice, once as prose and once for a proof assistant, and why the second form has to name its induction. |
| Prerequisites | Lists Lean 4 among the tools, with what a reader needs to know before Project 14. |
| Tutorial | Names the kernel verdict as the thing Project 14 is to reproduce. |
| Guide | The one-page summary of Project 14. |
What would change this section. A Lean development for the volume exists outside this repository, in the author's working tree. It closes the step Project 14 leaves open and formalises two counterexamples found in review, so that a relation failing to imply its conclusion becomes a fact a kernel confirms rather than a claim a reader is asked to accept. It is published here only if and when it compiles, and this section is rewritten in the past tense on the same day and not before.
The workflow reads the published tree, which is all a clone contains: the authoring sources are not here, so the checks that compare this Markdown against the LaTeX it came from run on the authoring machine instead.
python tools/check_links.py every relative link resolves
python tools/check_tree.py the file types, and nothing over four megabytes
python tools/no_authoring_files.py no .tex, .pdf, .html, tracked or not
The workflow adds three guards that have each been needed in a sibling repository: no authoring source, no assembled volume or PDF, no journal or correspondence. It also asserts the shape of the edition, one chapter file and four figures for each of the twenty-four, because a chapter that fails to render leaves no error behind in a Markdown build. It simply is not there, and the index that lists it still links to it.
Install the hooks once per clone, which is the same check before the commit rather than after the push:
sh tools/install-hooks.sh
| Path | What it is |
|---|---|
chapters/NN-title.md |
the volume, one file per chapter, 00 to 25. Written only by the catalogue's publish.py |
docs/*.md |
the companion: prerequisites, foundations, tutorial, guide |
figures/NAME.svg |
every figure rendered, committed because the Markdown draws nothing without them. The TikZ source is not published |
CONTENTS.md |
the chapter table, generated, which the table above follows |
PITFALLS.md |
every pitfall in the volume, generated, alphabetical across chapters |
tools/ |
the four guards and the hook installer |
.githooks/ |
the pre-commit and commit-message hooks, installed per clone |
Figure files carry a z prefix, as z07_wiring.svg, so that a copied figure cannot
silently resolve against another volume's files.
To read it, nothing. GitHub renders the Markdown, the figures are SVG, and the mathematics is written so that the host typesets it.
To run anything, read this first. This repository is the written volume and nothing
else. Of its tracked files, 26 are chapter Markdown, 99 are SVG figures, 4 are the companion,
and the only code is four Python guards under tools/ that check this repository's own
hygiene. Every program in the volume appears as a listing inside the prose and not as a file
you can run, and none of those listings has been compiled or executed by the author, with
the one exception at the end of this paragraph. A
reader who wants to run something copies the listing out of the chapter, writes the
manifest or build file themselves, and supplies the toolchain; the chapter's own Steps
section says which machine each piece belongs on. The one exception is the tutorial's four scripts, which are complete listings and were run
once on the authoring laptop on Saturday 7 November 2026 with Python 3.12.10 and py_ecc
8.0.0, printing every line the tutorial predicts. That is a run on a laptop and not on a
board, and it was not timed.
To run the four checks, Python 3.10 or newer and no package outside the standard library.
MIT, see LICENSE. The volume leans on a great deal of other people's work:
every chapter ends with its own numbered reference list, and the appendix carries all 145
entries. Of those, 38 carry a date on which the page was fetched and the figure read from
it, 106 read "to verify" and are recorded from a citation rather than from the source, and
one carries neither and should. Fourteen entries record the licence of the implementation
they name; the rest say that the licence has not been read, because a reader who builds on
a chapter needs to know what that commits them to, and a guessed identifier is worse than
an admitted gap.