[aviggiano]

Summary

• replace legacy implemented-property contracts with strict @3 evidence
• require exact semantics, executable oracle/entrypoint identity, positive and negative regressions, and reachability evidence
• require campaign intended/admitted entrypoint sets and reject complete campaigns with omitted properties
• make Recon liveness guidance selector-aware and protocol-agnostic

Fixes #519
Fixes #524

Greptile Summary

The PR replaces legacy implemented-property contracts with an @3 evidence contract and adds campaign admission checks intended to prevent false invariant-coverage claims.

• Requires exact semantic coverage, executable oracle metadata, regression paths, and reachability evidence for implemented properties.
• Records and compares intended versus backend-admitted property entrypoint sets.
• Updates built-in topologies, reports, prompts, schemas, and runtime gates for the new contract.
• Removes legacy @1 and @2 implemented-property contract handling.

Confidence Score: 4/5

The PR should not merge until the new evidence paths are tied to real declared artifacts, because unsupported property implementations can currently receive complete campaign credit.

The new strict contract requires evidence fields but validates only their textual presence, while campaign admission trusts the resulting implemented record without checking that the referenced regressions or reachability proof exist.

Files Needing Attention: packages/artifacts/src/property-provenance.ts, packages/runtime/src/artifact-gates.ts

Important Files Changed

Filename	Overview
packages/artifacts/src/property-provenance.ts	Adds @3 oracle and reachability fields, but treats evidence paths as unverified strings, allowing unsupported implemented-property claims.
packages/artifacts/src/artifact-contracts.ts	Replaces legacy implemented-property contracts with @3 and enables strict executable-evidence validation.
packages/runtime/src/artifact-gates.ts	Adds campaign intended/admitted entrypoint and semantic-completeness diagnostics, but does not authenticate the new evidence paths.
packages/runtime/src/templates/smithers/workflows/workflow.tsx	Updates generated workflow handoffs and report reconstruction to require the @3 contract.
packages/cli/src/report-artifacts.ts	Makes report reconciliation fail closed for malformed or missing current @3 implementation handoffs.
.ultrafuzz/prompts/strategies/invariants/implement-properties.md	Directs agents to classify exact semantics and provide executable-oracle, regression, and reachability evidence.
.ultrafuzz/prompts/strategies/invariants/invariant-testing-campaign.md	Requires campaigns to preserve intended and admitted property entrypoint sets and avoid complete outcomes when coverage is incomplete.

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart LR
  P[Implementation agent] --> I[implemented-properties @3]
  I --> V[Artifact schema validation]
  V --> C[Invariant campaign]
  C --> A[Admission checks]
  A --> R[Final report]
  T[Regression and reachability paths] -. currently checked only for nonempty strings .-> V

Loading

Prompt To Fix All With AI

### Issue 1
packages/artifacts/src/property-provenance.ts:428-429
**Evidence paths remain unauthenticated**

When an implementation record names nonexistent or unrelated positive, negative, or reachability evidence paths, the `@3` validator checks only that those strings are nonempty, and campaign admission still credits the property as implemented, allowing a campaign with no executable regression or reachability proof to be reported as complete.

---

For each issue above, determine whether it is valid and should be fixed. If so, fix it directly.

_{Reviews (1): Last reviewed commit: "test(invariants): enforce current oracle..." | Re-trigger Greptile}

Greptile also left 1 inline comment on this PR.

Context used (4)

• Knowledge Base — Artifacts
• Knowledge Base — Runtime: Run Orchestration Lifecycle
• Knowledge Base — Prompts
• Knowledge Base — Topology

[greptile-apps]

Evidence paths remain unauthenticated

When an implementation record names nonexistent or unrelated positive, negative, or reachability evidence paths, the @3 validator checks only that those strings are nonempty, and campaign admission still credits the property as implemented, allowing a campaign with no executable regression or reachability proof to be reported as complete.

Knowledge Base Used:

• Artifacts
• Runtime: Run Orchestration Lifecycle

Prompt To Fix With AI

This is a comment left during a code review.
Path: packages/artifacts/src/property-provenance.ts
Line: 428-429

Comment:
**Evidence paths remain unauthenticated**

When an implementation record names nonexistent or unrelated positive, negative, or reachability evidence paths, the `@3` validator checks only that those strings are nonempty, and campaign admission still credits the property as implemented, allowing a campaign with no executable regression or reachability proof to be reported as complete.

**Knowledge Base Used:**
- [Artifacts](https://app.greptile.com/monad-foudnation/-/custom-context/knowledge-base/monad-developers/ultrafuzz/-/docs/artifacts.md)
- [Runtime: Run Orchestration Lifecycle](https://app.greptile.com/monad-foudnation/-/custom-context/knowledge-base/monad-developers/ultrafuzz/-/docs/runtime.md)

---

For each issue above, determine whether it is valid and should be fixed. If so, fix it directly.

[aviggiano]

Closing without merge per updated scope: issues labeled help wanted are excluded from this task.