# Provenance of the IHVRK evidence

* Produced by `ihvrk/scripts/generate_evidence.py` at the commit recorded in `MANIFEST.json → source_commit`. The
  manifest also records whether `ihvrk/` had uncommitted changes when the evidence was generated
  (`ihvrk_tree_clean_at_generation`).
* TLC logs come from `ihvrk/formal/run_tlc.sh`, run on 2026-10-12 on the build host (6 vCPU, Linux 7.0.0-38,
  OpenJDK, tla2tools.jar).
* `ebpf_verifier_load.txt` records a kernel-verifier load without attachment, on the same host.
* `benchmark.json` comes from one run on a shared host under load. See its `environment.caveat`.
* MANIFEST.json is **not signed by itself**. Integrity comes from sha256 values, which are tied in turn to the
  signed auditor-kit release that carries this folder (the kit's release signature is made by the owner's key,
  not by the author of this evidence).
* Author: an AI coding session (Claude) working in the CAIN repository on the owner's instruction. No human or
  third-party review has taken place.