Property-based testing as an additional validation layer for executable specs?

I was exploring the executable execution specs and did not find property-based or invariant-oriented tests. I wanted to ask whether this approach has been considered or tried before.

**Context**

The current structure of the executable specs appears compatible with property-based testing:

* deterministic, mostly pure transition functions,
* explicit fork parameterization,
* separation between spec logic and fixture generation.

**Potential value**

A property-based testing layer could serve as an additional validation mechanism during spec development by:

1. Generating randomized but constrained states and transactions,
2. Checking basic invariants and internal consistency,
3. Exercising behavior across fork transitions,
4. Reducing failures to minimal, readable examples,
5. Optionally converting those cases into deterministic EEST fixtures.

This would be a tool for spec authors only. It would not define client compliance requirements and would not replace the existing fixture-based workflow.

**Question**

Is there any existing property-based testing infrastructure for the executable specs? If not, would a small proof of concept under `execution-specs` be useful to evaluate the potential value of this approach?