{"protocol":"ica-formal-proofs-v1","what":"The machine-checked safety proofs behind ICA. Read the exact TLA+ specifications and re-run them yourself.","engines":{"tool_gateway":"ICAGatewayDecision.tla, ICAGatewayUpgrade.tla, ICAGatewayNonce.tla — the enforcement plane.","relationship_trust":"RelationshipTrust.tla — the metadata-only TrustScore engine (#2)."},"how_to_run":{"tlc":"Fetch the .tla + .cfg files, then: java -cp tla2tools.jar tlc2.TLC -config <spec>-green.cfg <Spec>.tla (TLA+ v1.8.0). Green must verify; each red config must produce a counterexample.","suite":"run.sh runs the whole green/red suite. Every red is a deliberately injected bug the spec must catch.","conformance":"The *-domain.js / *-verify.js harnesses run the REAL running code over the whole finite domain and check its output, and a refinement gate refuses any change that grants authority the certified baseline withheld unless a person acknowledges that exact fingerprint. SECURITY-PROPERTY-CATALOG.md maps each gateway check to the property it covers.","live":"Exercise the running engines with no login: GET https://imperium.aleeth.com/api/ica/relationship-fingerprint/verify (POST your own metadata stream), and the gateway proof at /api/ica/tool-gateway/verify-proof."},"artifacts":[{"file":"ENVIRONMENT-ASSUMPTIONS.md","url":"https://imperium.aleeth.com/api/ica/formal/ENVIRONMENT-ASSUMPTIONS.md","description":null},{"file":"ICAGatewayDecision.tla","url":"https://imperium.aleeth.com/api/ica/formal/ICAGatewayDecision.tla","description":"TLA+ proof of the Tool Gateway deny-by-default decision kernel: revoked/tenant/fail-closed/denylist/consequential invariants over every request."},{"file":"ICAGatewayNonce.tla","url":"https://imperium.aleeth.com/api/ica/formal/ICAGatewayNonce.tla","description":"TLA+ proof that a capability is single-use under concurrency (no replay)."},{"file":"ICAGatewayUpgrade.tla","url":"https://imperium.aleeth.com/api/ica/formal/ICAGatewayUpgrade.tla","description":"TLA+ proof that an upgrade to the gateway can only tighten authority, never silently loosen it (#3)."},{"file":"ICAValueState.tla","url":"https://imperium.aleeth.com/api/ica/formal/ICAValueState.tla","description":null},{"file":"README.md","url":"https://imperium.aleeth.com/api/ica/formal/README.md","description":null},{"file":"RelationshipTrust.tla","url":"https://imperium.aleeth.com/api/ica/formal/RelationshipTrust.tla","description":"TLA+ proof of the Relationship Fingerprint → TrustScore update kernel (#2): spoof ceiling, no trust from untrusted signal, bounded gain, over the whole input domain."},{"file":"SECURITY-PROPERTY-CATALOG.md","url":"https://imperium.aleeth.com/api/ica/formal/SECURITY-PROPERTY-CATALOG.md","description":"Auditor-facing catalog mapping each safety property to its module and the real code it constrains."},{"file":"UCAMissionAuthority.tla","url":"https://imperium.aleeth.com/api/ica/formal/UCAMissionAuthority.tla","description":null},{"file":"decision-green.cfg","url":"https://imperium.aleeth.com/api/ica/formal/decision-green.cfg","description":null},{"file":"decision-red-consequential.cfg","url":"https://imperium.aleeth.com/api/ica/formal/decision-red-consequential.cfg","description":null},{"file":"decision-red-contract.cfg","url":"https://imperium.aleeth.com/api/ica/formal/decision-red-contract.cfg","description":null},{"file":"decision-red-revoked.cfg","url":"https://imperium.aleeth.com/api/ica/formal/decision-red-revoked.cfg","description":null},{"file":"decision-red-tenant.cfg","url":"https://imperium.aleeth.com/api/ica/formal/decision-red-tenant.cfg","description":null},{"file":"decision-red-untrusted.cfg","url":"https://imperium.aleeth.com/api/ica/formal/decision-red-untrusted.cfg","description":null},{"file":"fingerprint-baseline.json","url":"https://imperium.aleeth.com/api/ica/formal/fingerprint-baseline.json","description":null},{"file":"fingerprint-baseline.vector","url":"https://imperium.aleeth.com/api/ica/formal/fingerprint-baseline.vector","description":null},{"file":"fingerprint-domain.js","url":"https://imperium.aleeth.com/api/ica/formal/fingerprint-domain.js","description":"Conformance oracle: runs the REAL TrustScore engine over the whole domain and checks the proven invariants on its output."},{"file":"fingerprint-verify.js","url":"https://imperium.aleeth.com/api/ica/formal/fingerprint-verify.js","description":"Deploy gate for the TrustScore engine: oracle + adversarial harness + teeth check + refinement gate."},{"file":"gateway-baseline.json","url":"https://imperium.aleeth.com/api/ica/formal/gateway-baseline.json","description":null},{"file":"gateway-baseline.vector","url":"https://imperium.aleeth.com/api/ica/formal/gateway-baseline.vector","description":null},{"file":"gateway-domain.js","url":"https://imperium.aleeth.com/api/ica/formal/gateway-domain.js","description":"Conformance oracle: runs the REAL gateway decide() over the whole domain and holds every output to its checks; SECURITY-PROPERTY-CATALOG.md maps each check to the property it covers."},{"file":"gateway-verify.js","url":"https://imperium.aleeth.com/api/ica/formal/gateway-verify.js","description":"Deploy gate for the gateway: oracle + invariant-preserving-upgrade refinement gate."},{"file":"nonce-green.cfg","url":"https://imperium.aleeth.com/api/ica/formal/nonce-green.cfg","description":null},{"file":"nonce-red.cfg","url":"https://imperium.aleeth.com/api/ica/formal/nonce-red.cfg","description":null},{"file":"run.sh","url":"https://imperium.aleeth.com/api/ica/formal/run.sh","description":"The runner: every GREEN spec must verify, every RED twin (an injected bug) must be caught. CI runs this on every change."},{"file":"trust-green.cfg","url":"https://imperium.aleeth.com/api/ica/formal/trust-green.cfg","description":null},{"file":"trust-red-ceiling.cfg","url":"https://imperium.aleeth.com/api/ica/formal/trust-red-ceiling.cfg","description":null},{"file":"trust-red-gain.cfg","url":"https://imperium.aleeth.com/api/ica/formal/trust-red-gain.cfg","description":null},{"file":"trust-red-untrusted.cfg","url":"https://imperium.aleeth.com/api/ica/formal/trust-red-untrusted.cfg","description":null},{"file":"uca-mission-green.cfg","url":"https://imperium.aleeth.com/api/ica/formal/uca-mission-green.cfg","description":null},{"file":"uca-mission-red-auto-expand.cfg","url":"https://imperium.aleeth.com/api/ica/formal/uca-mission-red-auto-expand.cfg","description":null},{"file":"uca-mission-red-no-revoke-check.cfg","url":"https://imperium.aleeth.com/api/ica/formal/uca-mission-red-no-revoke-check.cfg","description":null},{"file":"uca-mission-red-self-approve.cfg","url":"https://imperium.aleeth.com/api/ica/formal/uca-mission-red-self-approve.cfg","description":null},{"file":"uca-mission-red-stale-token.cfg","url":"https://imperium.aleeth.com/api/ica/formal/uca-mission-red-stale-token.cfg","description":null},{"file":"upgrade-green-none.cfg","url":"https://imperium.aleeth.com/api/ica/formal/upgrade-green-none.cfg","description":null},{"file":"upgrade-green-tighten.cfg","url":"https://imperium.aleeth.com/api/ica/formal/upgrade-green-tighten.cfg","description":null},{"file":"upgrade-red-revoked.cfg","url":"https://imperium.aleeth.com/api/ica/formal/upgrade-red-revoked.cfg","description":null},{"file":"upgrade-red-tenant.cfg","url":"https://imperium.aleeth.com/api/ica/formal/upgrade-red-tenant.cfg","description":null},{"file":"value-state-green.cfg","url":"https://imperium.aleeth.com/api/ica/formal/value-state-green.cfg","description":null},{"file":"value-state-red-skip.cfg","url":"https://imperium.aleeth.com/api/ica/formal/value-state-red-skip.cfg","description":null},{"file":"verify-decision-proof.js","url":"https://imperium.aleeth.com/api/ica/formal/verify-decision-proof.js","description":null}],"generated_at":"2026-10-05T19:37:39.349Z"}