[codex] Fix production readiness gates

.github/scripts/check_checker_differential.py

@@ -327,16 +327,32 @@ def lookup_allowlist(
 
 
 def ensure_binaries() -> tuple[Path, Path]:
-    build_cmd = ["cargo", "build", "-p", "tarsier-cli", "-p", "tarsier-certcheck"]
+    build_cmd = [
+        "cargo",
+        "build",
+        "-p",
+        "tarsier-cli",
+        "-p",
+        "tarsier-certcheck",
+        "--features",
+        "tarsier-cli/governance",
+    ]
     print("[info] building checker binaries:", " ".join(build_cmd))
     rc, out, err = run_command(build_cmd, ROOT)
     if rc != 0:
         sys.stderr.write(out)
         sys.stderr.write(err)
         raise RuntimeError("failed to build checker binaries")
+    metadata_cmd = ["cargo", "metadata", "--no-deps", "--format-version", "1"]
+    rc, out, err = run_command(metadata_cmd, ROOT)
+    if rc != 0:
+        sys.stderr.write(out)
+        sys.stderr.write(err)
+        raise RuntimeError("failed to resolve cargo target directory")
+    target_dir = Path(json.loads(out)["target_directory"])
     suffix = ".exe" if sys.platform.startswith("win") else ""
-    legacy = ROOT / "target" / "debug" / f"tarsier{suffix}"
-    tiny = ROOT / "target" / "debug" / f"tarsier-certcheck{suffix}"
+    legacy = target_dir / "debug" / f"tarsier{suffix}"
+    tiny = target_dir / "debug" / f"tarsier-certcheck{suffix}"
     if not legacy.exists():
         raise RuntimeError(f"missing legacy checker binary: {legacy}")
     if not tiny.exists():

.github/workflows/ci.yml

@@ -38,6 +38,14 @@ jobs:
           else
             base_ref="HEAD"
           fi
+          if ! git cat-file -e "${base_ref}^{commit}" 2>/dev/null; then
+            echo "Base ref ${base_ref} is unavailable; falling back to HEAD^ for maintainability limits."
+            if git rev-parse --verify HEAD^ >/dev/null 2>&1; then
+              base_ref="HEAD^"
+            else
+              base_ref="HEAD"
+            fi
+          fi
           python3 scripts/check_maintainability_limits.py --base "${base_ref}"
 
       - name: Enforce Certification Gate Contract
@@ -220,9 +228,9 @@ jobs:
 
       - name: Checker Soundness Subset Gate
         run: |
-          output=$(cargo test -p tarsier-proof-kernel soundness_subset_ -- --nocapture 2>&1)
+          output=$(CARGO_TERM_COLOR=never cargo test -p tarsier-proof-kernel soundness_subset_ -- --nocapture 2>&1)
           echo "$output"
-          count=$(echo "$output" | grep -Ec 'test tests::soundness_subset_.*\\.\\.\\. ok')
+          count=$(echo "$output" | grep -Ec '^test tests::soundness_subset_.* \.\.\. ok$')
           if [ "$count" -lt 2 ]; then
             echo "ERROR: expected at least 2 checker soundness subset tests to pass, got $count"
             exit 1

.github/workflows/live-adapter-conformance.yml

@@ -27,6 +27,7 @@ jobs:
     runs-on: ubuntu-latest
     env:
       CMAKE_POLICY_VERSION_MINIMUM: "3.5"
+      WAIT_SECS: "120"
     steps:
       - name: Checkout
         uses: actions/checkout@v4
@@ -118,11 +119,13 @@ jobs:
           REPORT_FILE=artifacts/live-adapter/cometbft-live-report.json \
           EVENTS_FILE=artifacts/live-adapter/cometbft-live-events.jsonl \
           SERVER_LOG=artifacts/live-adapter/cometbft-live-server.log \
+          KEEP_HARNESS=1 \
           ./scripts/cometbft-conformance-active-smoke.sh smoke
 
           REPORT_FILE=artifacts/live-adapter/etcd-raft-live-report.json \
           EVENTS_FILE=artifacts/live-adapter/etcd-raft-live-events.jsonl \
           SERVER_LOG=artifacts/live-adapter/etcd-raft-live-server.log \
+          KEEP_HARNESS=1 \
           ./scripts/etcd-raft-conformance-active-smoke.sh smoke
 
       - name: Capture triage details on failure
@@ -137,6 +140,12 @@ jobs:
           docker compose -f integration/etcd-raft-live/docker-compose.yml ps > artifacts/live-adapter/etcd-compose-ps.txt || true
           docker compose -f integration/etcd-raft-live/docker-compose.yml logs --no-color > artifacts/live-adapter/etcd-compose-logs.txt || true
 
+      - name: Stop live harnesses
+        if: always()
+        run: |
+          ./scripts/cometbft-live-harness.sh stop >/dev/null 2>&1 || true
+          ./scripts/etcd-raft-live-harness.sh stop >/dev/null 2>&1 || true
+
       - name: Upload nightly artifacts
         if: always()
         uses: actions/upload-artifact@v4

benchmarks/bymc/Dockerfile

@@ -1,33 +1,43 @@
 # ByMC (Byzantine Model Checker) Docker image
-# Pinned to v2.4.4 for reproducible verification runs.
+# Pinned to bymc-2.4.2 for reproducible verification runs.
 #
 # Build:   docker build -t tarsier-bymc:latest benchmarks/bymc/
 # Run:     docker run --rm -v "$PWD":/work tarsier-bymc:latest /work/model.ta all
 
 FROM ubuntu:18.04
 
 ENV DEBIAN_FRONTEND=noninteractive
+ARG OPAM_VERSION=2.1.5
+ARG OPAM_REPOSITORY_REF=2026-05-before-lower-bound-ocaml411
 
 # System dependencies
 RUN apt-get update && apt-get install -y --no-install-recommends \
     build-essential \
     ca-certificates \
     curl \
     git \
+    libffi-dev \
+    libgmp-dev \
     m4 \
+    mpi-default-dev \
     pkg-config \
+    python2.7 \
     python3 \
     unzip \
     wget \
   && rm -rf /var/lib/apt/lists/*
 
-# Install opam 2.x
-RUN curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh | \
-    sh -s -- --version 2.1.5
+# Install a pinned opam binary instead of streaming the mutable installer script.
+RUN curl -fsSL \
+    "https://github.com/ocaml/opam/releases/download/${OPAM_VERSION}/opam-${OPAM_VERSION}-x86_64-linux" \
+    -o /usr/local/bin/opam && \
+    chmod +x /usr/local/bin/opam && \
+    opam --version
 
 # Initialize opam with OCaml 4.06.1 (last version well-supported by ByMC)
-RUN opam init --disable-sandboxing --bare -y && \
-    opam switch create 4.06.1 && \
+RUN opam init --disable-sandboxing --bare -y --shell=sh \
+      default "https://github.com/ocaml/opam-repository.git#${OPAM_REPOSITORY_REF}" && \
+    opam switch create 4.06.1 ocaml-base-compiler.4.06.1 -y && \
     eval $(opam env)
 
 # Install Z3 4.8.7 from GitHub release
@@ -38,20 +48,25 @@ RUN wget -q https://github.com/Z3Prover/z3/releases/download/z3-4.8.7/z3-4.8.7-x
     rm /tmp/z3.zip
 
 ENV PATH="/opt/z3/bin:${PATH}"
-ENV LD_LIBRARY_PATH="/opt/z3/bin:${LD_LIBRARY_PATH}"
+ENV LD_LIBRARY_PATH="/opt/z3/bin"
 
 # Install OCaml dependencies via opam
 RUN eval $(opam env) && \
     opam install -y \
+      ocamlbuild \
+      menhir.20181113 \
       batteries \
       ocamlgraph \
       sexplib \
+      lazy-trie.1.2.0 \
+      mpi.1.07 \
+      z3.4.8.7 \
       ctypes \
       ctypes-foreign
 
 # Clone and build ByMC at pinned tag
 RUN eval $(opam env) && \
-    git clone --depth 1 --branch v2.4.4 https://github.com/konnov/bymc.git /opt/bymc && \
+    git clone --depth 1 --branch bymc-2.4.2 https://github.com/konnov/bymc.git /opt/bymc && \
     cd /opt/bymc/bymc && \
     make
 

crates/tarsier-certcheck/src/tests.rs

@@ -8,7 +8,9 @@ use miette::miette;
 use std::collections::BTreeMap;
 use std::fs;
 use std::path::PathBuf;
-use std::time::{SystemTime, UNIX_EPOCH};
+use std::sync::atomic::{AtomicU64, Ordering};
+
+static TMP_DIR_COUNTER: AtomicU64 = AtomicU64::new(0);
 
 #[test]
 fn parse_solver_list_dedups_and_sorts() {
@@ -115,11 +117,8 @@ fn record_solver_outcome_tracks_per_solver_totals() {
 
 fn tmp_dir(prefix: &str) -> PathBuf {
     let mut path = std::env::temp_dir();
-    let nanos = SystemTime::now()
-        .duration_since(UNIX_EPOCH)
-        .expect("clock should be monotonic enough for tests")
-        .as_nanos();
-    path.push(format!("{}_{}_{}", prefix, std::process::id(), nanos));
+    let seq = TMP_DIR_COUNTER.fetch_add(1, Ordering::Relaxed);
+    path.push(format!("{}_{}_{}", prefix, std::process::id(), seq));
     path
 }
 
@@ -185,7 +184,11 @@ fn external_solver_runner_rejects_malformed_output() {
         &smt,
     )
     .expect_err("malformed solver output should be rejected");
-    assert!(err.to_string().contains("malformed solver output"));
+    let msg = err.to_string();
+    assert!(
+        msg.contains("malformed solver output"),
+        "unexpected solver error: {msg}"
+    );
 
     fs::remove_dir_all(&dir).ok();
 }