This repository fixes a public, anonymously authored snapshot of:
EffectIR: Translation-Validated Effect Refinement for Untrusted Agent Runtimes
It contains the paper PDF, the authors' Lean and integration sources, frozen experimental records, integrity manifests, and an RFC 3161 timestamp token.
paper/EffectIR-anonymous.pdf— metadata-sanitized paper.artifact/— Lean formalization, boundary probes, independent validators, and frozen evidence.RELEASE-MANIFEST.sha256— byte-level inventory of the public release.timestamp/— RFC 3161 request, response, certificate chain, and verifier.VERIFY.ps1— release and artifact integrity checks for Windows PowerShell.
From PowerShell at the repository root:
.\VERIFY.ps1For the strongest independent protocol replay included here, install the one Python dependency and run the ordinary and optimized interpreters:
python -m pip install -r artifact\requirements.txt
Push-Location artifact
python tests\fixtures\effectir_independent_correlation_v2_result_validator.py formal\results\effectir-independent-correlation-v2-2026-08-27.json
python -O tests\fixtures\effectir_independent_correlation_v2_result_validator.py formal\results\effectir-independent-correlation-v2-2026-08-27.json
Pop-LocationThe Lean package is self-contained apart from the version pinned in
artifact/formal/lean/lean-toolchain:
Set-Location artifact\formal\lean
lake buildThis snapshot deliberately excludes third-party OpenClaw and SDK source trees, package archives, private keys, and private authorship claims. The frozen OpenClaw capture identifies the tested upstream version and source hashes, while the public package contains only the authors' lowering capture, boundary code, validators, and evidence. Obtain any third-party source independently under its own license if a source-level reconstruction is desired.
Four frozen result JSON files contained machine-local absolute paths. Their
portable public forms replace only those path strings; artifact/REDACTIONS.json
records both the original and public SHA-256 hashes. No semantic result field was
changed.
The public repository establishes a stable public object. A separate authorship claim, signed by the controlling private key, is intentionally not included.