Lightweight formal verification requires the use of a workload generator that can cover all relevant code paths with a high enough probability. This is an approximation to model-checking in the traditional formal verification, which deterministically tests all possible code paths. But as we don't use a formal language, we can't actually do that.

WT-11620 introduced the alphabet of workload operations; this ticket implements the basic workload generator.