An agent-facing property job is only as honest as its seeds. Replay the seeds that already produced parent hits, hold out a seed set the generator never saw, and freeze flakes only on the replay set. A green run on a fresh RNG stream does not prove the patch preserved the invariant. It often proves the counterexample was dropped.
The failure mode
Property tests look robust because they claim to search a space. In CI they usually search whatever stream the runner draws that morning. Agent patches exploit that gap. The model changes a parser, the property draws new inputs, and last week's failing example never appears. The job is green. The bug is still in the tree.
Fixtures close part of the hole. They do not close all of it. A fixture without a seed journal cannot tell you whether a later freeze covers a real hit or covers a test that never fired. Holdout seeds close a second hole. They detect properties overfit to the replay set, including properties a model proposed after seeing those examples.
What to record
Keep one journal per property, outside the path the agent can edit. The journal is the artifact. The job color is not.
{
"id": "parse_ledger_balances",
"selector": "tests/properties/test_ledger.py::test_balance_invariant",
"parent_sha": "REPLACE_WITH_MERGE_BASE",
"replay": {
"seeds": [8, 21, 34],
"fixtures": [
"oracles/parse_ledger_balances/8.json",
"oracles/parse_ledger_balances/21.json"
],
"hits": 3,
"last_hit_at": "2026-09-18T12:00:00Z"
},
"holdout": {
"seeds": [55, 89, 144],
"generator_saw": false
},
"flake": {
"replay_flakes": 1,
"holdout_flakes": 0,
"freeze_replay_until": null
},
"state": "locked"
}
Treat every timestamp and hit count in that sample as a placeholder. Copy the shape, not the numbers. generator_saw must stay false for holdout seeds. If a scratch job used those values while proposing the property, they are replay seeds. Move them.
Four states, one freeze target
-
proposed— exists only on a scratch tree. -
hit— at least one replay seed failed the parent, or a fixture matched. -
locked— a human promoted the journal into the merge gate. -
replay-frozen— replay seeds are flaky; holdout seeds still run.
There is no freeze state for holdouts. A flaky holdout is a failed gate or a deleted property, not a skipped one. That rule is the difference between a freeze and a mute.
Pipeline
The steps below are a procedure, not a report of a production incident. Run them in order. Do not let the agent patch rewrite the journal.
1. Pin the parent and open a scratch tree
PARENT_SHA=$(git merge-base HEAD origin/main)
git fetch --quiet origin
git worktree add --detach /tmp/oracle-parent "$PARENT_SHA"
git worktree add /tmp/oracle-scratch -b scratch/oracles-"$PARENT_SHA" "$PARENT_SHA"
mkdir -p oracles
Scratch may receive model output. Parent is read-only. The agent branch is not checked out here on purpose. Delete the scratch worktree after classification. Do not open a pull request from it.
2. Propose properties without the patch or the holdout list
A coding model can draft property tests from public parent functions. It must not read the agent diff. It must not receive holdout seeds. If you need a machine that is not your merge runner, park the proposer on a scratch host.
Disclosure: This article was prepared as part of MonkeyCode's product outreach. MonkeyCode offers free model access and a free server option, which can run that proposer against the parent worktree so merge CI never executes untrusted generated files. The journal still has to be reviewed and copied by a human into a protected path. A free server does not change the hit rule or the holdout rule.
3. Hunt hits on the parent with an explicit seed list
The runner below is a reference implementation. Register any Hypothesis profile you set, or omit that environment variable. --hypothesis-seed reproduces one starting point; it is not a proof that the full search space was covered.
"""parent_seed_hunt.py — reference runner, unexecuted here."""
from __future__ import annotations
import json
import os
import subprocess
import sys
from pathlib import Path
def run_one(selector: str, cwd: Path, seed: int, timeout: int = 45) -> dict:
env = os.environ.copy()
cmd = [
sys.executable, "-m", "pytest", "-q",
selector, f"--hypothesis-seed={seed}",
]
try:
proc = subprocess.run(
cmd, cwd=cwd, env=env, capture_output=True, text=True,
timeout=timeout, check=False,
)
return {
"seed": seed,
"returncode": proc.returncode,
"failed": proc.returncode != 0,
"timed_out": False,
"stderr_tail": proc.stderr[-500:],
}
except subprocess.TimeoutExpired:
return {
"seed": seed,
"returncode": -1,
"failed": False,
"timed_out": True,
"stderr_tail": "",
}
def hunt(selector: str, parent: Path, candidate_seeds: list[int]) -> dict:
rows = [run_one(selector, parent, s) for s in candidate_seeds]
hits = [r["seed"] for r in rows if r["failed"]]
timeouts = [r["seed"] for r in rows if r["timed_out"]]
return {"hits": hits, "timeouts": timeouts, "rows": rows}
if __name__ == "__main__":
parent = Path(sys.argv[1])
selector = sys.argv[2]
seeds = [int(x) for x in sys.argv[3].split(",")]
print(json.dumps(hunt(selector, parent, seeds), indent=2))
python3 parent_seed_hunt.py /tmp/oracle-parent \
tests/properties/test_ledger.py::test_balance_invariant \
2,3,5,8,13,21,34,55,89
Seeds that fail the parent go to replay.seeds. Write the shrinking input to oracles/<id>/<seed>.json. Seeds that never fail stay eligible for holdout, provided the proposer never saw them. Timeouts during the hunt are not hits. They are noise. Do not lock a property whose only parent signal is a timeout.
4. Split the seed space before any patch is scored
"""split_seeds.py — deterministic split after the hunt."""
import hashlib
def holdout_from_parent(parent_sha: str, k: int = 3, modulus: int = 10_000) -> list[int]:
"""Stable unseen seeds derived from the merge base, not from the model."""
out = []
for i in range(k):
digest = hashlib.sha256(f"{parent_sha}:{i}".encode()).hexdigest()
out.append(int(digest[:8], 16) % modulus)
return out
def split_hits_and_holdout(all_seeds: list[int], hits: list[int], parent_sha: str) -> dict:
hit_set = set(hits)
replay = sorted(hit_set)
if not replay:
return {"error": "zero-hit", "replay": [], "holdout": []}
derived = [s for s in holdout_from_parent(parent_sha) if s not in hit_set]
unused = [s for s in all_seeds if s not in hit_set]
holdout = derived or unused[:3]
return {"replay": replay, "holdout": holdout}
Zero hits means the candidate is dead. Delete it. Do not freeze it. Do not copy unused seeds into replay to make the journal look populated. If a derived holdout collides with a replay seed, drop that value and draw the next digest. Collision handling is cheap. Calling a seen seed a holdout is not.
5. Human lock, then score the patch on two lanes
Replay lane: run fixtures plus replay.seeds. Any miss is a regression. This lane is blocking.
Holdout lane: run holdout.seeds with generator_saw: false. A failure here is also blocking. It means the invariant still searches, not that it memorized three examples.
python3 score_journal.py --journal oracles/parse_ledger_balances.json \
--tree "$PWD" --lane replay
python3 score_journal.py --journal oracles/parse_ledger_balances.json \
--tree "$PWD" --lane holdout
If the agent patch adds tests, ignore them in both lanes. Advisory jobs may run those tests. They do not write the journal. Promotion from hit to locked is a human write. No model, including the one that proposed the property, gets that write.
6. Freeze only replay flakes, with an expiry
A replay seed that failed the parent last week and times out today is merge noise. Set freeze_replay_until to a concrete timestamp. While the freeze is active, replay fixtures that still load must keep running. Only the unstable seeds are skipped. When the clock expires, those seeds return as blocking. If they fail again, fix the test or the platform. Do not extend the freeze from the agent branch.
Holdout timeouts do not start a freeze. They fail the gate or they cause the property to be removed from locked. Silent holdout skips are how overfit oracles survive. A freeze without hits >= 1 is invalid. The correct state for that row is deletion.
Decision table
| Lane | Parent hunt | Patch run | Flake? | Action |
|---|---|---|---|---|
| replay | hit | fail | no | block merge (regression) |
| replay | hit | pass | no | allow this lane |
| replay | hit | mixed / timeout | yes | freeze those seeds only; keep fixtures |
| replay | miss | n/a | n/a | refuse lock; refuse freeze |
| holdout | unused seeds | fail | no | block merge (invariant still live) |
| holdout | unused seeds | pass | no | allow this lane |
| holdout | unused seeds | timeout | yes | fail gate or drop property |
| either | proposer saw seed | any | n/a | move seed to replay; do not call it holdout |
Encode the table in score_journal.py. Do not encode it in the model prompt that proposed the property. The prompt is not an audit trail.
Limitations
Hypothesis seeds are not portable across dependency bumps. When you upgrade the property library, re-hunt on the parent and rewrite the journal. The old seed list is then a historical fixture source, not a live search key. Replaying a stale seed that no longer shrinks to the same input is a false regression. Re-record the fixture bytes when that happens.
This workflow does not estimate how much of the product is specified. It only estimates whether a locked invariant is still attached to counterexamples. A journal with three replay seeds can still miss a fourth class of bug. A holdout of three seeds is a canary, not a fuzzer budget. Raise k only when parent runtime allows it. Do not claim statistical coverage.
The scratch host does not have to be any particular vendor. Any isolated machine works. The method fails open if the bot account can edit oracles/ or if holdout seeds leak into the proposer prompt. Protect the path with CODEOWNERS, a second repository, or a signed artifact the merge job verifies. Pick one. Do not rely on prompt instructions to keep the bot out.
Who should not use this
Skip the journal if your tests are non-deterministic by design: live network, wall-clock, shared staging. Skip it if the deliverable is the test suite the agent authors. Skip it if you cannot protect a path or a second repo from the bot. Screenshot and visual diffs do not produce replayable seeds. Keep them on a different gate.
The useful part of the pipeline is the journal, the split, and the freeze rule. Free model access and a free scratch server are only a way to propose candidates without billing merge runners. If those candidates never hit the parent, throw them away.
Top comments (0)