# E14 Reproducibility

The reference verifier is deterministic with respect to the source tree and fixed demonstration inputs.

```bash
PYTHONHASHSEED=1414 python3 verification/verify_e14.py > receipt-a.json
PYTHONHASHSEED=2424 python3 verification/verify_e14.py > receipt-b.json
cmp receipt-a.json receipt-b.json
```

The verifier builds `one-market`, `one-marketctl`, and `one-market-e14-demo` twice with:

```text
CGO_ENABLED=0
-trimpath
-buildvcs=false
-buildid=
```

The race detector is executed separately with CGO enabled on the E14 cryptographic and qualification packages. TLC and SMT mutants must fail with the targeted property; a suite that cannot detect those mutants is not accepted.
