{
  "async": {
    "adversarial_prefix": [
      "delay RBC from p3",
      "deliver p0/p1 messages",
      "delay threshold share"
    ],
    "finite_delay_refutes_probabilistic_termination": false,
    "finite_prefix_has_decision": false,
    "timing_free_liveness_still_requires_eventual_message_delivery_and_randomness": true
  },
  "environment": {
    "platform": "Linux-5.10.134-013.16.kangaroo.al8.x86_64-x86_64-with-glibc2.39",
    "python": "3.12.3"
  },
  "gates": {
    "bft_certificate_intersection": true,
    "finite_delay_not_liveness_counterexample": true,
    "ordered_network_gap_requires_recovery": true,
    "streamlet_consecutive_rule": true
  },
  "model": "finite assumption checks, not protocol implementations or benchmarks",
  "not_modeled": [
    "NOPaxos switch/sequencer or failover",
    "Streamlet network or signatures",
    "HoneyBadger cryptography, ACS, or randomness",
    "latency, throughput, hardware, or production code"
  ],
  "ordering": {
    "missing_sequence": 3,
    "network_ordering_replaces_all_recovery_logic": false,
    "normal_path_can_continue_without_recovery": false,
    "ordered_delivery": {
      "r1": [
        1,
        2,
        4
      ],
      "r2": [
        1,
        2,
        3,
        4
      ]
    },
    "replica_with_gap": "r1"
  },
  "quorum": {
    "all_intersections_contain_correct_node": true,
    "cases": 24,
    "certificate_size": 3,
    "f": 1,
    "n": 4
  },
  "schema_version": 1,
  "streamlet": {
    "middle_block_finalized": {
      "consecutive": true,
      "gap": false,
      "only_two": false
    },
    "notarized_epoch_sequences": {
      "consecutive": [
        1,
        2,
        3
      ],
      "gap": [
        1,
        3,
        4
      ],
      "only_two": [
        5,
        6
      ]
    }
  }
}