feat: initial code import from monorepo (mirror)

.github/workflows/docs-check.yml

@@ -0,0 +1,12 @@
+name: docs-check
+on:
+  push: { branches: [main] }
+  pull_request: { branches: [main] }
+jobs:
+  check:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with: { python-version: "3.12" }
+      - run: python scripts/check_docs.py

PROVENANCE.md

@@ -0,0 +1,8 @@
+# Provenance
+
+Clean import (no history rewrite) from `verifiablelabs/verifiable-labs-envs`
+at commit `a0f30dc547a73aaae8608d193f94035192404627` (main). Docs authored fresh from approved positioning; no private implementation details.
+
+The source monorepo remains canonical until the split flips; this mirror is
+refreshed by the migration tooling documented in
+`verifiable-labs-private/docs/ops/github-repo-split-migration.md`.

docs/architecture-overview.md

@@ -0,0 +1,24 @@
+# Architecture overview (public)
+
+Verifiable Labs runs an Evaluate / Improve / Gate / Substrate pipeline:
+
+1. **Contract compiler** turns an agent goal into an evaluation contract.
+2. **Scenario generator** produces public / hidden / OOD / adversarial
+   scenarios (generated after freeze — never reused from training corpora).
+3. **Evaluation** runs the agent through a provider abstraction
+   (dummy provider in the open SDK; commercial providers server-side).
+4. **Contamination firewall** scores data-contamination risk (DCR) and
+   enforces split policy; **anti-hack scanning** scores hack risk.
+5. **Clean promotion gate** decides ACCEPT / REJECT / LIMITED_ROLLOUT from
+   clean VGS, generalization gap, and regression checks.
+6. **Assurance card** records the decision; **substrate records** capture
+   transfer metrics and failure memory under an explicit data policy.
+
+The open-source surface is the SDK contracts ([vlabs-sdk](https://github.com/verifiablelabs/vlabs-sdk))
+and the formal track ([vlabs-formal](https://github.com/verifiablelabs/vlabs-formal)).
+Scenario generation, the firewall, anti-hack detection details, and the
+platform are private — that separation keeps the feedback clean.
+
+Selected mathematical properties behind the contamination-resistant
+promotion gate are machine-verified in Lean 4. The implementation is
+property-tested against the formal specification.

docs/onboarding.md

@@ -0,0 +1,12 @@
+# Onboarding paths
+
+1. **Dashboard upload** — upload an agent bundle; receive a contract draft,
+   scenario plan, and dry-run cost estimate before anything runs.
+2. **CLI / API key** — drive evaluations from your terminal or CI.
+3. **Bring your own key (BYOK)** — your provider key, encrypted and
+   project-scoped; we charge orchestration/scoring only, no token markup.
+4. **Self-hosted / VPC** — run inside your boundary (architecture defined;
+   productionization in progress).
+
+Privacy defaults: evaluate-only, nothing exported, nothing reused for
+training, human review required.

docs/operating-model-github-hf-wandb.md

@@ -0,0 +1,13 @@
+# Operating model: GitHub / Hugging Face / W&B (public summary)
+
+- **GitHub** — open-core split: SDK contracts, formal track, examples,
+  evidence, and docs are public; scenario generation, contamination
+  firewall, anti-hack engine, platform, and all runs/data are private.
+- **Hugging Face** — only redacted, license-clean artifacts are ever
+  published, gated by an export-policy check and an explicit approval flag.
+- **Weights & Biases** — dashboards carry sanitized metrics only (no
+  hidden-eval content, no raw traces, no keys), same approval gating.
+
+What is never published anywhere: hidden evaluation content, gold answers,
+anti-hack detection details, private verifier logic, raw or customer
+traces, secrets.

docs/positioning.md

@@ -19,9 +19,9 @@ feedback substrate.
 
 ## Claims we do not make
 
-We do not claim to build, solve, or prove AGI; to guarantee general
-intelligence; to have a "formally verified system/product/API/code"; to
-prove that a model generalizes; or to eliminate contamination. The only
-formal claim we make is:
+We do not claim to build, solve, or prove AGI, and we do not claim to
+guarantee general intelligence. We do not claim to have a "formally verified system/product/API/code".
+We never claim to prove that a model generalizes, and we never claim to eliminate contamination.
+The only formal claim we make is:
 
 > Selected mathematical properties behind the contamination-resistant promotion gate are machine-verified in Lean 4. The implementation is property-tested against the formal specification.

docs/sdk-and-cli.md

@@ -0,0 +1,20 @@
+# SDK and CLI (public surface)
+
+## Schemas and config
+
+- `RunConfig` — modes `evaluate_only` (default) / `gate_only` /
+  `improve_and_gate` / `substrate`, privacy-preserving defaults.
+- `EvaluationContract`, `ScoreSet`, `TransferMetrics`, `GateOutcome`,
+  `AssuranceCardV2`, split policy validation.
+- `ModelProvider` interface (`validate_config` / `estimate_cost` / `run` /
+  `dry_run`) with a deterministic `DummyProvider`.
+
+## clean-gate CLI
+
+```bash
+vlabs-prm-eval clean-gate --old baseline.json --new candidate.json
+# exit 0 = ACCEPT, exit 1 = REJECT (reasons printed)
+```
+
+See runnable demos in
+[vlabs-examples](https://github.com/verifiablelabs/vlabs-examples).

scripts/check_docs.py

@@ -0,0 +1,35 @@
+"""CI gate: docs carry only approved claims and no secret-shaped strings."""
+from __future__ import annotations
+
+import re
+import sys
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parents[1]
+SECRET = re.compile(r"sk-or-v1-[A-Za-z0-9]|AKIA[0-9A-Z]{16}|xox[baprs]-")
+FORBIDDEN = re.compile(
+    r"formally verified (system|product|api|code|service)"
+    r"|prove[sd]? that the model generalizes"
+    r"|eliminates? contamination"
+    r"|(build|solve|prove)s? AGI",
+    re.IGNORECASE,
+)
+NEGATION = re.compile(r"do not|never|claims? we do not|not a claim", re.IGNORECASE)
+
+
+def main() -> int:
+    bad: list[str] = []
+    for p in sorted(ROOT.rglob("*.md")):
+        for i, line in enumerate(p.read_text(encoding="utf-8").splitlines(), 1):
+            if SECRET.search(line):
+                bad.append(f"{p}:{i}: secret-shaped string")
+            if FORBIDDEN.search(line) and not NEGATION.search(line):
+                bad.append(f"{p}:{i}: forbidden claim: {line.strip()[:80]}")
+    for b in bad:
+        print("FAIL:", b)
+    print("OK: docs clean" if not bad else f"{len(bad)} violation(s)")
+    return 1 if bad else 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())