Agent Invariant Coverage Gap Resolver

Find what your agent verification still has not covered. Submit a canonical execution graph, structured behavioral invariants and verification evidence. Receive the exact remaining obligations under the declared ci007-dag-v1 coverage model.

The resolver generates verification obligations, not tests. It never runs agents, witnesses or tests, interprets free-text requirements, or certifies safety or correctness. Zero LLM calls; no network dependencies in the core.

Quick start

Use the prefilled example or complete JSON demo. On Apify place the full input inside the request field. HTTP takes the input directly, without this wrapper. A successful Actor evaluation produces one dataset report and key-value OUTPUT.

The synthetic example has 12 required obligations, 8 covered and 4 uncovered, a coverage ratio of 0.6667. It checks a cumulative payment cap through direct, delegated and retry paths. Four missing checks include delegated above-threshold behavior and retry cumulative boundary cases.

Start with evidence: [] to discover obligations and their invariant_signature. Run your own verification outside this API. Submit evidence records with the returned signature and witness references for the next assessment. This does not authenticate the evidence or prove the agent correct.

Input contract

Top-level: graph, invariants, evidence. Unknown fields are rejected. Max 64 KiB JSON input, 250 nodes, 2000 edges, 100 invariants and 10,000 evidence records. IDs are nonempty strings up to 200 characters.

Canonical graph

graph.nodes: {id, type:"agent"|"effect", repeatable?:boolean}. An effect node is its own unique surface; there is no alias or free-text effect matching. repeatable is only permitted on effects and defaults to false.

graph.edges: {from,to,mode:"DIRECT"|"DELEGATED"|"RETRY"}. Edges are allowed transitions, not a declaration that every outgoing edge executes. Parallel branches describe alternative paths. Identical edges are deduplicated.

graph.entrypoints: optional nonempty unique agent IDs. If omitted, all agent nodes with no incoming edges are entrypoints. A disconnected effect node is not automatically an entrypoint. Explicit entrypoints can name an agent reached elsewhere too: this declares it independently invocable.

The entire graph must be a DAG. Cycles, including retry self-loops, return GRAPH_CYCLE_ERROR. A RETRY edge is an abstract retry execution mode, not an unrolled loop or retry count. Effects with repeatable:true explicitly declare multi-action applicability outside retry paths.

Mode at a surface is derived from its entrypoint-to-surface path: RETRY if any prefix edge is RETRY; otherwise DELEGATED if any is DELEGATED; otherwise DIRECT. Distinct paths may expose more than one mode. The three labels are abstractions; combined delegated-retry interaction coverage is not separately modeled.

Invariant DSL

Every invariant has unique id, effect (an effect-node ID) and operator.

Family	Additional fields	Obligation conditions
BOUND	field, comparison (<=, <, >=, >), finite numeric value, optional scope (single default or cumulative)	BELOW_THRESHOLD, AT_THRESHOLD, ABOVE_THRESHOLD
MEMBERSHIP	field, comparison (IN, NOT_IN), values (up to 100 JSON scalars)	MEMBER, NON_MEMBER
CARDINALITY	field, comparison:"<=", nonnegative safe-integer value below MAX_SAFE_INTEGER	N_MINUS_1, N, N_PLUS_1
SEQUENCE	before, after, comparison:"BEFORE"; before/after are distinct effect IDs, after must equal effect	A_BEFORE_B, B_BEFORE_A, B_ONLY

BOUND cumulative adds MULTI_ACTION_BELOW, MULTI_ACTION_AT and MULTI_ACTION_ABOVE only in RETRY mode or on an effect declared repeatable. It does not infer actual numeric traces or quantities from the graph.

BOUND relations use a real-number domain; there is no caller-specific integer, nonnegative or finite-value-domain constraint model for BOUND. CARDINALITY is a nonnegative integer count: N_MINUS_1 is impossible when N is zero. MEMBERSHIP accepts strings, finite numbers, booleans and null with exact typed equality; duplicates and set ordering are normalized. An empty set makes MEMBER impossible. Object/array membership and arbitrary natural language are unsupported.

SEQUENCE examines allowed complete entrypoint-to-leaf paths containing B (after). A_BEFORE_B means both effects occur in that order; B_BEFORE_A is reversed; B_ONLY contains B without A. Paths without B create no required sequence checks because the implication is vacuous. Conditions are projected using the mode at B, ignoring mode changes after B. An ordering case with no such graph path is unreachable. Dynamic programming avoids enumerating exponentially many paths.

The graph represents allowed transitions and their order, not concurrency, parallel execution, scheduler behavior, data-dependent guards, cross-invariant feasibility or real-world reachability. Marking an edge incorrectly changes the report. For graph adapters, normalize these semantics before calling.

Evidence and signature binding

Each evidence record requires:

{
  "invariant_id": "spend-cap",
  "invariant_signature": "<64 lowercase hexadecimal characters returned by assessment>",
  "surface": "payment",
  "mode": "DIRECT",
  "condition": "ABOVE_THRESHOLD",
  "result": "PASS",
  "witness_id": "your-test-run-reference"
}

PASS means the verification check passed, including expected rejection or blocking for a violating input. It does not mean an above-limit payment was allowed. expected_case on each obligation states whether the described boundary/order satisfies or violates the invariant; your external harness must test the intended enforcement behavior.

The signature is SHA-256 of the canonical normalized invariant and coverage-model identifier. It is a binding identifier, not an authenticity signature. Evidence must supply it. A mismatch is reported as stale and does not cover an obligation. Changing a threshold, comparison, scope or membership set therefore invalidates old evidence. Graph mutations recompute applicable obligations; a new path creates new gaps while existing matching obligations can retain evidence.

Evidence for an unknown invariant, wrong surface, unsupported condition or unreachable obligation returns EVIDENCE_WITHOUT_OBLIGATION. Remove records that are no longer applicable when changing the graph. Exact duplicate records are deduplicated; repeated witnesses never increase the number of covered obligations. A witness ID may be a caller's reference, not a URL; it is not fetched or validated.

Report and decisions

• COVERED: every required obligation has at least one PASS and no FAIL record under the current invariant signature.
• GAPS_FOUND: one or more required obligations have no passing evidence. FAIL-only checks remain uncovered and retain failing witness references.
• CONFLICTING_EVIDENCE: at least one obligation has both PASS and FAIL evidence. Conflicts are never counted as covered.
• NO_REACHABLE_OBLIGATIONS: no required checks are reachable; ratio is null, not a fabricated 100% coverage. Per-invariant status is UNREACHABLE in this case.

coverage.required = covered + uncovered + conflicting. Ratio is covered / required, rounded to four decimals, or null for zero required. This is a count ratio under this model, not a risk score.

Outputs include normalized invariants and signatures, per-invariant summaries, all required obligations, uncovered obligations, unreachable combinations with pruning reasons, conflicts, passing/failing witness IDs and stale evidence. Input list/key ordering and duplicate edges/evidence do not change semantic output.

Explicit failures

Errors are machine-readable: INVALID_INPUT, INVALID_GRAPH, INVALID_INVARIANT, UNSUPPORTED_INVARIANT, UNKNOWN_EFFECT, INVALID_EVIDENCE, EVIDENCE_WITHOUT_OBLIGATION, GRAPH_CYCLE_ERROR, AMBIGUOUS_SURFACE and UNSUPPORTED_EXECUTION_MODE. HTTP returns 400 for invalid/unsupported inputs. Apify fails invalid input before writing a result. Ambiguous duplicate node IDs are rejected rather than merged.

Boundaries

A covered declaration is not proof of correctness or safety. Graphs, repeatability, invariants, test meaning, outcomes and witness references are caller supplied and unauthenticated. The resolver does not build graphs, generate or run tests, inspect test code, evaluate witness trust, issue a certification or change a deployment. It does not infer missing invariants.

Input schema. Contract and integration guide.

Contact: bonometti.work.ai@gmail.com