Property-based testing and fuzzing
Eighteen pages on generative testing: what these two techniques actually are, why the oracle matters more than the mutator, and what both look like against a protocol with eleven independent implementations.
Five chapters: property-based testing, from generators and shrinking up to stateful model-based testing; fuzzing, organised around the oracle rather than the mutator; where static analysis, symbolic execution and formal verification sit against both; what all of it looks like when the target is Ethereum; and a deliberately thin chapter on tools.
The argument is that the interesting question about a fuzzing campaign is not how it picks the next input but how it decides something went wrong. A crash oracle finds crashes. Most of what threatens a blockchain is not a crash; it is two clients quietly disagreeing. Which is also why a protocol with eleven independent implementations gets its oracle for free.
Two smaller things I had not seen written down plainly. Integrated shrinking is not a stylistic preference: a shrinker that can wander outside its generator's invariants manufactures counterexamples that no real input could produce, which is a false positive your own test framework built for you. And a machine-checked proof covers the model, not the deployed artifact. The gap between the two is where the residual risk lives, and it is why the Ethereum Foundation's protocol security team reports finding more in formally verified code, not less.
Concepts first, because tooling here dates within months and the ideas underneath it have not moved in decades. Another redacted cut of a longer private document, and it stands on its own.
If something here is wrong, the source is a pull request away.