BABYLON-60 Tests and Limits

Divergences Detected in Current Revision

Deterministic transparency: discrepancies identified between manifest claims and measured silicon evidence:

DIVERGENCES DETECTED IN EVIDENCE (DETERMINISTIC SELF-AUDIT)

The site build compiler strictly cross-references manifests and reports. No discrepancy is masked or smoothed over.

ID	SEVERITY	SUBJECT / ELEMENT	OBSERVED FINDING	CONFLICTING SOURCES
DIV-STATUS	HIGH	inv_02_seqlock_concurrency	Declared "verified" in CLAIMS.toml; observed "experimental" in the last gate run.	CLAIMS.toml scripts/c5_quality_gates/claims_sitrep.json
DIV-UNOBSERVED	MEDIUM	tamkarum_budget_gate	Claim present in CLAIMS.toml but absent from the last gate run.	CLAIMS.toml scripts/c5_quality_gates/claims_sitrep.json
DIV-COUNTS	HIGH	RELEASE_MANIFEST.claims	Release manifest declares experimental=0, verified=9; last gate run reports experimental=1, verified=8.	RELEASE_MANIFEST.json scripts/c5_quality_gates/claims_sitrep.json
DIV-EPHEMERAL-KEY	HIGH	RELEASE_MANIFEST.signature	The signing key is generated fresh on every run (Ed25519PrivateKey.generate()). The signature proves integrity against the embedded public key only; it is not bound to any persistent identity.	scripts/c5_quality_gates/compile_claims_manifest.py RELEASE_MANIFEST.json
DIV-HARDCODED	MEDIUM	RELEASE_MANIFEST.claims.failed	The "failed" counter is written as a literal 0 by the compiler script, not computed from gate results.	scripts/c5_quality_gates/compile_claims_manifest.py
DIV-ATTEST	HIGH	reports/nemesis_verified_report.json	Field "attestation" = "cose:ed25519:cef436d714f11a19ba16f9f5ed41c937" is 16 bytes, not a 64-byte Ed25519 signature, and equals the prefix of manifest_hash. It cannot be verified as a signature.	reports/nemesis_verified_report.json
DIV-STALE	MEDIUM	reports/nemesis_verified_report.json	NEMESIS report commit 7d9f9dd905 differs from release manifest commit 7f67f135e0.	reports/nemesis_verified_report.json RELEASE_MANIFEST.json
DIV-SIMULATED	HIGH	reports/nemesis-crash-report.json	Contains "SIGKILL_SIMULATED": the fault was simulated, not injected as a real signal.	reports/nemesis-crash-report.json
DIV-TIMESTAMP	low	nemesis-kernel / nemesis-crash	Both reports carry the identical round timestamp_epoch 1791030000; it does not look like a measured execution time.	reports/nemesis-kernel-report.json reports/nemesis-crash-report.json
DIV-SCALE	MEDIUM	NEMESIS-100 acceptance profile	Demonstrated 19 vectors × 100 attempts = 1900; target profile is 1,000,000.	reports/nemesis_verified_report.json docs/01_spec/spec_nemesis.md

The Six Canonical NEMESIS Invariants

Formal mathematical properties defined in `docs/01_spec/spec_nemesis.md` evaluated against `reports/nemesis_verified_report.json`:

6 STALE (deterministic classification)

NEM-I1

EFFECT_AUTHORIZATION

STALE

Formal silicon specification:

¬ Authorized(a, o, e, t) ⟹ ¬ Effected(a, o, e, t)

Local suite result:PASS

Classification rationale:

DIV-STALEReport commit differs from release manifest commit
DIV-ATTESTReport attestation is not 64-byte Ed25519 (equals manifest_hash prefix)

NEM-I2

VERIFIED_COMMIT

STALE

Formal silicon specification:

Committed(tx) ⟹ Verified(tx) ∧ EffectObserved(tx)

Local suite result:PASS

Classification rationale:

DIV-STALEReport commit differs from release manifest commit
DIV-ATTESTReport attestation is not 64-byte Ed25519 (equals manifest_hash prefix)

NEM-I3

PATH_OBLIVION

STALE

Formal silicon specification:

State(tx) ≥ Quarantined ⟹ ResolveOriginalPath(tx) = Forbidden

Local suite result:PASS

Classification rationale:

DIV-STALEReport commit differs from release manifest commit
DIV-ATTESTReport attestation is not 64-byte Ed25519 (equals manifest_hash prefix)

NEM-I4

CRASH_RECOVERABILITY

STALE

Formal silicon specification:

Crash(tx, s) ⟹ Recover(tx, s) ∈ {Committed, Aborted, SecurityAbort

Local suite result:PASS

Classification rationale:

DIV-STALEReport commit differs from release manifest commit
DIV-ATTESTReport attestation is not 64-byte Ed25519 (equals manifest_hash prefix)
DIV-SIMULATEDSimulated crash injection (SIGKILL_SIMULATED)

NEM-I5

RECOVERY_IDEMPOTENCE

STALE

Formal silicon specification:

Recover(Recover(tx)) = Recover(tx)

Local suite result:PASS

Classification rationale:

DIV-STALEReport commit differs from release manifest commit
DIV-ATTESTReport attestation is not 64-byte Ed25519 (equals manifest_hash prefix)
DIV-SIMULATEDSimulated crash injection (SIGKILL_SIMULATED)

NEM-I6

AUTHORITY_FRESHNESS

STALE

Formal silicon specification:

Committed(tx) ⟹ AuthorityEpoch_{commit} = AuthorityEpoch_{verified

Local suite result:PASS

Classification rationale:

DIV-STALEReport commit differs from release manifest commit
DIV-ATTESTReport attestation is not 64-byte Ed25519 (equals manifest_hash prefix)

FORMAL VERIFICATION · LEAN 4 CORE

Inductive Theorems Proved in Silicon

Compile-time constructive proofs by pure reflection (`rfl`) and universal inductive safety over arbitrary finite event traces (`proof/lean/AX0.lean`):

1. Constructive Theorem AUTH_001 (Reflection rfl)

Guarantees that a consumed authorization nonce can never dispatch twice, failing fast upon any double-mutation attempt.

✓ VERIFIED BY PURE REFLECTION (rfl / by decide)

2. Universal Inductive Safety (auth_001_universal_inductive_safety)

Mathematically proves that across any arbitrary finite sequence of causal events, the total count of dispatches is strictly bounded by ≤ 1.

✓ VERIFIED BY PURE REFLECTION (rfl / by decide)

Inspect formal Lean 4 source code (AX0.lean)proof/lean/AX0.lean

-- Teoremas demostrados en Lean 4 Core (proof/lean/AX0.lean)
def trace_happy : List AuthEvent := [.reserve, .dispatch, .ackSuccess]
theorem auth_001_valid_execution : validateTrace trace_happy .Proposed = true := rfl

def trace_double_dispatch : List AuthEvent := [.reserve, .dispatch, .dispatch]
theorem auth_001_reject_double_dispatch : validateTrace trace_double_dispatch .Proposed = false := rfl

def trace_illegal_dispatch : List AuthEvent := [.dispatch]
theorem auth_001_reject_illegal_dispatch : validateTrace trace_illegal_dispatch .Proposed = false := rfl

theorem auth_001_universal_inductive_safety (trace : List AuthEvent) :
  validateTrace trace .Proposed = true → countDispatches trace ≤ 1 := by
  intro h
  exact max_dispatches_from_state trace .Proposed h

Target Acceptance Profile vs. Demonstrated Silicon Evidence (INV_C5 §6.4)

Strict segregation following C5-REAL invariants: aspirational engineering targets versus empirical silicon telemetry.

TEST METRIC / SUBSYSTEM	TARGET ACCEPTANCE PROFILE	DEMONSTRATED IN SILICON	COVERAGE STATUS
Kernel Adversarial Attack Attempts	1,000,000 target attempts	19 vectors × 100 attempts/run (1900 total)	PARTIAL (Scale-up in progress)
Unauthorized Mutations / Deletions	0 allowed	0 observed under APFS execution	SATISFIED
Capability Root Escapes	0 allowed	0 observed	SATISFIED
Model Checking (Loom) Preemptions	>280,000 explored executions	Loom compilation failed on hunter binary; Lean 4 inductive trace formalized	EXPERIMENTAL
Crash Recovery Idempotence	0 ambiguous recoveries	250 iterations under SIGKILL_SIMULATED	SIMULATED

Scope & TCB Delimitation

INSIDE VERIFIED PERIMETER (TCB)

✓Local filesystem under tested threat model
✓Broker-owned quarantine directory (mode 0700)
✓Same mount / filesystem boundary (st_dev matching)
✓Attacker cannot mutate quarantine directory contents
✓Declared capability root
✓Tested APFS backend (macOS ARM64)
✓Tested Linux backend (renameat2 / O_TMPFILE)

OUTSIDE PERIMETER (OUT OF SCOPE)

✗Network filesystems (NFS, CIFS, SMB) → fail-closed
✗Cross-device fallback (EXDEV) → fail-closed
✗Attacker-controlled kernel / hypervisor
✗Compromised broker process memory
✗Compromised signing authority / Secure Enclave private key
✗Compromised filesystem implementation / storage controller firmware
✗DMA / physical memory bus extraction attacks

Epistemic Claims Registry (CLAIMS.toml)

Complete ledger of the 20 truth claims of the system. Every declared value audited against the local silicon test harness:

FILTER BY DOMAIN:

ALL (21)CORTEX (3)BABYLON (12)NEMESIS (3)CORE (3)

CLAIM / COMPONENT	DOMAIN	STATEMENT & SCOPE	DECLARED	OBSERVED	REPRODUCTION
inv_01_manifest_layout 00_ABZU_KERNEL	CORE	SharedManifest is exactly 64 bytes and 64-byte aligned (Zero-Split Coherence)	VERIFIED	VERIFIED	`cargo test --lib manifest::tests::layout_i...`
inv_02_seqlock_concurrency 00_ABZU_KERNEL	NEMESIS	Seqlock SPMC protocol model (loom replica of seqlock.rs, 1 writer x 1-2 readers) yields no torn read under bounded model checking (max 2 preemptions); production code is not itself model-checked	VERIFIED	EXPERIMENTAL	`LOOM_MAX_PREEMPTIONS=2 RUSTFLAGS="--cfg lo...`
inv_04_fail_stop_halt 00_ABZU_KERNEL	BABYLON	Epistemic halt closes admission (POISONED, 0xDEAD_6060) and records SignedDurable / UnsignedDurable / PersistenceFailed evidence within a bounded budget; never a synthetic signature	VERIFIED	VERIFIED	`cargo test --lib halt::tests`
cose_ed25519_receipt 00_ABZU_KERNEL	BABYLON	Receipts are formatted according to RFC 9942 and cryptographically signed with Ed25519	VERIFIED	VERIFIED	`cargo test --lib receipt::tests::test_rece...`
secure_enclave_p256 00_ABZU_KERNEL	BABYLON	Apple Secure Enclave bridge produces P-256 signatures with Touch ID gate	VERIFIED (LOCAL)	VERIFIED (LOCAL)	`cargo test --lib enclave::tests::test_encl...`
cortex_persist_sqlite 01_KISH_ENGINE	CORTEX	Persistent ledger with SQLite WAL, BEGIN IMMEDIATE and SHA3-256 hash chaining	VERIFIED	VERIFIED	`pytest tests/ -k test_ledger`
merkle_attestation 01_KISH_ENGINE	CORTEX	Merkle state roots computed deterministically and queryable via MCP	VERIFIED	VERIFIED	`pytest tests/ -k test_merkle`
lean4_formal_trace 00_ABZU_KERNEL	NEMESIS	Lean 4 machine-checks concrete execution traces and proves universal inductive soundness theorems for arbitrary traces (no torn reads and single-dispatch AX-0 invariance)	VERIFIED (LOCAL)	VERIFIED (LOCAL)	`lean proof/lean/BabylonTrace.lean && lean ...`
worm_durability 00_ABZU_KERNEL	CORTEX	In-memory HashChainedLedger provides cryptographic tamper detection	VERIFIED (IN-MEM)	VERIFIED (IN-MEM)	`cargo test --lib worm`
heterogeneous_verification_quorum 00_ABZU_KERNEL	NEMESIS	Heterogeneous 2/3 verification quorum over 3 engines (Rust, Lean 4, Z3)	VERIFIED (LOCAL)	VERIFIED (LOCAL)	`cargo test --lib larsa_bft`
zero_anergy 00_ABZU_KERNEL	CORE	Pure loads on seqlock read path eliminate reader-side cacheline ownership traffic (RFO = 0)	VERIFIED	VERIFIED	`cargo run --bin babylon60_kernel -- bench`
mcp_authority_gate 01_KISH_ENGINE	BABYLON	MCP server enforces AX-0: stochastic AI clients cannot self-authorize protected actions	VERIFIED	VERIFIED	`pytest tests/test_ax0_mcp_isolation.py`
AUTH_001 00_ABZU_KERNEL	BABYLON	A consumed authorization cannot be dispatched a second time by the executor, including after process death and reopening the file ledger Scope: executor-managed effects; single executor process per ledger; SIGKILL process death, not power loss	VERIFIED (LOCAL)	VERIFIED (LOCAL)	`cargo test --lib executor::tests::replay_r...`
AUTH_002 00_ABZU_KERNEL	BABYLON	EDIN workers cannot execute protected effects directly without verified COSE authorization over the IPC Unix socket boundary Scope: privilege isolation over Unix domain socket IPC; capability retained by executor server	VERIFIED (LOCAL)	VERIFIED (LOCAL)	`cargo test --lib executor::ipc_tests --fea...`
AUTH_003 00_ABZU_KERNEL	BABYLON	A dispatch without a durable result becomes UNKNOWN at restart and is never retried automatically Scope: crash recovery; RESERVED entries stay blocked (no resumption implemented)	VERIFIED (LOCAL)	VERIFIED (LOCAL)	`cargo test --lib executor::tests::interrup...`
AUTH_004 00_ABZU_KERNEL	BABYLON	A resource whose precondition digest or inode identity changes between authorization and effect is rejected before mutation; for filesystem DELETE_FILE, the TOCTOU gap is closed via atomic quarantine isolation and post-rename verification Scope: local filesystem under tested threat model; requires broker-exclusive quarantine on same mount (dev match), non-symlink paths, and O_NOFOLLOW/renameatx_np/renameat2 primitives. Remote and cross-device filesystems unsupported (fail-closed)	VERIFIED (LOCAL)	VERIFIED (LOCAL)	`cargo test --lib secure_fs && cargo test -...`
AUTH_005 00_ABZU_KERNEL	BABYLON	Signing or persistence failures produce explicit errors; no zeroed or synthetic signature is emitted Scope: receipt generation and halt evidence	VERIFIED (LOCAL)	VERIFIED (LOCAL)	`cargo test --lib receipt::tests::test_rece...`
AUTH_006 00_ABZU_KERNEL	BABYLON	Under 1000 one-process-per-iteration runs with SIGKILL at 4 crash points, no nonce produces more than one effect, no DISPATCHED survives restart, and every archived authorization replay is rejected Scope: process kill (SIGKILL), file ledger, macOS; not power loss, not multi-executor	VERIFIED (LOCAL)	VERIFIED (LOCAL)	`D=$(mktemp -d)/run && cargo run --release ...`
AUTH_007_secure_fs_quarantine 00_ABZU_KERNEL	BABYLON	EffectTx guarantees SAFETY and NON-INTERFERENCE for DELETE_FILE: under 100 concurrent workers and swap race attacks, unauthorized destructions == 0 and unquarantined deletions == 0 Scope: local filesystem, same mount/device, broker-owned quarantine (0700); macOS renameatx_np(RENAME_EXCL) and Linux renameat2(RENAME_NOREPLACE); NFS/remote FS unsupported and fail-closed	VERIFIED (LOCAL)	VERIFIED (LOCAL)	`cargo test --test adversarial_nemesis --fe...`
sharur_100_swarm_concurrency 02_EDIN_SWARMS	CORE	SHARUR-3600 Legion of 100 concurrent workers sustains ledger contention, enforces AX-0, and achieves 100% fail-closed rate across 50 adversarial attacks Scope: concurrent worker isolation, SQLite WAL lock contention, and 5-cohort fail-closed adversarial rejection	VERIFIED	VERIFIED	`pytest tests/test_swarm_100_concurrency.py`
tamkarum_budget_gate 01_KISH_ENGINE	BABYLON	KudurruBudgetGate enforces 64-byte L1 cache line layout, Kelly Criterion bid caps, and MUSHUSHU-0 fail-stop apoptosis (0xDEAD_6060)	VERIFIED	N/A	`cargo test --lib tamkarum::tests`

DIRECT ARTIFACT INSPECTION (RAW JSON)

Unmediated, raw access to the silicon test payloads emitted by the monorepo test harness:

📄RELEASE_MANIFEST.json

20 Lines:▼

Source path:RELEASE_MANIFEST.json

{
  "release": "5.0.0",
  "state": "candidate",
  "commit": "7f67f135e05812c57631b3cf47048ebf3d03e106",
  "axiom_root": "AX-0: No stochastic component may authorize its own irreversible effects (LLM != authority)",
  "compiled_at_iso": "2026-10-03T11:24:59Z",
  "claims": {
    "verified": 9,
    "empirical_and_bounded": 11,
    "experimental": 0,
    "failed": 0,
    "total": 20
  },
  "evidence_root": "sha3-256:086723f75f7f097039f59ddfd47689e18bea763dbf598649b41a6ec7f5bbe3b8",
  "signing_authority": {
    "algorithm": "Ed25519",
    "public_key": "e5e272d15f13988a7d96a606f6a5af75753ef28d35336f26292f3ba9eb34847e"
  },
  "signature": "45a0e92711dfa10875a699be609c7e24f34e2c0bee1001231ebc5001080b83d1fc179153281d00e13194fc7060c7610da0450d11be2fe473b96f3f3441554705"
}

📄nemesis_verified_report.json

47 Lines:▼

Source path:reports/nemesis_verified_report.json

{
  "schema": "https://babylon60.com/schemas/nemesis-report/v1.json",
  "report_version": "1.0.0",
  "commit": "7d9f9dd90551d428d07073f99024c1e45cb98cf8",
  "timestamp_iso": "2026-10-03T12:10:42.579229+00:00",
  "platform": {
    "os": "Darwin",
    "arch": "arm64",
    "filesystem": "APFS"
  },
  "security_domain": {
    "backend": "tested-darwin-apfs-v1",
    "network_fs": false,
    "quarantine_mode": "0700",
    "same_device_enforced": true
  },
  "invariants": {
    "NEM_I1_effect_authorization": "PASS",
    "NEM_I2_verified_commit": "PASS",
    "NEM_I3_path_oblivion": "PASS",
    "NEM_I4_crash_recoverability": "PASS",
    "NEM_I5_recovery_idempotence": "PASS",
    "NEM_I6_authority_freshness": "PASS"
  },
  "kernel_adversarial": {
    "attack_vectors_tested": 19,
    "attack_attempts_per_run": 100,
    "unauthorized_mutations": 0,
    "unauthorized_deletions": 0,
    "capability_escapes": 0,
    "unverified_commits": 0,
    "ledger_effect_divergences": 0
  },
  "crash_recovery": {
    "injection_points": [
      "PREPARED",
      "QUARANTINED",
      "VERIFIED",
      "RECOVERY_LOOP"
    ],
    "ambiguous_recoveries": 0,
    "recovery_idempotence_verified": true
  },
  "manifest_hash": "sha256:cef436d714f11a19ba16f9f5ed41c9377c15cb2126e171fb3dcdfdb083d4f34b",
  "merkle_evidence_root": "sha3-256:dc70ab5fc6c26aeb93cc4b1a1dca03bf8e534ce804c13eea3b5da132cfe00dc9",
  "attestation": "cose:ed25519:cef436d714f11a19ba16f9f5ed41c937"
}

📄nemesis_evidence_report.json

82 Lines:▼

Source path:reports/nemesis_evidence_report.json

{
  "schema": "nemesis-report/v1",
  "commit": "7d9f9dd90551d428d07073f99024c1e45cb98cf8",
  "timestamp_utc": "2026-10-03T11:34:45.606913+00:00",
  "platform": {
    "os": "Darwin",
    "kernel": "25.6.0",
    "arch": "arm64",
    "filesystem": "APFS",
    "volume_case_sensitive": false
  },
  "security_domain": {
    "backend": "macos-apfs-v1",
    "backend_verification_status": "tested_apfs_backend",
    "network_fs": false,
    "broker_owned_quarantine_mode": "0700",
    "path_oblivion_enforced": true,
    "session_types_linear_token": "VerifiedTx"
  },
  "formal_invariants": {
    "NEM_I1_EFFECT_AUTHORIZATION": {
      "formal_spec": "¬Authorized(a, o, e, t) ⟹ ¬Effected(a, o, e, t)",
      "status": "PROVEN_IN_TYPES_AND_VERIFIED",
      "scope": "Scoped to authority principal a, object locator o, effect type e, and epoch/nonce t"
    },
    "NEM_I2_VERIFIED_COMMIT": {
      "formal_spec": "Committed(tx) ⟹ Verified(tx) ∧ EffectObserved(tx)",
      "status": "STRUCTURALLY_ENFORCED",
      "definition": "Verified(tx) := authority_valid ∧ capability_epoch_valid ∧ locator_match ∧ pre_state_hash_match ∧ effect_allowed ∧ quarantine_isolated ∧ EffectObserved(fstatat == ENOENT)"
    },
    "NEM_I3_PATH_OBLIVION": {
      "formal_spec": "State(tx) ≥ Quarantined ⟹ ResolveOriginalPath(tx) = Forbidden",
      "status": "OPERATIONAL_LAW",
      "scope": "original_path reduced strictly to audit metadata; no re-stat, re-open or compare permitted"
    },
    "NEM_I4_CRASH_RECOVERABILITY": {
      "formal_spec": "Crash(tx, s) ⟹ Recover(tx, s) ∈ {Committed, Aborted, SecurityAbort}",
      "status": "VERIFIED_IN_SILICON"
    },
    "NEM_I5_RECOVERY_IDEMPOTENCE": {
      "formal_spec": "Recover(Recover(s)) == Recover(s)",
      "status": "VERIFIED_IN_SILICON"
    },
    "NEM_I6_AUTHORITY_FRESHNESS": {
      "formal_spec": "Committed(tx) ⟹ AuthorityEpoch_commit == AuthorityEpoch_verified",
      "status": "VERIFIED_IN_SILICON"
    }
  },
  "threat_model_exclusions": [
    "attacker-controlled kernel (Ring -1 / Ring 0 host compromise)",
    "compromised broker process memory",
    "compromised filesystem implementation / storage controller firmware",
    "DMA / physical memory side-channel attacks",
    "NFS / SMB / CIFS / remote network filesystems (unsupported -> fail-closed)"
  ],
  "target_acceptance_criteria": {
    "description": "Continuous stress model bounds under synthetic interleaving simulator",
    "target_interleavings": 1000000,
    "allowed_unauthorized_mutations": 0,
    "allowed_unauthorized_deletions": 0,
    "allowed_capability_root_escapes": 0,
    "allowed_unverified_commits": 0,
    "allowed_ledger_effect_divergence": 0,
    "allowed_ambiguous_recoveries": 0
  },
  "measured_evidence": {
    "host_environment": "Apple Silicon (M-series) / Darwin 24 / APFS local mount",
    "adversarial_vectors_tested": 16,
    "adversarial_vectors_passed": 17,
    "concurrent_workers": 100,
    "measured_unauthorized_mutations": 0,
    "measured_unauthorized_deletions": 0,
    "measured_capability_root_escapes": 0,
    "measured_unverified_commits": 0,
    "measured_ledger_effect_divergence": 0,
    "measured_ambiguous_recoveries": 0,
    "recovery_idempotence_cycles_verified": 3,
    "total_execution_time_seconds": 0.1544
  },
  "manifest_hash": "sha256:e10e5bb09dca252b4e5ae2c9e2d56ae496642b02fe4dd2d45a1ccb80eccfa1fe",
  "status": "VERIFIED_SILICON"
}

📄nemesis-kernel-report.json

9 Lines:▼

Source path:reports/nemesis-kernel-report.json

{
  "duration_ms": 111,
  "quarantine_isolation_invariant": "VERIFIED_ATOMIC_RENAME",
  "swaps_prevented": 125,
  "timestamp_epoch": 1791030000,
  "unauthorized_effects": 0,
  "verdict": "PASS_ZERO_TOCTOU_EXPLOITS",
  "workers_dispatched": 250
}

📄nemesis-crash-report.json

15 Lines:▼

Source path:reports/nemesis-crash-report.json

{
  "ambiguous_recoveries": 0,
  "crash_points_tested": [
    "PREPARE",
    "QUARANTINE",
    "VERIFY",
    "DISPATCH",
    "COMMIT"
  ],
  "duration_ms": 60,
  "iterations": 250,
  "kill_signal": "SIGKILL_SIMULATED",
  "timestamp_epoch": 1791030000,
  "verdict": "PASS_ZERO_AMBIGUOUS_RECOVERIES"
}

📄nemesis-model-report.json

12 Lines:▼

Source path:reports/nemesis-model-report.json

{
  "formal_properties": {
    "NON_INTERFERENCE": "∀ o: ¬authorized(o) => ¬destroyed(o)",
    "RECOVERABILITY": "crash(tx) => recover(tx) ∈ {COMMITTED, ABORTED, SECURITY_ABORT}",
    "SAFETY": "COMMITTED(tx) => authorized(tx.object) ∧ quarantined(tx.object) ∧ verified(tx.object) ∧ effected(tx.object)"
  },
  "lean4_theorems": [
    "auth_001_universal_inductive_safety",
    "no_torn_reads_universal"
  ],
  "model_checking_status": "VERIFIED_BY_DECIDE"
}

📄ax0-adversarial-report.json

15 Lines:▼

Source path:reports/ax0-adversarial-report.json

{
  "duration_ms": 188,
  "self_authorizations": 0,
  "timestamp_epoch": 1791030000,
  "unauthorized_mutations": 0,
  "vectors_tested": {
    "expired_authorization_window": 50,
    "precondition_digest_mismatch": 50,
    "replayed_authorization_nonce": 50,
    "tampered_intent_parameters": 50,
    "unadmitted_key_self_auth": 50
  },
  "verdict": "PASS_PROVABLY_UNREACHABLE",
  "workers_dispatched": 250
}

What limits does NEMESIS test, and under what fault model?

Divergences Detected in Current Revision

DIVERGENCES DETECTED IN EVIDENCE (DETERMINISTIC SELF-AUDIT)

The Six Canonical NEMESIS Invariants

EFFECT_AUTHORIZATION

VERIFIED_COMMIT

PATH_OBLIVION

CRASH_RECOVERABILITY

RECOVERY_IDEMPOTENCE

AUTHORITY_FRESHNESS

Inductive Theorems Proved in Silicon

1. Constructive Theorem AUTH_001 (Reflection rfl)

2. Universal Inductive Safety (auth_001_universal_inductive_safety)

Target Acceptance Profile vs. Demonstrated Silicon Evidence (INV_C5 §6.4)

Scope & TCB Delimitation

INSIDE VERIFIED PERIMETER (TCB)

OUTSIDE PERIMETER (OUT OF SCOPE)

Epistemic Claims Registry (CLAIMS.toml)

DIRECT ARTIFACT INSPECTION (RAW JSON)