If you specify the operations (API) of your system in a relational algebra, then you can use that algebra to generate valid state transitions. (this essentially can construct the tree of continuations the article is discussing or enumerate the paths of this tree)
If you create a query language, then the state can be verified to match expectations at any point.
If you create a query language, then the state can be verified to match expectations at any point.
I'm not sure why we don't program like this.