Documentation / Proof Center · AI for Truth-Seeking

EvidenceBound-MAS: contestable verification for AI-generated analysis.

SignalReview treats generated analytical code as untrusted. This public read-only explorer shows how immutable requests, a fail-closed AST boundary, deterministic execution, Z3 obligations, semantic counterexamples and a rooted Proof Pack preserve human review rather than replacing it.

Read-only · No arbitrary uploads · Zero production writes

Human approval required · No automatic promotion

VERIFIED

Bounded obligations completed

Source, IR, concrete result and declared invariant agree for the supported profile.

REFUTED

Counterexample found

A concrete input or execution binding disproves the equivalence or declared invariant.

BLOCKED

Outside the proved profile

Unsupported semantics or deterministic runtime limits stop the claim before PASS.

UNKNOWN

Solver did not finish reliably

A resource-limited solver state remains visibly non-verified and requires escalation.

Truth Boundary Notice

Human review remains strictly mandatory. No candidate bundle is automatically promoted or committed to Git production branches. This replay reflects a verified static ledger and is not presented as live generation.

Domain POC / Sports-algorithm safety

Sports Verification Gateway

Inspect a pinned historical source, an exact candidate, operator-owned invariants, deterministic runtime limits, real counterexamples and downloadable Proof Packs. The gateway verifies the analytical procedure—not a sports result—and preserves human promotion authority.

M00 verifiedM02 counterexampleM03/M04 blockedM05 tamper detection

Open terminal →

Controlled Mutation Corpus

Inject a failure. Watch the evidence boundary move.

The verified baseline is generated by EvidenceBound Core, committed as a public snapshot, and checked for drift in CI. Mutations run only in this browser, perform no server execution, and write no user data.

M01

Math overflow

BLOCKED

Replace a bounded volatility increment with value + 2^63.

M02

Branch drift

REFUTED

Invert strict_bounds so the generated branch no longer matches source semantics.

M03

Scale mismatch

BLOCKED

Change one fixed-point operation from scale 4 to scale 6 without exact conversion.

M04

Fuel exhaustion

BLOCKED

Expand a bounded recalculation beyond the declared deterministic fuel budget.

M05

Output tampering

REFUTED

Change one byte in execution-result.json after a valid run.

M06

Solver resource limit

UNKNOWN

Tighten the declared Z3 time budget until an obligation returns unknown.

Deterministic Body Inspector

Canonical JSON · UTF-8 · sorted keys · no indentation in root calculation

VERIFIEDMATCH

Changed evidence

No mutation — core-generated bindings match

Root transition

f4dbb0fc801f…8871641c → f4dbb0fc801f…8871641c

Committed baseline: f4dbb0fc801f…8871641c · MATCH

{
  "artifact_bindings": {
    "canonical_ast_sha256": "52ad1e7d59b4093e01c93b1c6ea0c0307d0d2cd0c3c4f79af23c3f5bddd24f99",
    "concrete_outputs_sha256": "5b485b6945a96d7f4dfb1703a71273d232bf6c187c0eb3db307e3cf1a6d79469",
    "execution_ir_sha256": "bb1e1bc8998daf6687901ef31b040150abdfd0eef3c0c2256208fe180cb1234d",
    "formal_proof_report_sha256": "c5efa6f8c6ae7266ca58eacb357a8c42224d595ead8c381a918f32a3c39e84ca",
    "semantic_preservation_proof_sha256": "4c290fa4e942570500ff1edcaf30982715930de69778b36ff9c7e1dd65724556",
    "source_binding_proof_sha256": "23384e58acd2b893403507eb7979da070b1a1b6dd02708c537f0c5570f8d7e06",
    "verification_request_sha256": "f763afda2f3a596ba3e78b1116781ced61ed6de522427ff10608a2415c31614f",
    "z3_context_sha256": "7489d48b23782c20eed8da7053c29b3d055a9772c3e9dce6de7d3b37d0db50d7"
  },
  "environment_fingerprint": "135aa0dc6b264cb5c33653df9a0503f47a9eff7a76fddf83a6ed85d78235b403",
  "execution_provenance": {
    "final_verdict": "VERIFIED",
    "runtime_status": "SUCCESS",
    "solver_status": "UNSAT_VERIFIED",
    "source_semantics_verified": true,
    "specification_verified": true
  },
  "safety_contract": {
    "arbitrary_public_code_execution_enabled": false,
    "automatic_promotion_permitted": false,
    "human_approval_required": true
  },
  "schema_version": "evidencebound-manifest/1.0"
}

Manifest binding · execution-result.json

5b485b6945a96d7f4dfb1703a71273d232bf6c187c0eb3db307e3cf1a6d79469

Observed file digest

5b485b6945a96d7f4dfb1703a71273d232bf6c187c0eb3db307e3cf1a6d79469

Evidence interpretation matrix

What each PASS proves—and what it does not.

Evidence	Proves	Does not prove
AST Guard PASS	Static policy satisfied	Logical correctness or production suitability
Deterministic interpreter PASS	Canonical IR completed within declared limits	Real-world truth, usefulness or forecast accuracy
Semantic preservation VERIFIED	Supported source AST and execution IR agree for the declared domain	A universal compiler theorem or correctness of the human specification
SHA-256 Proof Pack	Exact candidate content is immutable and traceable	ROI, certainty, performance or automatic approval
Recorded replay	Repository evidence can be inspected without a fresh call	A new live model invocation occurred

Technical disclaimer and non-claims

Architectural, not commercial verification. VERIFIED means the exact artifacts satisfied the declared bounded obligations. It does not guarantee trading profitability, a sports outcome, financial efficiency, scientific validity or product suitability.

Closed execution context. The proof covers the fixed request, deterministic signed-i64/fixed-point runtime and declared specification. It does not establish the truth or completeness of external data feeds, future provider availability, market liquidity or internet connectivity.

Toolchain-bound reproduction. The deterministic root excludes timestamp and optional signing metadata, but includes an environment fingerprint. A compiler, interpreter, policy or Z3 version change requires a new proof pack rather than silently validating the old environment.

No universal theorem. Phase 5 is per-request symbolic translation validation for the supported scalar profile. Global compiler and interpreter correctness flags remain false.

Proof Pack CLI

cd packages/evidencebound_core
python -m pip install -e .
evidencebound verify examples/verified-request.json --output proof-pack/
evidencebound reproduce proof-pack/
evidencebound reproduce sports-fault-receipt.json

Exact reproduction—including a BLOCKED fault receipt—exits 0. Any artifact-binding mismatch exits 1 with MANIFEST_TAMPERING_DETECTED or reproduction mismatch.

Implementation evidence

Four controls between generated code and a reviewable candidate.

01packages/evidencebound_core/models

Constrained Specification

Accepted constraints restrict the generation scope to deterministic business logic. The system eliminates open-ended agent behavior at the entry contract level.

02packages/evidencebound_core/source

AST Policy Guard

The Abstract Syntax Tree filter executes a fail-closed inspection. It permanently blocks unsafe imports, unauthorized network access, subprocesses, filesystem mutations, and dynamic execution.

03packages/evidencebound_core/execution

Isolated Sandbox Validation

The approved implementation enters a deterministic representation with no candidate-level disk, network, import, subprocess, dynamic-attribute or CPython bytecode capability. Automated fixture-based regression tests compile, lint, and validate the candidate bundle without external dependencies.

04packages/evidencebound_core/proof_pack.py

Immutable Cryptographic Sealing

Successful artifacts and proof reports are content-addressed using SHA-256, generating an unalterable, reproducible engineering receipt whose deterministic root excludes timestamp and optional signing metadata.

EvidenceBound-MAS is an early verification prototype developed inside SignalReview. The public route is a controlled read-only demonstration, not a public arbitrary-code execution service or a certification authority.