Skip to content

Architecture

TermVerify separates application control from verification policy.

Application under test
  ├── direct adapter: fast commands and structured observation   [built]
  └── production adapter: PTY/subprocess terminal path           [built: Windows ConPTY + JSONL]
                         │
                    TermVerify runners
  ├── deterministic run configuration                            [built]
  ├── transcript dispatch and replay                             [built]
  ├── observation normalization                                  [built]
  ├── comparator/oracle policies                                 [partial: exact comparator only]
  ├── property and state-machine integration                     [planned]
  └── reports and failure artifacts                              [planned]

Sequencing and rationale for the planned rows live once, in the product vision.

The runner, comparison/replay, oracle-policy, and reporting rows describe the Phase 2 verification-core layer, active under the accepted phase-2-verification-core-boundary.md decision. At the current pre-release boundary, TermVerify ships the adapter/runtime contracts, direct and Windows terminal adapters, transcript codec/validation, safe redacted persistence, and — from Phase 2 slices 1–3 — the termverify.recorder transcript recorder with its minimal scripted-run orchestrator, the termverify.comparator exact comparator with its deterministic plain-text report (equivalence excludes only the envelope run_id; the exclusion set is closed), and the termverify.replay caller-bound replay engine (selector agreement disclosed, never enforced). Oracle policies, differential orchestration, and behavioral baselines remain outside the accepted boundary.

Boundary

Applications expose a small adapter surface: start a deterministic run, dispatch an input event, advance an explicit clock, observe structured state/UI evidence, and stop. State save/restore is not part of the adapter surface.

Phase 1 serializes that surface into single-flight execution epochs. Complete capability negotiation is followed by one positional initial readiness observation. Each later input is drained to an application-port-reported quiescent observation or terminal result before another input is accepted. Quiescence never depends on wall-clock quiet periods. The accepted adapter execution contract defines readiness, causality, stop/drain behavior, and enforcement receipts for the public immutable contracts and direct execution path. The protocol validator, canonical fixtures, and generative property model implement the same lifecycle semantics. termverify.direct.DirectAdapter composes explicit constraint and application ports without consulting ambient time, terminal, or process state.

The direct adapter is the default for fast unit tests, and is the path property testing will use when it exists ([planned] above). The Windows production path is termverify.terminal.TerminalAdapter over the reviewed ConptyBinding, with the fail-closed termverify.vt.VtScreenNormalizer above it. That adapter is platform-neutral and also ships PosixPtyBinding, whose evidence today stops at the binding, so there is no POSIX production path to claim yet (issue #269). On Windows the path verifies real terminal input, rendering, resize, EOF/exit evidence, forced teardown, and process-tree handling through explicit readiness-marker epochs. A successful Windows integration run has exercised the real binding, cooperation-tier constraint delivery, text input, normalized/replayable frames, resize, and observed exit. termverify.key-encoding/v1 dispatch is implemented; real-child Windows-matrix evidence proves exact byte delivery to a cooperative raw-mode subject for one representative of every encodable family class, replay identity, native exit through an in-band key, and fail-closed unencodable input with OS-observed teardown. This is delivery evidence, not key-support negotiation, input-mode tracking, or a claim that an arbitrary subject decodes every chord.

The production adapter does not claim OS filesystem/network containment. Its terminal dimensions receipt is OS-level; the other constraints require explicit subject-cooperation ports whose delivered receipts disclose delivery rather than subject compliance. Non-empty terminal capabilities remain unsupported. The terminal adapter is platform-neutral and ships a POSIX binding, but no leg anywhere yet drives a real subject through it on a pseudoterminal, so there is no POSIX terminal path to rely on (issue #269). Browser bridging remains deferred until the direct and terminal vertical slices prove that a shared abstraction is needed.

Process containment is bounded, and the boundary is disclosed

A subject's process tree is contained by a kill-on-close job object on Windows and by a process group on POSIX. Neither is escape-proof, and TermVerify does not claim otherwise. A process can leave the containment in a known way on each platform: on POSIX by starting a new session (setsid), which no process-group signal reaches; on Windows by descending from a child that exited before it could be assigned at all. The ConPTY binding closes the other historical Windows escape — a descendant started between CreateProcess and job assignment — by spawning its child CREATE_SUSPENDED and assigning before the main thread resumes (issue #235); the JSONL transport's Windows spawn does not own CreateProcess and retains that window.

Such a survivor is not reaped. Reaping it portably would require cgroups or a subreaper — horizontal platform machinery, rejected as out of scope by recorded owner decision — so the honest position is disclosure, not a guarantee. A verified run must not be read as asserting that no process outlived it.

What replaces the containment claim is narrower, and splits into what every platform owes and what only POSIX currently delivers. Keeping the two apart is the point: the previous claim failed precisely by averaging them.

Guaranteed on every platform:

  • Failure classification is identical. When a run produces a result, that result is structured and carries a real exit record or a real forced-termination record. No record is ever fabricated, and no run reports anything it did not observe.

Guaranteed on POSIX only:

  • A survivor cannot hold the verifier hostage. This is the substantive guarantee, because the damaging case is not the orphan itself but the pipe end it holds: a reader blocked on a descriptor no containment can close wedges permanently. The POSIX pipe binding therefore interrupts its own blocked reads and writes through a self-pipe instead of relying on containment to reach the holder, so the abort deadline still produces a structured failure and the teardown still returns.

Not guaranteed on Windows, and disclosed as such: select/poll do not work on anonymous pipe handles, so the job object is the only interruption available there. A holder outside the job — a process from the assignment window, or a descendant of a child that exited before assignment — can still stall a teardown, and a stalled teardown produces no result at all rather than a wrong one. Tracked as issue #213's Windows leg.

The invariant behind both, stated because it has been violated twice: release every mechanism that can unblock an operation before performing an operation that can block on it. A teardown that blocks inside a finally cannot report anything at all.

Design constraints

  • No required model provider, agent harness, web service, or GUI toolkit.
  • Run configuration makes seed, clock, terminal dimensions, locale, timezone, filesystem root, and network policy explicit.
  • The library owns generic protocols and comparison; applications own domain semantics through adapters and normalizers.
  • An adapter either applies each requested deterministic constraint — at the strongest tier its mechanism supports, down to delivered, where honoring the value is subject cooperation — and reports the effective value with that tier, or returns a structured unsupported result before input dispatch; it never silently falls back to ambient state, and never records a tier stronger than the mechanism it used.
  • Requested/effective equality does not prove enforcement. Each applied result is backed by a constraint-specific receipt from the path that applied the constraint; direct adapters can produce those receipts only through explicit application ports.