# IHVRK: Independent Human Verification Resource Kit

**What it does.** IHVRK stops an autonomous agent from carrying out a high-impact action until an enrolled human
verifier has approved **that exact action**. The approved action is then allowed to run **once**, and every step
leaves evidence an auditor can check.

**Where the human boundary is.** Between `propose()` (the agent asks) and `ExecutionGate.execute()` (the action
runs). The only thing that crosses it is a single-use permit, issued after a signed approval from an enrolled
verifier key has been bound to the action digest and checked by two independent encodings of the policy.

**How it is enforced.** In the reference deployment, the permit is consumed in one database transaction right
before the operation runs (`ARCHITECTURE.md §4`). On Linux, the agent's cgroup can additionally be frozen while a
request is pending (`runtime/`). An eBPF LSM program that denies connect/exec/write was written and passes the
kernel verifier, but cannot be attached on this host.

**Status at a glance.** These are evidence labels, not marketing:

| Area | Status |
|---|---|
| Canonical encoding, Ed25519 structures, challenge, registry, permits, gate, break-glass, ledger | IMPLEMENTED_AND_TESTED |
| Policy invariants I1–I15 (Z3, with sensitivity and control checks) | FORMALLY_VERIFIED_WITH_STATED_ASSUMPTIONS |
| Protocol safety + liveness (TLA+/TLC, bounded model) | FORMALLY_VERIFIED_WITH_STATED_ASSUMPTIONS |
| cgroup v2 freeze gatekeeper | IMPLEMENTED_AND_TESTED (disposable scopes, this host) |
| eBPF LSM enforcement | IMPLEMENTED_BUT_NOT_FULLY_TESTED: verifier-loaded, attach BLOCKED (host LSM config) |
| eBPF tracepoints | telemetry only (cannot deny) |
| HSM, ML-DSA, hardware attestation, biometrics, DID resolution | NOT_IMPLEMENTED |
| Integration into the live CAIN gateway / MCPGate / the 3 sites | NOT_IMPLEMENTED (plan in `INTEGRATION.md`) |
| Third-party review | none |

Release verdict: see `ASSURANCE_CASE.md` and `release_gate.json`.

## Run it

```bash
# from the repository root; Python 3.10+; pinned deps in ihvrk/requirements.lock
pip install -r ihvrk/requirements.lock
python3 -m pytest -q -p no:cacheprovider ihvrk/tests           # full suite (runtime tests need root + cgroup v2)
python3 -m ihvrk.solver.ihvrk_solver                           # Z3 proofs; exit 0 = all as expected
ihvrk/formal/run_tlc.sh                                        # TLA+ (needs Java + tla2tools.jar, ~25 min)
python3 ihvrk/scripts/mutation_test.py                         # 30 security-guard mutants
python3 ihvrk/scripts/benchmark.py                             # baseline latencies
python3 ihvrk/scripts/generate_evidence.py                     # rebuild ihvrk/evidence/
cd ihvrk/evidence && python3 verify_ihvrk_evidence.py          # stand-alone check of the bundle (stdlib only)
```

## Documents

| File | Contents |
|---|---|
| `THREAT_MODEL.md` | assets, boundaries, attacker, stronger compromises, attack tree, risk register, threat→control→test |
| `SECURITY_INVARIANTS.md` | I1–I15 and TLA+ properties: formal statement, assumptions, guard, code, tests |
| `ARCHITECTURE.md` | components, dependency graph, state machine, sequence, TOCTOU, failure matrix, six-component matrix |
| `ASSURANCE_CASE.md` | claim, argument, evidence, assumptions, release gates, verdict |
| `LIMITATIONS.md` | every known limitation with an ID |
| `FINDINGS.md` | defects found while building this, with fix and regression test |
| `INTEGRATION.md` | Top-100 product mapping, overlap, integration plan, commercial evidence matrix |
| `runtime/README.md` | Linux runtime: cgroups vs namespaces, escape paths, eBPF hook semantics |
| `auditor/` | quickstart, verification steps, expected results, findings template, provenance |
| `schemas/` | JSON Schemas for approval, permit, challenge, decision, ledger record |

## Fixtures

`fixtures/lab.py` builds a complete synthetic deployment. Every key is generated in memory when it runs, and every
identity is invented. The kit contains no production keys, no customer data and no biometric data.