engineering-verification-loop

name

engineering-verification-loop

description

Top-level engineering verification orchestration skill and distributable skill-pack entry point. Use when Codex must plan, execute, or review a Go/Python-heavy engineering change that needs an auditable TDD inner loop plus risk-based gates for formal correctness, model-to-implementation conformance, algorithms, performance, API/schema compatibility, CI failures, profiling, distributed behavior, or experiment claims.

Engineering Verification Loop

Operating Contract

Use this skill as a thin orchestration layer. Classify the change, route observable behavior through test-driven-development, layer each additional risk through the right specialist skill, enforce entry/exit gates, and produce one Evidence Bundle 2.0. Do not duplicate specialist procedures; load the specialist skill when that gate is active.

Do not claim a behavior change is ready without a valid TDD cycle. Do not claim a change is ready when any active risk lacks passed evidence. Unsupported claims are structured limitations; they do not make a readiness claim true. Non-behavioral waivers support only restricted conclusions.

When Go/Python implementation work is claimed to follow a Dafny/TLA model, require explicit model-to-implementation conformance evidence. Dafny/TLA proof is model evidence; handwritten Go/Python needs fixtures, fuzz, differential tests, or generated-code linkage before implementation alignment can be claimed.

Risk Routing

Risk or symptom	Required specialist
Feature, bug fix, observable behavior change	test-driven-development
Behavior-preserving or legacy refactor	test-driven-development
Security-sensitive invariant, auth, parser/validator, critical state transition	dafny-verification for formal_correctness in addition to TDD
Optimized implementation must match oracle/model	property-based-differential-testing
Algorithm/data-structure choice, benchmarked candidate	algorithm-selection-benchmarking
OpenAPI, JSON Schema, Protobuf, GraphQL, SDK surface	api-contract-compatibility
CI failure, noisy log, regression reproduction	ci-regression-forensics
Experiment/benchmark claim needs reproducibility	reproducible-experiment-analysis
Hot path, CPU/memory/allocation/I/O optimization	profiler-guided-optimization
Dafny/TLA model must be mapped to Go/Python implementation evidence	model-implementation-conformance
Distributed protocol semantics	tla-distributed-model-checking

Workflow

1. Classify the change type and TDD mode:
   • feature or bugfix -> red_green_refactor;
   • covered behavior-preserving refactor -> green_refactor;
   • uncovered legacy refactor -> characterization_refactor;
   • strictly non-behavioral change -> structured waived mode with a restricted conclusion.
2. Set change.behavior_change=true for any observable runtime, API, persistence, dependency, build, security, or operational behavior change. Route it through test-driven-development before claiming readiness; behavior is orthogonal to the outer risks list.
3. Classify additional risks:
   • formal correctness-critical;
   • algorithmic/performance-sensitive;
   • API/schema/public contract;
   • experiment or benchmark claim;
   • CI failure/regression;
   • distributed protocol behavior.
4. Build a verification plan with requirement-to-test traceability, cycle phases, regression scopes, active risk labels, specialist skills, commands/artifacts expected, and stop conditions.
5. Run gates in dependency order:
   • write acceptance tests and capture valid Red before production behavior for features and bug fixes;
   • capture baseline Green or characterization Green before refactoring;
   • formal spec/proof after acceptance criteria and valid Red, but before production implementation when applicable;
   • algorithm choice before profiling when the algorithm is unknown;
   • differential/property tests before accepting optimized behavior;
   • API compatibility before claiming contract safety;
   • reproducibility audit before trusting experiment conclusions;
   • profiling after a representative workload exposes a bottleneck;
   • CI forensics first when the entry point is a failing job, then require a valid behavioral Red for the prevention fix;
   • model-to-implementation conformance before claiming handwritten Go/Python matches a verified model;
   • targeted Green, explicit refactor decision, then post-decision targeted, affected, and full regression before final outer-gate acceptance.
6. Capture executions with evl run-gate; never execute command strings from a bundle or hand-author runner-owned results.
7. Stop and reroute when a gate fails. Do not continue to later claims as if earlier evidence passed.
8. Assemble an Evidence Bundle 2.0 and audit it with evl audit (or the packaged auditor entry point).
9. Final answer must include the TDD mode/cycles, active outer risks, specialist skills used, commands, artifact paths, pass/fail status, unsupported claims, and next gate if blocked.

Decision Rules

• If observable behavior can change, set change.behavior_change=true and require test-driven-development; do not add behavior to the outer risks list, and do not infer formal proof from ordinary behavioral evidence.
• If a feature or bug fix lacks valid Red, stop. Import, collection, compile, dependency, timeout, and environment failures are not valid TDD Red.
• If a pure refactor has adequate tests, require baseline Green rather than fabricated Red. If coverage is inadequate, add characterization tests before editing production code.
• If correctness and performance both matter, prove/model critical properties and add differential tests before interpreting speedups.
• If an API check fails in CI, use ci-regression-forensics to classify and reproduce, then hand the compatibility issue to api-contract-compatibility.
• If benchmark results support a product/research claim, route through reproducible-experiment-analysis; raw benchmark output alone is insufficient.
• If the bottleneck is not measured, do not optimize; use profiler-guided-optimization.
• If a change modifies distributed semantics, use tla-distributed-model-checking; Dafny may still verify local deterministic handlers.
• If Go/Python code is handwritten against a Dafny/TLA model, include conformance risk and route through model-implementation-conformance.
• If an implementation_conformance claim exists, declare implementation_languages, Go/Python targets, and target-language test artifacts; do not let the claim stand without target-language gates.
• If a benchmark uses synthetic inputs, do not claim production impact unless replay, canary, shadow, or production evidence also exists.
• If CI is an active risk, require a structured CI failure footer or a structured unsupported_claims limitation scoped to ci-observability.

Evidence Bundle 2.0

Evidence Bundle v1 is not accepted. Migrate it with evl migrate-v1; the result remains change.tdd_ready=false until real TDD evidence is captured. Do not synthesize historical Red.

• schema_version and change_summary: identify the v2 format and summarize the change.
• change: ID, type, behavior_change, TDD mode/readiness, real base/candidate commit IDs, and optional compile-stub exception or waiver. Commit IDs are 40/64-character hexadecimal Git IDs that resolve in the audited repository; WORKTREE is invalid.
• requirements and acceptance_criteria: stable traceability from requested behavior to tests.
• tests: stable IDs, paths, frameworks, levels, normalized selectors, and acceptance-criterion links.
• tdd_cycles: Red or baseline Green, targeted Green, explicit refactor decision, and regression execution references.
• regression: targeted, affected, and full scopes plus their execution references.
• test_sufficiency: declared profile, coverage/mutation thresholds and results, critical/equivalent mutants, standard JSON report artifacts, and optional quality_checks; the core profile requires deterministic evidence, at least two flake reruns with no failures, zero weakened assertions, enough repeated test logs, and a matching standard quality audit result.
• risks: outer labels only: formal_correctness, conformance, algorithm, performance, api, ci, experiment, profile, and distributed; ordinary behavior is represented by change.behavior_change and TDD cycles.
• risk_traits: optional descriptive context that does not activate or satisfy an outer gate.
• targets: Go/Python changed implementation targets and entrypoints.
• implementation_languages: go, python, or both when target code is in those languages.
• formal_coverage_map: model properties mapped to Go/Python evidence, or a repo-root-contained path to that JSON. Each declared implementation language must cover each claimed property.
• workloads: structured workload manifests with synthetic_only, replay, shadow, canary, or production level.
• claims: structured readiness/performance/conformance claims linked to evidence and workloads.
• ci_structured_footer: for active CI risk, a strict present: true footer linked to the matching failing ci-log, unless a structured ci-observability limitation blocks or scopes the claim.
• artifacts: immutable result artifacts with SHA-256 and runner provenance containing argv, environment, Git snapshot, exit code, and parsed report. Snapshot head is a real commit ID, tree is that commit's tree ID, and diff_base64 contains one canonical JSON structure of tracked entries (path, status, content or deletion) plus untracked file/symlink entries; the auditor recomputes changed_paths from it. Each execution includes a snapshot-manifest provenance artifact linked by snapshot.evidence_ref.
• evidence: object keyed by risk label. Each item needs skill, command, status, artifact_refs, and summary; a passed outer-risk entry must reference a runner-owned specialist result and a fresh qualifying structured specialist JSON report, not only an ordinary test-log.
• unsupported_claims: structured limitations with scope, disposition, and related fields.
• extensions: namespaced non-core data; core objects otherwise reject unknown properties.

Use evl audit <bundle.json> [--repo-root PATH] as the final gate. Capture a phase with evl run-gate --bundle BUNDLE --cycle ID --phase PHASE --adapter ADAPTER --selector SELECTOR [--repeat N] [--attach KIND=PATH ...] [metadata options] -- COMMAND ARG...; the project-native argv must appear only after --. Behavioral pytest phases require python -m pytest with an explicit verbose flag; direct pytest shims are rejected. Go phases require go test -json -count=1 and <Package>::<TestName> selectors. The generic adapter cannot establish any non-waived TDD phase. Except for Red, phases run at a clean candidate revision and must leave the captured snapshot unchanged. Use --repeat 3 on a passing Green/regression phase to capture an initial attempt plus two comparable flake reruns. Attach only reports produced by that execution. Run outer gates with evl run-specialist ... --report PATH -- COMMAND...; a passing result requires a fresh contract-valid report. Valid phases are red, green, baseline_green, refactor, targeted, affected, and full.

Boundaries

This skill coordinates. It does not design TDD details, repair Dafny proofs, design generators, interpret flamegraphs in depth, fix CI, write OpenAPI compatibility policy, or prove experiments. Those tasks belong to the named specialist skills.

Resources

• evl run-gate: execute explicit project argv and append test provenance plus attached coverage/mutation reports to Bundle 2.0.
• evl audit: validate Bundle 2.0 structure, TDD integrity, sufficiency, artifacts, and active outer risks.
• evl migrate-v1: create a blocked v2 draft without fabricating historical TDD evidence.
• evl eval-audit: validate structured Skill evaluation cases and optional observed results.
• scripts/audit-evidence-bundle.py: compatibility wrapper for the fail-closed bundle audit.
• scripts/infer-go-python-targets.py: infer Go/Python targets from changed file lists.
• ../test-driven-development/SKILL.md: acceptance-test design, Red-Green-Refactor, characterization, and sufficiency gates.
• references/risk-routing-matrix.md: expanded routing and gate order.
• references/evidence-policy.md: required evidence by claim type.
• references/go-python-policy.md: Go/Python-specific proof, conformance, benchmark, and profile policy.
• assets/templates/evidence-bundle.json: strict schema-valid Bundle 2.0 behavioral example with runner provenance.
• assets/templates/formal-coverage-map.json: model-to-implementation mapping template.
• assets/templates/workload-validity.json: structured workload and claims template.
• assets/templates/verification-plan.md: concise plan template.
• assets/templates/final-report.md: final report template.