hanzoai/bot-formal-models
2
0
Fork 0
mirror of https://github.com/hanzoai/bot-formal-models.git synced 2026-10-30 18:46:45 +00:00
Code Issues Packages Projects Releases Wiki Activity
Files
main
bot-formal-models/tla/models
T
History
vignesh07 859c999492 models: add discord interaction role+thread retry harness
2026-02-03 13:35:09 -08:00
..
approvals_negative_ignore_approval.cfg
tla+: add approval lifecycle gating for nodes.run with counterexample
2026-01-25 13:53:47 -08:00
approvals_ok.cfg
tla+: add approval lifecycle gating for nodes.run with counterexample
2026-01-25 13:53:47 -08:00
approvals_token_negative_replay.cfg
tla+: tokenized approvals to prevent nodes.run replay (with counterexample)
2026-01-25 15:10:39 -08:00
approvals_token_ok.cfg
tla+: tokenized approvals to prevent nodes.run replay (with counterexample)
2026-01-25 15:10:39 -08:00
attacker_negative_nodes_declared_missing.cfg
tla+: extend attacker harness with nodes.run declaredCommands gating
2026-01-25 12:58:25 -08:00
attacker_negative_policy_allows_memory.cfg
tla+: extend attacker harness with nodes.run declaredCommands gating
2026-01-25 12:58:25 -08:00
attacker_nodes_allowlist_negative.cfg
tla+: derive nodes.run gate from gateway allow/deny command policy
2026-01-25 13:00:20 -08:00
attacker_nodes_allowlist_ok.cfg
tla+: derive nodes.run gate from gateway allow/deny command policy
2026-01-25 13:00:20 -08:00
attacker_ok.cfg
tla+: extend attacker harness with nodes.run declaredCommands gating
2026-01-25 12:58:25 -08:00
basic.cfg
tla+: add reproducible TLC model config + core invariants
2026-01-24 20:20:04 -08:00
config_normalization_negative.cfg
models: add config normalization idempotency harness
2026-02-01 01:00:53 -08:00
config_normalization_ok.cfg
models: add config normalization idempotency harness
2026-02-01 01:00:53 -08:00
crash_restart_dedupe_negative.cfg
models: add dedupe collision, crash/restart, concurrency, and conformance harnesses
2026-02-01 10:41:46 -08:00
crash_restart_dedupe_ok.cfg
models: add dedupe collision, crash/restart, concurrency, and conformance harnesses
2026-02-01 10:41:46 -08:00
dedupe_collision_fallback_negative.cfg
models: add dedupe collision, crash/restart, concurrency, and conformance harnesses
2026-02-01 10:41:46 -08:00
dedupe_collision_fallback_ok.cfg
models: add dedupe collision, crash/restart, concurrency, and conformance harnesses
2026-02-01 10:41:46 -08:00
delivery_pipeline_negative.cfg
models: add end-to-end delivery pipeline harness
2026-02-01 01:53:52 -08:00
delivery_pipeline_ok.cfg
models: add end-to-end delivery pipeline harness
2026-02-01 01:53:52 -08:00
delivery_route_stability_negative.cfg
models: add retry route/session stability harness
2026-02-01 01:45:19 -08:00
delivery_route_stability_ok.cfg
models: add retry route/session stability harness
2026-02-01 01:45:19 -08:00
discord_interaction_idempotency_negative.cfg
models: add discord interaction idempotency harness
2026-02-03 13:28:49 -08:00
discord_interaction_idempotency_ok.cfg
models: add discord interaction idempotency harness
2026-02-03 13:28:49 -08:00
discord_interaction_role_thread_negative.cfg
models: add discord interaction role+thread retry harness
2026-02-03 13:35:09 -08:00
discord_interaction_role_thread_ok.cfg
models: add discord interaction role+thread retry harness
2026-02-03 13:35:09 -08:00
discord_pluralkit_negative_webhook.cfg
models: add routing thread parent + discord pluralkit identity harnesses
2026-02-01 00:39:14 -08:00
discord_pluralkit_ok.cfg
models: add routing thread parent + discord pluralkit identity harnesses
2026-02-01 00:39:14 -08:00
discord_role_gating_negative.cfg
models: add discord role gating harness
2026-02-02 12:43:33 -08:00
discord_role_gating_ok.cfg
models: add discord role gating harness
2026-02-02 12:43:33 -08:00
discord_role_gating_thread_parent_negative.cfg
models: add discord role gating thread-parent harness
2026-02-02 13:04:25 -08:00
discord_role_gating_thread_parent_ok.cfg
models: add discord role gating thread-parent harness
2026-02-02 13:04:25 -08:00
discord_shared.cfg
tla+: add scenario model configs (discord shared, dm main)
2026-01-24 20:24:26 -08:00
dm_main.cfg
tla+: add scenario model configs (discord shared, dm main)
2026-01-24 20:24:26 -08:00
elevated_bad_global_only.cfg
tla+: model-check elevated gating requires global+agent
2026-01-24 23:06:13 -08:00
elevated_negative_or_bug.cfg
tla+: model-check elevated gating requires global+agent
2026-01-24 23:06:13 -08:00
elevated_ok.cfg
tla+: model-check elevated gating requires global+agent
2026-01-24 23:06:13 -08:00
gateway_auth_conformance_safe.cfg
tla+: add gateway auth conformance harness (code-shaped)
2026-01-26 09:56:52 -08:00
gateway_auth_conformance_unsafe.cfg
tla+: add gateway auth conformance harness (code-shaped)
2026-01-26 09:56:52 -08:00
gateway_auth_proxy_green.cfg
tla+: add gateway auth trusted-proxy spoof-resistance harness
2026-01-26 13:31:27 -08:00
gateway_auth_proxy_header_spoof_negative.cfg
models: add combined routing tri-rule + proxy header spoof harness
2026-02-01 22:51:56 -08:00
gateway_auth_proxy_header_spoof_ok.cfg
models: add combined routing tri-rule + proxy header spoof harness
2026-02-01 22:51:56 -08:00
gateway_auth_proxy_red.cfg
tla+: add gateway auth trusted-proxy spoof-resistance harness
2026-01-26 13:31:27 -08:00
gateway_auth_tailscale_green.cfg
tla+: add gateway auth tailscale spoof-resistance harness
2026-01-26 13:29:54 -08:00
gateway_auth_tailscale_red.cfg
tla+: add gateway auth tailscale spoof-resistance harness
2026-01-26 13:29:54 -08:00
gateway_exposure_safe.cfg
tla+: add gateway exposure harness (bind beyond loopback + no auth)
2026-01-25 16:40:25 -08:00
gateway_exposure_unsafe.cfg
tla+: add gateway exposure harness (bind beyond loopback + no auth)
2026-01-25 16:40:25 -08:00
gateway_exposure_v2_protected_auto_token_no_creds.cfg
tla+: add gateway bind=auto cases; document gateway exposure matrix
2026-01-26 00:39:32 -08:00
gateway_exposure_v2_protected_custom_token_no_creds.cfg
tla+: expand gateway exposure v2 matrix (custom/tailnet + password)
2026-01-26 00:04:21 -08:00
gateway_exposure_v2_protected_lan_password_no_creds.cfg
tla+: expand gateway exposure v2 matrix (custom/tailnet + password)
2026-01-26 00:04:21 -08:00
gateway_exposure_v2_protected_lan_password_with_creds.cfg
tla+: expand gateway exposure v2 matrix (custom/tailnet + password)
2026-01-26 00:04:21 -08:00
gateway_exposure_v2_protected_lan_token_no_creds.cfg
tla+: add protected gateway exposure scenarios (token blocks unauth attacker)
2026-01-25 20:25:28 -08:00
gateway_exposure_v2_protected_lan_token_with_creds.cfg
tla+: add protected gateway exposure scenarios (token blocks unauth attacker)
2026-01-25 20:25:28 -08:00
gateway_exposure_v2_protected_tailnet_token_no_creds.cfg
tla+: expand gateway exposure v2 matrix (custom/tailnet + password)
2026-01-26 00:04:21 -08:00
gateway_exposure_v2_safe_loopback.cfg
tla+: refine gateway exposure model (bind modes + auth auto resolution)
2026-01-25 19:22:14 -08:00
gateway_exposure_v2_unsafe_auto_noauth.cfg
tla+: add gateway bind=auto cases; document gateway exposure matrix
2026-01-26 00:39:32 -08:00
gateway_exposure_v2_unsafe_custom_noauth.cfg
tla+: expand gateway exposure v2 matrix (custom/tailnet + password)
2026-01-26 00:04:21 -08:00
gateway_exposure_v2_unsafe_lan_noauth.cfg
tla+: refine gateway exposure model (bind modes + auth auto resolution)
2026-01-25 19:22:14 -08:00
gateway_exposure_v2_unsafe_tailnet_noauth.cfg
tla+: expand gateway exposure v2 matrix (custom/tailnet + password)
2026-01-26 00:04:21 -08:00
group_memory_bad_missing.cfg
conformance: wire tool group expansion to extracted constants; cleanup stale models
2026-01-25 00:57:10 -08:00
group_memory_conformance.cfg
conformance: wire tool group expansion to extracted constants; cleanup stale models
2026-01-25 00:57:10 -08:00
group_memory_ok.cfg
conformance: wire tool group expansion to extracted constants; cleanup stale models
2026-01-25 00:57:10 -08:00
indirect_prompt_injection_negative.cfg
models: add indirect prompt injection boundary harness
2026-02-02 12:24:11 -08:00
indirect_prompt_injection_ok.cfg
models: add indirect prompt injection boundary harness
2026-02-02 12:24:11 -08:00
ingress_dedupe_fallback_negative.cfg
formal: ingress dedupe fallback when eventId missing (green+red)
2026-01-27 14:41:31 -08:00
ingress_dedupe_fallback_ok.cfg
formal: ingress dedupe fallback when eventId missing (green+red)
2026-01-27 14:41:31 -08:00
ingress_gating_negative.cfg
tla+: add ingress gating harness (mention gating + control-command bypass)
2026-01-26 15:44:11 -08:00
ingress_gating_ok.cfg
tla+: add ingress gating harness (mention gating + control-command bypass)
2026-01-26 15:44:11 -08:00
ingress_idempotency_negative.cfg
formal: ingress provider event idempotency harness (green+red)
2026-01-27 12:41:08 -08:00
ingress_idempotency_ok.cfg
formal: ingress provider event idempotency harness (green+red)
2026-01-27 12:41:08 -08:00
ingress_multievent_trace_negative.cfg
formal: ingress multi-event trace correlation harness (green+red)
2026-01-27 11:02:39 -08:00
ingress_multievent_trace_ok.cfg
formal: ingress multi-event trace correlation harness (green+red)
2026-01-27 11:02:39 -08:00
ingress_multimsg_trace_negative.cfg
formal: ingress multi-message trace correlation harness (green+red)
2026-01-27 10:22:01 -08:00
ingress_multimsg_trace_ok.cfg
formal: ingress multi-message trace correlation harness (green+red)
2026-01-27 10:22:01 -08:00
ingress_retry_negative.cfg
models: add ingress retry+dedupe harness
2026-02-01 00:45:54 -08:00
ingress_retry_ok.cfg
models: add ingress retry+dedupe harness
2026-02-01 00:45:54 -08:00
message_delete_session_binding_negative.cfg
models: add message delete session binding harness
2026-02-02 12:22:44 -08:00
message_delete_session_binding_ok.cfg
models: add message delete session binding harness
2026-02-02 12:22:44 -08:00
message_edit_session_binding_negative.cfg
models: add message edit + thread reaction binding harnesses
2026-02-02 10:52:21 -08:00
message_edit_session_binding_ok.cfg
models: add message edit + thread reaction binding harnesses
2026-02-02 10:52:21 -08:00
message_lifecycle_session_key_negative.cfg
models: add message lifecycle session key stability harness
2026-02-03 13:11:00 -08:00
message_lifecycle_session_key_ok.cfg
models: add message lifecycle session key stability harness
2026-02-03 13:11:00 -08:00
multi_channel_identity_collision_negative.cfg
models: add multi-channel identity collision harness
2026-02-02 12:27:46 -08:00
multi_channel_identity_collision_ok.cfg
models: add multi-channel identity collision harness
2026-02-02 12:27:46 -08:00
multi_channel_identity_override_negative.cfg
models: add multi-channel identity override harness
2026-02-03 13:26:23 -08:00
multi_channel_identity_override_ok.cfg
models: add multi-channel identity override harness
2026-02-03 13:26:23 -08:00
multi_event_eventual_emission_negative.cfg
models: add multi-event eventual emission liveness harness
2026-02-01 02:09:14 -08:00
multi_event_eventual_emission_ok.cfg
models: add multi-event eventual emission liveness harness
2026-02-01 02:09:14 -08:00
no_cross_stream_negative.cfg
models: add no cross-stream leakage harness
2026-02-01 02:06:13 -08:00
no_cross_stream_ok.cfg
models: add no cross-stream leakage harness
2026-02-01 02:06:13 -08:00
nodes_pipeline_negative_replay.cfg
tla+: compose nodes.run pipeline harness (allowlist+declared+tokenized approval)
2026-01-25 16:24:59 -08:00
nodes_pipeline_ok.cfg
tla+: compose nodes.run pipeline harness (allowlist+declared+tokenized approval)
2026-01-25 16:24:59 -08:00
nodes_policy_negative_bad_impl_allows_undeclared.cfg
tla+: model-check gateway node command allowlist + declaredCommands gating
2026-01-25 00:47:25 -08:00
nodes_policy_ok.cfg
tla+: model-check gateway node command allowlist + declaredCommands gating
2026-01-25 00:47:25 -08:00
openclaw_session_key_conformance_negative.cfg
models: add dedupe collision, crash/restart, concurrency, and conformance harnesses
2026-02-01 10:41:46 -08:00
openclaw_session_key_conformance_ok.cfg
models: add dedupe collision, crash/restart, concurrency, and conformance harnesses
2026-02-01 10:41:46 -08:00
pairing_concurrent_negative.cfg
tla+: add pairing store race harness (locked vs non-atomic cap check)
2026-01-27 03:08:29 -08:00
pairing_concurrent_ok.cfg
tla+: add pairing store race harness (locked vs non-atomic cap check)
2026-01-27 03:08:29 -08:00
pairing_idempotency_negative.cfg
formal: pairing-store idempotency harness (green+red)
2026-01-27 04:02:12 -08:00
pairing_idempotency_ok.cfg
formal: pairing-store idempotency harness (green+red)
2026-01-27 04:02:12 -08:00
pairing_refresh_enabled_negative.cfg
formal: pairing-store refresh enabled at cap (green+red)
2026-01-27 11:42:09 -08:00
pairing_refresh_enabled_ok.cfg
formal: pairing-store refresh enabled at cap (green+red)
2026-01-27 11:42:09 -08:00
pairing_refresh_race_negative.cfg
formal: pairing refresh race harness (green+red)
2026-01-27 13:42:07 -08:00
pairing_refresh_race_ok.cfg
formal: pairing refresh race harness (green+red)
2026-01-27 13:42:07 -08:00
pairing_v2_cap_negative.cfg
tla+: extend pairing store model with MaxPending cap counterexample
2026-01-26 15:20:50 -08:00
pairing_v2_cap_ok.cfg
tla+: extend pairing store model with MaxPending cap counterexample
2026-01-26 15:20:50 -08:00
pairing_v2_negative_badexpiry.cfg
tla+: add pairing store harness (TTL + max pending) with expiry counterexample
2026-01-26 14:52:51 -08:00
pairing_v2_ok.cfg
tla+: add pairing store harness (TTL + max pending) with expiry counterexample
2026-01-26 14:52:51 -08:00
policy_hot_reload_negative.cfg
models: add policy hot-reload safety harness
2026-02-03 13:22:58 -08:00
policy_hot_reload_ok.cfg
models: add policy hot-reload safety harness
2026-02-03 13:22:58 -08:00
precedence_min.cfg
tla+: model-check tool policy precedence (deny wins)
2026-01-24 22:04:18 -08:00
precedence_negative_bad_allow_overrides.cfg
tla+: add negative test demonstrating precedence bug counterexample
2026-01-24 22:33:42 -08:00
queue_drain_ok.cfg
models: add queue drain liveness harness
2026-02-01 01:27:29 -08:00
reaction_session_binding_negative.cfg
models: add reaction session binding conformance harness
2026-02-02 01:37:24 -08:00
reaction_session_binding_ok.cfg
models: add reaction session binding conformance harness
2026-02-02 01:37:24 -08:00
retry_eventual_success_negative.cfg
models: add retry eventual success liveness harness
2026-02-01 02:01:07 -08:00
retry_eventual_success_ok.cfg
models: add retry eventual success liveness harness
2026-02-01 02:01:07 -08:00
retry_termination_negative.cfg
models: add retry termination liveness harness
2026-02-01 01:57:58 -08:00
retry_termination_ok.cfg
models: add retry termination liveness harness
2026-02-01 01:57:58 -08:00
routing_identity_channel_override_negative.cfg
formal: channel override can disable identityLinks (green+red)
2026-01-27 19:41:22 -08:00
routing_identity_channel_override_ok.cfg
formal: channel override can disable identityLinks (green+red)
2026-01-27 19:41:22 -08:00
routing_identity_symmetry_negative.cfg
formal: routing identityLinks symmetry/reflexivity harness (green+red)
2026-01-27 18:42:32 -08:00
routing_identity_symmetry_ok.cfg
formal: routing identityLinks symmetry/reflexivity harness (green+red)
2026-01-27 18:42:32 -08:00
routing_identity_transitive_negative.cfg
formal: routing identityLinks transitive closure harness (green+red)
2026-01-27 15:44:37 -08:00
routing_identity_transitive_ok.cfg
formal: routing identityLinks transitive closure harness (green+red)
2026-01-27 15:44:37 -08:00
routing_identitylinks_negative.cfg
formal: routing identityLinks harness (group partition; green+red)
2026-01-27 14:50:21 -08:00
routing_identitylinks_ok.cfg
formal: routing identityLinks harness (group partition; green+red)
2026-01-27 14:50:21 -08:00
routing_isolation_negative.cfg
tla+: add routing/session-key isolation harness (R3)
2026-01-26 19:51:04 -08:00
routing_isolation_ok.cfg
tla+: add routing/session-key isolation harness (R3)
2026-01-26 19:51:04 -08:00
routing_precedence_negative.cfg
formal: routing dmScope precedence harness (green+red)
2026-01-27 05:22:13 -08:00
routing_precedence_ok.cfg
formal: routing dmScope precedence harness (green+red)
2026-01-27 05:22:13 -08:00
routing_thread_parent_channel_override_negative.cfg
models: add thread parent channel override conformance harness
2026-02-01 22:45:27 -08:00
routing_thread_parent_channel_override_ok.cfg
models: add thread parent channel override conformance harness
2026-02-01 22:45:27 -08:00
routing_thread_parent_negative.cfg
models: add routing thread parent + discord pluralkit identity harnesses
2026-02-01 00:39:14 -08:00
routing_thread_parent_ok.cfg
models: add routing thread parent + discord pluralkit identity harnesses
2026-02-01 00:39:14 -08:00
routing_trirule_negative.cfg
models: add combined routing tri-rule + proxy header spoof harness
2026-02-01 22:51:56 -08:00
routing_trirule_ok.cfg
models: add combined routing tri-rule + proxy header spoof harness
2026-02-01 22:51:56 -08:00
session_explosion_ok.cfg
models: add session key stability + session explosion bound harnesses
2026-02-01 00:51:40 -08:00
session_key_stability_negative.cfg
models: add session key stability + session explosion bound harnesses
2026-02-01 00:51:40 -08:00
session_key_stability_ok.cfg
models: add session key stability + session explosion bound harnesses
2026-02-01 00:51:40 -08:00
taint_propagation_negative.cfg
models: add taint propagation approval harness
2026-02-03 13:17:12 -08:00
taint_propagation_ok.cfg
models: add taint propagation approval harness
2026-02-03 13:17:12 -08:00
thread_parent_reaction_binding_negative.cfg
models: add message edit + thread reaction binding harnesses
2026-02-02 10:52:21 -08:00
thread_parent_reaction_binding_ok.cfg
models: add message edit + thread reaction binding harnesses
2026-02-02 10:52:21 -08:00
two_worker_dedupe_negative.cfg
models: add dedupe collision, crash/restart, concurrency, and conformance harnesses
2026-02-01 10:41:46 -08:00
two_worker_dedupe_ok.cfg
models: add dedupe collision, crash/restart, concurrency, and conformance harnesses
2026-02-01 10:41:46 -08:00