Merge branch 'feature-export-rng' into feature-export-rng-lean

.github/workflows/formal-verification.yml

@@ -0,0 +1,127 @@
+name: Formal Verification (Lean)
+
+on:
+  push:
+    branches: ["feature-export-rng-lean"]
+  pull_request:
+    branches: ["**"]
+    types: [opened, synchronize, reopened]
+  workflow_dispatch:
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  lean-consensus:
+    name: Lean/C++ drift checks
+    runs-on: [self-hosted, macOS]
+    env:
+      BUILD_DIR: .build-formal
+      CMAKE_BUILD_DIR: .build-formal-cmake
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Add Homebrew to PATH
+        run: |
+          echo "/opt/homebrew/bin" >> "$GITHUB_PATH"
+          echo "/opt/homebrew/sbin" >> "$GITHUB_PATH"
+
+      - name: Install core tools
+        run: |
+          brew install coreutils
+          echo "Num proc: $(nproc)"
+
+      - name: Setup toolchain (mise)
+        uses: jdx/mise-action@v3.6.1
+        with:
+          cache: false
+          install: true
+          mise_toml: |
+            [tools]
+            cmake = "3.25.3"
+            python = "3.12"
+            pipx = "latest"
+            conan = "2"
+            ninja = "latest"
+
+      - name: Install tools via mise
+        run: |
+          mise install
+          mise reshim
+          echo "$HOME/.local/share/mise/shims" >> "$GITHUB_PATH"
+
+      - name: Install Lean toolchain
+        run: |
+          toolchain="$(cat formal_verification/lean-toolchain)"
+          curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+            | sh -s -- -y --default-toolchain "$toolchain"
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+          "$HOME/.elan/bin/lake" --version
+          "$HOME/.elan/bin/lean" --version
+
+      - name: Build Lean proofs
+        run: |
+          cd formal_verification
+          "$HOME/.elan/bin/lake" build XahauConsensus:static
+
+      - name: Detect compiler version
+        id: detect-compiler
+        run: |
+          compiler_version=$(clang --version | grep -oE 'version [0-9]+' | grep -oE '[0-9]+')
+          echo "compiler_version=${compiler_version}" >> "$GITHUB_OUTPUT"
+          echo "Detected Apple Clang version: ${compiler_version}"
+
+      - name: Configure Conan profile
+        run: |
+          mkdir -p ~/.conan2/profiles
+          cat > ~/.conan2/profiles/default <<EOF
+          [settings]
+          arch=armv8
+          build_type=Debug
+          compiler=apple-clang
+          compiler.cppstd=20
+          compiler.libcxx=libc++
+          compiler.version=${{ steps.detect-compiler.outputs.compiler_version }}
+          os=Macos
+
+          [conf]
+          tools.build:cxxflags=["-Wno-missing-template-arg-list-after-template-kw"]
+          EOF
+          conan profile show
+
+      - name: Export custom Conan recipes
+        run: |
+          conan export external/snappy --version 1.1.10 --user xahaud --channel stable
+          conan export external/soci --version 4.0.3 --user xahaud --channel stable
+          conan export external/wasmedge --version 0.11.2 --user xahaud --channel stable
+
+      - name: Install Conan dependencies
+        env:
+          CONAN_REQUEST_TIMEOUT: 180
+        run: |
+          conan install . \
+            --output-folder "$BUILD_DIR" \
+            --build missing \
+            --settings build_type=Debug \
+            -o '&:tests=True' \
+            -o '&:xrpld=True' \
+            -o '&:formal_verification=True'
+
+      - name: Configure formal build
+        run: |
+          cmake -S . -B "$CMAKE_BUILD_DIR" -G Ninja \
+            -DCMAKE_TOOLCHAIN_FILE="$PWD/$BUILD_DIR/build/generators/conan_toolchain.cmake" \
+            -DCMAKE_BUILD_TYPE=Debug \
+            -Dtests=ON \
+            -Dxrpld=ON \
+            -Dformal_verification=ON
+
+      - name: Build formal-enabled rippled
+        run: |
+          cmake --build "$CMAKE_BUILD_DIR" --target rippled --parallel "$(nproc)"
+
+      - name: Run Lean/C++ drift checks
+        run: |
+          "$CMAKE_BUILD_DIR/rippled" --unittest=LeanConsensus --unittest-log

Builds/levelization/results/ordering.txt

@@ -59,6 +59,8 @@ test.csf > xrpl.basics
 test.csf > xrpld.consensus
 test.csf > xrpl.json
 test.csf > xrpl.protocol
+test.formal_verification > xrpld.app
+test.formal_verification > xrpld.consensus
 test.json > test.jtx
 test.json > xrpl.json
 test.jtx > xrpl.basics

cmake/RippledCore.cmake

@@ -160,6 +160,10 @@ target_link_modules(xrpl PUBLIC
 #     $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/include>
 #     $<INSTALL_INTERFACE:include>)
 
+if(formal_verification AND NOT xrpld)
+  message(FATAL_ERROR "formal_verification requires xrpld=ON")
+endif()
+
 if(xrpld)
   add_executable(rippled)
   if(tests)
@@ -211,6 +215,7 @@ if(xrpld)
     # This is likely not strictly necessary, but listed explicitly as a good practice.
     m
   )
+  include(XahaudFormalVerification)
   exclude_if_included(rippled)
   # define a macro for tests that might need to
   # be exluded or run differently in CI environment

cmake/RippledSettings.cmake

@@ -19,6 +19,14 @@ option(xahaud_runtime_test_config
 # [conf]
 # tools.cmake.cmaketoolchain:extra_variables={"xahaud_runtime_test_config":"ON"}
 
+option(formal_verification
+  "Enable Lean-backed formal-verification cross-check tests"
+  OFF)
+# Default off: this pulls the Lean runtime and the vendored formal model into
+# the test binary. Conan/local opt-in mirrors the runtime-test-config pattern:
+# [conf]
+# tools.cmake.cmaketoolchain:extra_variables={"formal_verification":"ON"}
+
 option(unity "Creates a build using UNITY support in cmake. This is the default" ON)
 if(unity)
   if(NOT is_ci)

cmake/XahaudFormalVerification.cmake

@@ -0,0 +1,65 @@
+if(NOT formal_verification)
+  return()
+endif()
+
+if(NOT xrpld)
+  message(FATAL_ERROR "formal_verification requires xrpld=ON")
+endif()
+
+if(NOT tests)
+  message(FATAL_ERROR "formal_verification requires tests=ON")
+endif()
+
+if(CMAKE_CROSSCOMPILING)
+  message(FATAL_ERROR "formal_verification currently supports native builds only")
+endif()
+
+if(WIN32)
+  message(FATAL_ERROR "formal_verification currently supports Unix-like native builds only")
+endif()
+
+set(XAHAU_FORMAL_VERIFICATION_DIR
+  "${CMAKE_CURRENT_SOURCE_DIR}/formal_verification"
+  CACHE PATH
+  "Lean formal-verification project used by formal_verification=ON")
+
+include(XahaudLean)
+xahaud_require_lean_toolchain("${XAHAU_FORMAL_VERIFICATION_DIR}")
+
+set(XAHAU_FORMAL_ARCHIVE
+  "${XAHAU_FORMAL_VERIFICATION_DIR}/.lake/build/lib/libxahau__consensus_XahauConsensus.a")
+
+file(GLOB_RECURSE XAHAU_FORMAL_SOURCES CONFIGURE_DEPENDS
+  "${XAHAU_FORMAL_VERIFICATION_DIR}/*.lean")
+
+# Lake currently writes package artifacts under the Lean workspace's .lake/
+# directory. Keep this option native/test-only until the build is moved to a
+# copied CMake-binary-dir workspace or Lake grows a stable external build-dir
+# interface we can rely on here.
+#
+# This target deliberately invokes Lake whenever the formal-enabled `rippled`
+# target is built. Lake still performs its own incremental rebuild, but CMake
+# must not trust a source-tree `.lake` archive purely by timestamp.
+add_custom_target(xahaud_formal_verification_lean
+  COMMAND "${LAKE_EXECUTABLE}" build XahauConsensus:static
+  WORKING_DIRECTORY "${XAHAU_FORMAL_VERIFICATION_DIR}"
+  DEPENDS
+    "${XAHAU_FORMAL_VERIFICATION_DIR}/lakefile.toml"
+    "${XAHAU_FORMAL_VERIFICATION_DIR}/lean-toolchain"
+    "${XAHAU_FORMAL_VERIFICATION_DIR}/lake-manifest.json"
+    ${XAHAU_FORMAL_SOURCES}
+  BYPRODUCTS "${XAHAU_FORMAL_ARCHIVE}"
+  COMMENT "Building Lean formal-verification archive"
+  VERBATIM)
+
+add_dependencies(rippled xahaud_formal_verification_lean)
+target_compile_definitions(rippled PRIVATE XAHAUD_ENABLE_FORMAL_VERIFICATION=1)
+target_include_directories(rippled PRIVATE "${LEAN_INCLUDE_DIR}")
+target_link_libraries(rippled "${XAHAU_FORMAL_ARCHIVE}" "${LEAN_SHARED_LIBRARY}")
+
+if(UNIX)
+  set_property(TARGET rippled APPEND PROPERTY BUILD_RPATH "${LEAN_SYSROOT}/lib/lean")
+endif()
+
+message(STATUS "Formal verification enabled: ${XAHAU_FORMAL_VERIFICATION_DIR}")
+message(STATUS "Lean ${LEAN_EXPECTED_VERSION} sysroot: ${LEAN_SYSROOT}")

cmake/XahaudLean.cmake

@@ -0,0 +1,113 @@
+include_guard(GLOBAL)
+
+function(xahaud_require_lean_toolchain project_dir)
+  if(NOT EXISTS "${project_dir}/lean-toolchain")
+    message(FATAL_ERROR "Lean project is missing lean-toolchain: ${project_dir}")
+  endif()
+
+  file(READ "${project_dir}/lean-toolchain" lean_toolchain)
+  string(STRIP "${lean_toolchain}" lean_toolchain)
+  if(NOT lean_toolchain MATCHES "^leanprover/lean4:v([0-9]+\\.[0-9]+\\.[0-9]+([-+._A-Za-z0-9]+)?)$")
+    message(FATAL_ERROR
+      "Unsupported lean-toolchain format `${lean_toolchain}` in ${project_dir}")
+  endif()
+  set(expected_lean_version "${CMAKE_MATCH_1}")
+
+  find_program(LAKE_EXECUTABLE
+    NAMES lake
+    HINTS "$ENV{HOME}/.elan/bin")
+  if(NOT LAKE_EXECUTABLE)
+    message(FATAL_ERROR
+      "formal_verification=ON requires Lake on PATH or in ~/.elan/bin. "
+      "Install elan, then run `lake build` once in ${project_dir}.")
+  endif()
+
+  execute_process(
+    COMMAND "${LAKE_EXECUTABLE}" env lean --version
+    WORKING_DIRECTORY "${project_dir}"
+    OUTPUT_VARIABLE lean_version_output
+    ERROR_VARIABLE lean_version_error
+    OUTPUT_STRIP_TRAILING_WHITESPACE
+    ERROR_STRIP_TRAILING_WHITESPACE
+    RESULT_VARIABLE lean_version_result)
+  if(NOT lean_version_result EQUAL 0)
+    message(FATAL_ERROR
+      "Could not run `${LAKE_EXECUTABLE} env lean --version`: "
+      "${lean_version_error}")
+  endif()
+  if(NOT lean_version_output MATCHES "^Lean \\(version ([^,)]+)[,)]")
+    message(FATAL_ERROR
+      "Could not parse Lean version from `${lean_version_output}`")
+  endif()
+  set(actual_lean_version "${CMAKE_MATCH_1}")
+  if(NOT actual_lean_version STREQUAL expected_lean_version)
+    message(FATAL_ERROR
+      "Lean version mismatch for formal_verification=ON. "
+      "Expected ${expected_lean_version} from ${project_dir}/lean-toolchain, "
+      "but `${LAKE_EXECUTABLE} env lean --version` returned "
+      "`${lean_version_output}`")
+  endif()
+
+  execute_process(
+    COMMAND "${LAKE_EXECUTABLE}" --version
+    WORKING_DIRECTORY "${project_dir}"
+    OUTPUT_VARIABLE lake_version_output
+    ERROR_VARIABLE lake_version_error
+    OUTPUT_STRIP_TRAILING_WHITESPACE
+    ERROR_STRIP_TRAILING_WHITESPACE
+    RESULT_VARIABLE lake_version_result)
+  if(NOT lake_version_result EQUAL 0)
+    message(FATAL_ERROR
+      "Could not run `${LAKE_EXECUTABLE} --version`: ${lake_version_error}")
+  endif()
+  if(NOT lake_version_output MATCHES "Lean version ([^)]+)\\)")
+    message(FATAL_ERROR
+      "Could not parse Lake's Lean version from `${lake_version_output}`")
+  endif()
+  set(lake_lean_version "${CMAKE_MATCH_1}")
+  if(NOT lake_lean_version STREQUAL expected_lean_version)
+    message(FATAL_ERROR
+      "Lake version mismatch for formal_verification=ON. "
+      "Expected Lean ${expected_lean_version} from ${project_dir}/lean-toolchain, "
+      "but `${LAKE_EXECUTABLE} --version` returned `${lake_version_output}`")
+  endif()
+
+  if(NOT EXISTS "${project_dir}/lakefile.toml")
+    message(FATAL_ERROR
+      "formal_verification=ON requires ${project_dir}/lakefile.toml")
+  endif()
+
+  execute_process(
+    COMMAND "${LAKE_EXECUTABLE}" env printenv LEAN_SYSROOT
+    WORKING_DIRECTORY "${project_dir}"
+    OUTPUT_VARIABLE lean_sysroot
+    ERROR_VARIABLE lean_sysroot_error
+    OUTPUT_STRIP_TRAILING_WHITESPACE
+    ERROR_STRIP_TRAILING_WHITESPACE
+    RESULT_VARIABLE lean_sysroot_result)
+  if(NOT lean_sysroot_result EQUAL 0 OR NOT lean_sysroot)
+    message(FATAL_ERROR
+      "Could not determine Lean sysroot via "
+      "`${LAKE_EXECUTABLE} env printenv LEAN_SYSROOT`: ${lean_sysroot_error}")
+  endif()
+
+  set(lean_include_dir "${lean_sysroot}/include")
+  if(NOT EXISTS "${lean_include_dir}/lean/lean.h")
+    message(FATAL_ERROR "Lean header not found: ${lean_include_dir}/lean/lean.h")
+  endif()
+
+  find_library(lean_shared_library
+    NAMES leanshared libleanshared
+    PATHS "${lean_sysroot}/lib/lean"
+    NO_DEFAULT_PATH)
+  if(NOT lean_shared_library)
+    message(FATAL_ERROR
+      "Lean shared runtime not found under ${lean_sysroot}/lib/lean")
+  endif()
+
+  set(LAKE_EXECUTABLE "${LAKE_EXECUTABLE}" PARENT_SCOPE)
+  set(LEAN_SYSROOT "${lean_sysroot}" PARENT_SCOPE)
+  set(LEAN_INCLUDE_DIR "${lean_include_dir}" PARENT_SCOPE)
+  set(LEAN_SHARED_LIBRARY "${lean_shared_library}" PARENT_SCOPE)
+  set(LEAN_EXPECTED_VERSION "${expected_lean_version}" PARENT_SCOPE)
+endfunction()

conanfile.py

@@ -1,4 +1,5 @@
 from conan import ConanFile
+from conan.errors import ConanInvalidConfiguration
 from conan.tools.cmake import CMake, CMakeToolchain, cmake_layout
 import re
 
@@ -14,6 +15,7 @@ class Xrpl(ConanFile):
         'assertions': [True, False],
         'coverage': [True, False],
         'fPIC': [True, False],
+        'formal_verification': [True, False],
         'jemalloc': [True, False],
         'rocksdb': [True, False],
         'shared': [True, False],
@@ -45,6 +47,7 @@ class Xrpl(ConanFile):
         'assertions': False,
         'coverage': False,
         'fPIC': True,
+        'formal_verification': False,
         'jemalloc': False,
         'rocksdb': True,
         'shared': False,
@@ -110,6 +113,14 @@ class Xrpl(ConanFile):
         if self.settings.compiler == 'apple-clang':
             self.options['boost/*'].visibility = 'global'
 
+    def validate(self):
+        if self.options.formal_verification and (
+            not self.options.tests or not self.options.xrpld
+        ):
+            raise ConanInvalidConfiguration(
+                'formal_verification=True requires tests=True and xrpld=True'
+            )
+
     def requirements(self):
         # Force sqlite3 version to avoid conflicts with soci
         self.requires('sqlite3/3.47.0', override=True)
@@ -132,6 +143,18 @@ class Xrpl(ConanFile):
         'cfg/*',
         'cmake/*',
         'external/*',
+        'formal_verification/*.json',
+        'formal_verification/*.lean',
+        'formal_verification/*.md',
+        'formal_verification/*.toml',
+        'formal_verification/lean-toolchain',
+        'formal_verification/XahauConsensus/*.lean',
+        '!formal_verification/.lake',
+        '!formal_verification/.lake/*',
+        '!formal_verification/.lake/**',
+        '!formal_verification/**/.lake',
+        '!formal_verification/**/.lake/*',
+        '!formal_verification/**/.lake/**',
         'include/*',
         'src/*',
     )
@@ -148,6 +171,7 @@ class Xrpl(ConanFile):
         tc.variables['tests'] = self.options.tests
         tc.variables['assert'] = self.options.assertions
         tc.variables['coverage'] = self.options.coverage
+        tc.variables['formal_verification'] = self.options.formal_verification
         tc.variables['jemalloc'] = self.options.jemalloc
         tc.variables['rocksdb'] = self.options.rocksdb
         tc.variables['BUILD_SHARED_LIBS'] = self.options.shared
@@ -163,6 +187,11 @@ class Xrpl(ConanFile):
         cmake.build()
 
     def package(self):
+        if self.options.formal_verification:
+            raise ConanInvalidConfiguration(
+                'formal_verification=True is a local/CI test build option and '
+                'is not supported for Conan packages'
+            )
         cmake = CMake(self)
         cmake.verbose = True
         cmake.install()

formal_verification/.gitignore

@@ -0,0 +1 @@
+/.lake

formal_verification/README.md

@@ -0,0 +1,166 @@
+# xahau_consensus
+
+Lean proofs for small Xahau consensus invariants.
+
+This package is intentionally narrow. It does **not** try to verify the C++
+implementation directly. It mirrors small formulas and decision ladders from
+the consensus-extension code so the safety arguments can be checked as theorems
+instead of repeatedly re-derived in review notes.
+
+Current modules:
+
+- `XahauConsensus.Threshold`
+  - mirrors `calculateParticipantThreshold`
+  - proves the Tier-2 intersection inequality:
+    `count + floor(count / 5) < 2 * participantThreshold count`
+  - proves the threshold is minimal for that strict inequality
+  - proves the original-view threshold remains safe when nUNL shrinks the
+    effective view
+  - includes the `original=10`, `effective=8` regression example showing why
+    using the effective view for the Tier-2 floor is forkable
+  - proves `participantThreshold count <= quorumThreshold count` for
+    non-empty views
+  - distinguishes raw formula helpers from the live safety-wrapped gate
+    thresholds used by `ConsensusExtensions`
+- `XahauConsensus.ThresholdFacts`
+  - records small-network values and band-empty/band-present examples
+  - proves exact multiple-of-five behavior
+  - proves threshold monotonicity facts
+- `XahauConsensus.SixtyPercent`
+  - defines a naive `ceil(60%)` threshold
+  - proves naive 60% is unsafe at exact multiples of five
+  - proves the live derived floor is one higher there and restores strict
+    intersection safety
+- `XahauConsensus.Intersection`
+  - proves the abstract cardinality argument behind quorum intersection
+  - shows two threshold-sized cohorts must overlap above the fault bound
+    whenever `n + f < 2t`
+  - specializes that argument to the live participant threshold, including
+    nUNL-shrunk effective views
+- `XahauConsensus.HonestOverlap`
+  - bridges overlap arithmetic to the consensus claim that two cohorts share at
+    least one honest validator
+  - specializes that bridge to the participant threshold and `floor(n/5)` fault
+    bound
+- `XahauConsensus.ViewUniverse`
+  - proves original-view anchoring remains safe under nUNL shrink
+  - separates strict safety from threshold reachability
+  - defines cross-view participant-band presence/absence
+  - shows effective-view thresholds can be unsafe against the original fault
+    bound
+  - shows trusted-superset counting universes erode the intersection margin
+- `XahauConsensus.NunlCap`
+  - models the protocol's ceil-25% nUNL disablement cap
+  - proves 8/6 and 10/8 band collapse examples
+  - records that 10 at max cap has effective view 7, below the original
+    participant floor
+  - records the important counterexample: original `20`, effective `15` does
+    **not** make validator quorum meet the original participant floor
+- `XahauConsensus.SidecarAlignment`
+  - models aligned participant counting for sidecar hashes
+  - proves non-active peers and non-active local publication cannot pad the
+    alignment count
+  - proves changing nonmember reports cannot change quorum alignment
+- `XahauConsensus.EntropySelector`
+  - models the tier-label ladder from `ConsensusExtensions::selectEntropy`
+  - proves non-UNLReport views select fallback
+  - proves the quorum / participant / fallback bands select the expected tier
+- `XahauConsensus.SelectorDeterminism`
+  - models labeled digest output
+  - proves digest payload bytes do not affect the label when consensus metadata
+    is fixed
+  - records examples where changing view provenance or view sizes changes labels
+- `XahauConsensus.ExportGate`
+  - models export's quorum-aligned success rule
+  - models export's sidecar-gate outcome as `proceed` or `retryOrExpire`, with
+    no deterministic fallback signature set
+  - proves missing minority observation does not block a quorum-aligned export
+  - proves `fullObservation` alone cannot change the export decision
+- `XahauConsensus.ExportQuorum`
+  - proves two 80% export quorums overlap above the standard Byzantine bound
+    in nonempty active universes
+  - proves export quorum overlap remains above the original-view Byzantine
+    bound when nUNL shrinkage is within the protocol cap
+  - proves Byzantine validators at the standard bound cannot veto quorum
+  - records concrete overlap margins for 5/10/20-validator universes
+- `XahauConsensus.FinsetIntersection`
+  - uses Mathlib finite sets to prove the cardinality premise behind the
+    arithmetic intersection theorems
+  - specializes that bridge for Tier-2 cohorts, nUNL-shrunk cohorts, and export
+    80% quorums
+- `XahauConsensus.Invariants`
+  - restates cross-module design contracts in one place
+  - pins the live safety-wrapped threshold relationship
+  - proves the cross-view entropy gate is exactly the selector's non-fallback
+    boundary
+  - pins non-UNLReport fallback and export full-observation independence
+
+Run:
+
+```sh
+~/.elan/bin/lake build
+```
+
+## Optional C++ cross-checks
+
+The xahaud CMake build can also compile a Lean-backed unit-test path, but it is
+off by default and is not part of normal release builds:
+
+Install Lean through `elan` first. The CMake integration intentionally keeps the
+tooling rule simple: when `formal_verification=ON`, it looks for `lake` on
+`PATH` or in `~/.elan/bin`, asks that Lake environment to run `lean --version`,
+verifies the exact version specified by this package's `lean-toolchain`, then
+asks Lake for `LEAN_SYSROOT` and checks that `lean.h` and `libleanshared`
+exist.
+
+```sh
+conan install . --output-folder=build-formal --build=missing \
+  -s build_type=Release \
+  -o '&:tests=True' \
+  -o '&:xrpld=True' \
+  -o '&:formal_verification=True'
+
+cmake -S . -B build-formal-cmake \
+  -DCMAKE_TOOLCHAIN_FILE=$PWD/build-formal/build/generators/conan_toolchain.cmake \
+  -Dtests=ON \
+  -Dxrpld=ON \
+  -Dformal_verification=ON
+
+cmake --build build-formal-cmake --target rippled
+./build-formal-cmake/rippled --unittest=LeanConsensus
+```
+
+This path currently supports native test builds only. It builds
+`XahauConsensus:static`, links the resulting Lean archive and runtime into the
+test binary, and runs C++ drift tests over selected scalar formulas and helper
+predicates. Some checks compare directly to named production helpers; others are
+review-oriented safety predicates computed from those helpers. The exported
+surface is intentionally scalar and reviewable:
+
+- Byzantine bound, participant threshold, and validator quorum threshold.
+- The safety-wrapped zero-view thresholds used by the live gates.
+- The cross-view entropy gate threshold, with effective and original view
+  denominators kept separate.
+- The entropy tier selector policy for `(fromUNLReport, participantCount,
+  effectiveView, originalView)`.
+- Sidecar aligned-participant counting, full-observation, quorum-aligned
+  predicates, and active-view mask-counting samples.
+- Export's quorum-only sidecar-gate proceed predicate, where `fullObservation`
+  is diagnostic rather than success-gating; a small final-apply snapshot model
+  makes explicit that gate proceed is not the same as closed-ledger
+  `Export::doApply` success.
+- NegativeUNL cap/effective-view arithmetic.
+- View-universe safety predicates and naive-60% regression anchors.
+
+This is still a model-to-code cross-check, not a proof that the C++ implements
+the Lean model. Its value is narrower and practical: if a production formula,
+decision ladder, or helper predicate changes without the formal model changing
+too, the gated unit test fails. The formal CMake target invokes Lake on each
+formal-enabled `rippled` build and lets Lake decide whether its own artifacts
+are current; CMake does not trust an existing source-tree archive by timestamp.
+Lake still writes build artifacts under the Lean workspace's `.lake/`
+directory, and the Conan recipe intentionally excludes that directory from
+exported sources, so keep this option as a local/CI confidence build rather
+than a release packaging input. The Conan recipe rejects
+`formal_verification=True` unless `tests=True` and `xrpld=True`, and refuses to
+package formal-enabled builds.

formal_verification/ROADMAP.md

@@ -0,0 +1,32 @@
+# Xahau Lean Roadmap
+
+This package should stay focused on invariants that are compact enough to be
+reviewable and stable enough to mirror from C++.
+
+Good targets:
+
+1. Threshold arithmetic
+   - Tier-2 participant threshold formula
+   - quorum threshold relation
+   - nUNL original-view anchoring
+   - small-network boundary examples
+2. Sidecar alignment
+   - active-view-only counting
+   - quorum-aligned predicate
+   - full-observation as diagnostic vs success precondition where applicable
+3. Entropy selector
+   - non-UNLReport fallback
+   - tier ladder from agreed participant count
+   - no local pending-state dependency in the tier decision
+4. Export gate
+   - quorum-aligned success without full observation
+   - no deterministic fallback value
+   - retry/expire as liveness behavior, not ledger-content substitution
+
+Poor targets for this package:
+
+- direct verification of C++ implementation details
+- wall-clock timing and network scheduling liveness
+- full ledger execution semantics
+
+Those belong in C++ tests, CSF/testnet scenarios, or a dedicated temporal model.

formal_verification/XahauConsensus.lean

@@ -0,0 +1,17 @@
+-- This module serves as the root of the `XahauConsensus` library.
+-- Import modules here that should be built as part of the library.
+import XahauConsensus.Threshold
+import XahauConsensus.ThresholdFacts
+import XahauConsensus.SixtyPercent
+import XahauConsensus.Intersection
+import XahauConsensus.HonestOverlap
+import XahauConsensus.ViewUniverse
+import XahauConsensus.NunlCap
+import XahauConsensus.SidecarAlignment
+import XahauConsensus.EntropySelector
+import XahauConsensus.SelectorDeterminism
+import XahauConsensus.ExportGate
+import XahauConsensus.ExportQuorum
+import XahauConsensus.FinsetIntersection
+import XahauConsensus.Invariants
+import XahauConsensus.FFI

formal_verification/XahauConsensus/EntropySelector.lean

@@ -0,0 +1,74 @@
+import XahauConsensus.Threshold
+
+namespace XahauConsensus
+
+inductive EntropyTier where
+  | consensusFallback
+  | participantAligned
+  | validatorQuorum
+  deriving DecidableEq, Repr
+
+/-- Minimal model of `ConsensusExtensions::selectEntropy`'s network,
+non-failed, non-empty tier ladder.
+
+The real C++ also computes a digest. This model deliberately focuses on the
+part that can fork by labeling the same agreed set differently: the tier
+decision from `(fromUNLReport, participantCount, effectiveView, originalView)`.
+It does not model the standalone development shortcut, timeout-driven
+`entropyFailed_` downgrade, or empty-map fallback; those paths all bypass or
+downgrade this ladder rather than producing a stronger non-fallback label.
+-/
+def selectEntropyTier
+    (fromUNLReport : Bool)
+    (participantCount effectiveView originalView : Nat) : EntropyTier :=
+  if !fromUNLReport then
+    EntropyTier.consensusFallback
+  else if participantCount >= safeQuorumThreshold effectiveView then
+    EntropyTier.validatorQuorum
+  else if participantCount >= safeParticipantThreshold originalView then
+    EntropyTier.participantAligned
+  else
+    EntropyTier.consensusFallback
+
+/-- Non-standalone nodes must fail closed to fallback until the validator view
+is ledger-anchored by a UNLReport. -/
+theorem no_unl_report_selects_fallback
+    (participantCount effectiveView originalView : Nat) :
+    selectEntropyTier false participantCount effectiveView originalView =
+      EntropyTier.consensusFallback := by
+  rfl
+
+/-- At or above the effective-view quorum threshold, the ladder selects the
+strongest entropy tier. -/
+theorem quorum_count_selects_validator_quorum
+    {participantCount effectiveView originalView : Nat}
+    (hQuorum : safeQuorumThreshold effectiveView <= participantCount) :
+    selectEntropyTier true participantCount effectiveView originalView =
+      EntropyTier.validatorQuorum := by
+  unfold selectEntropyTier
+  simp [hQuorum]
+
+/-- Below validator quorum but at or above the original-view participant floor,
+the ladder selects Tier 2. -/
+theorem participant_band_selects_tier2
+    {participantCount effectiveView originalView : Nat}
+    (hBelowQuorum : participantCount < safeQuorumThreshold effectiveView)
+    (hParticipant : safeParticipantThreshold originalView <= participantCount) :
+    selectEntropyTier true participantCount effectiveView originalView =
+      EntropyTier.participantAligned := by
+  unfold selectEntropyTier
+  simp [Nat.not_le_of_gt hBelowQuorum, hParticipant]
+
+/-- Below both thresholds, the ladder falls back. -/
+theorem below_participant_floor_selects_fallback
+    {participantCount effectiveView originalView : Nat}
+    (hBelowQuorum : participantCount < safeQuorumThreshold effectiveView)
+    (hBelowParticipant : participantCount < safeParticipantThreshold originalView) :
+    selectEntropyTier true participantCount effectiveView originalView =
+      EntropyTier.consensusFallback := by
+  unfold selectEntropyTier
+  simp [
+    Nat.not_le_of_gt hBelowQuorum,
+    Nat.not_le_of_gt hBelowParticipant]
+
+end XahauConsensus

formal_verification/XahauConsensus/ExportGate.lean

@@ -0,0 +1,139 @@
+namespace XahauConsensus
+
+/-- Minimal model of the sidecar export gate.
+
+`alignedParticipants` is the number of participants observed on the export
+sidecar, `quorumThreshold` is the required aligned count, and
+`fullObservation` records whether every participant was observed. The C++ gate
+must use quorum alignment for success; full observation is only diagnostic.
+-/
+structure ExportGate where
+  alignedParticipants : Nat
+  quorumThreshold : Nat
+  fullObservation : Bool
+  deriving DecidableEq, Repr
+
+/-- Export sidecar-gate outcome. This is not the final `Export::doApply`
+result: closed-ledger apply re-validates the frozen agreed signature snapshot
+before it can create a shadow ticket. -/
+inductive ExportOutcome where
+  | proceed
+  | retryOrExpire
+  deriving DecidableEq, Repr
+
+/-- The success predicate used by export: enough participants are aligned. -/
+def ExportGate.quorumAligned (gate : ExportGate) : Bool :=
+  decide (gate.quorumThreshold <= gate.alignedParticipants)
+
+/-- Export proceeds exactly when quorum alignment is met. -/
+def ExportGate.proceed (gate : ExportGate) : Bool :=
+  gate.quorumAligned
+
+/-- Export's externally visible decision shape. -/
+def ExportGate.outcome (gate : ExportGate) : ExportOutcome :=
+  if gate.proceed then ExportOutcome.proceed else ExportOutcome.retryOrExpire
+
+/-- Minimal model of the additional closed-ledger apply preconditions.
+
+The sidecar gate only proves that one `exportSigSetHash` had quorum alignment.
+Network-mode `Export::doApply` then independently requires a ledger-anchored
+validator view, no convergence failure for the round, a frozen agreed sidecar
+map, a parseable/valid signature set, and enough verified signers in that map.
+The model intentionally excludes cryptography and metadata construction; it
+exists to prevent reading `ExportGate.proceed` as final apply success.
+-/
+structure ExportApplySnapshot where
+  fromUNLReport : Bool
+  convergenceFailed : Bool
+  agreedSetPresent : Bool
+  agreedSetValid : Bool
+  signerCount : Nat
+  quorumThreshold : Nat
+  deriving DecidableEq, Repr
+
+/-- Closed-ledger apply can use only a valid, frozen agreed sidecar snapshot. -/
+def ExportApplySnapshot.validAgreedSnapshot
+    (snapshot : ExportApplySnapshot) : Bool :=
+  snapshot.fromUNLReport &&
+    !snapshot.convergenceFailed &&
+    snapshot.agreedSetPresent &&
+    snapshot.agreedSetValid &&
+    decide (snapshot.quorumThreshold <= snapshot.signerCount)
+
+/-- Minimal network-mode apply decision: valid agreed snapshot applies; all
+other cases retry or expire. -/
+def ExportApplySnapshot.outcome
+    (snapshot : ExportApplySnapshot) : ExportOutcome :=
+  if snapshot.validAgreedSnapshot then
+    ExportOutcome.proceed
+  else
+    ExportOutcome.retryOrExpire
+
+theorem apply_success_iff_valid_agreed_snapshot
+    (snapshot : ExportApplySnapshot) :
+    snapshot.outcome = ExportOutcome.proceed ↔
+      snapshot.validAgreedSnapshot = true := by
+  unfold ExportApplySnapshot.outcome
+  by_cases h : snapshot.validAgreedSnapshot <;> simp [h]
+
+/-- Gate success alone is not final apply success. For example, the sidecar
+gate may have quorum alignment while the final apply path has no frozen agreed
+sidecar map available and therefore retries. -/
+theorem gate_proceed_does_not_imply_apply_success :
+    ∃ gate : ExportGate, ∃ snapshot : ExportApplySnapshot,
+      ExportGate.proceed gate = true ∧
+        ExportApplySnapshot.outcome snapshot =
+          ExportOutcome.retryOrExpire := by
+  refine ⟨
+    ExportGate.mk 4 4 false,
+    ExportApplySnapshot.mk true false false true 4 4,
+    ?_,
+    ?_⟩ <;> rfl
+
+/-- A missing minority, represented by `fullObservation = false`, does not
+prevent export when the quorum threshold is met. -/
+theorem missing_minority_does_not_prevent_proceed
+    {alignedParticipants quorumThreshold : Nat}
+    (hQuorum : quorumThreshold <= alignedParticipants) :
+    (ExportGate.mk alignedParticipants quorumThreshold false).proceed = true := by
+  unfold ExportGate.proceed ExportGate.quorumAligned
+  simp [hQuorum]
+
+theorem missing_minority_proceeds
+    {alignedParticipants quorumThreshold : Nat}
+    (hQuorum : quorumThreshold <= alignedParticipants) :
+    (ExportGate.mk alignedParticipants quorumThreshold false).outcome =
+      ExportOutcome.proceed := by
+  unfold ExportGate.outcome
+  simp [missing_minority_does_not_prevent_proceed hQuorum]
+
+/-- Export must not proceed below the aligned-participant quorum threshold. -/
+theorem below_quorum_does_not_proceed
+    {alignedParticipants quorumThreshold : Nat}
+    (fullObservation : Bool)
+    (hBelow : alignedParticipants < quorumThreshold) :
+    (ExportGate.mk alignedParticipants quorumThreshold fullObservation).proceed =
+      false := by
+  unfold ExportGate.proceed ExportGate.quorumAligned
+  simp [Nat.not_le_of_gt hBelow]
+
+/-- Below quorum, export retries or expires. There is no deterministic fallback
+signature set analogous to RNG's Tier 1 fallback digest. -/
+theorem below_quorum_retries_or_expires
+    {alignedParticipants quorumThreshold : Nat}
+    (fullObservation : Bool)
+    (hBelow : alignedParticipants < quorumThreshold) :
+    (ExportGate.mk alignedParticipants quorumThreshold fullObservation).outcome =
+      ExportOutcome.retryOrExpire := by
+  unfold ExportGate.outcome
+  simp [below_quorum_does_not_proceed fullObservation hBelow]
+
+/-- Flipping only the diagnostic `fullObservation` field cannot change the
+export decision. -/
+theorem changing_fullObservation_alone_does_not_change_proceed
+    (alignedParticipants quorumThreshold : Nat) :
+    (ExportGate.mk alignedParticipants quorumThreshold true).proceed =
+      (ExportGate.mk alignedParticipants quorumThreshold false).proceed := by
+  rfl
+
+end XahauConsensus

formal_verification/XahauConsensus/ExportQuorum.lean

@@ -0,0 +1,254 @@
+import XahauConsensus.Intersection
+import XahauConsensus.NunlCap
+import XahauConsensus.ThresholdFacts
+
+namespace XahauConsensus
+
+/-!
+Nat-cardinality arithmetic for export sidecar quorum uniqueness.
+
+The model deliberately stays at the level used by `Intersection.lean`:
+
+* `n` is the active validator universe size.
+* `a` and `b` are the numbers of validators supporting two export sidecar
+  hashes in that same universe.
+* `overlap` is the size of the intersection between those two support sets.
+* `faultyOverlap + honestOverlap = overlap` splits that intersection.
+
+No `Finset` structure is needed here; callers supply the usual
+inclusion-exclusion cardinality inequality `a + b <= n + overlap`.
+-/
+
+theorem disabled_le_cap_mul_four_le
+    {originalView disabled : Nat}
+    (hCap : disabled <= disabledCap originalView) :
+    disabled * 4 <= originalView + 3 := by
+  unfold disabledCap ceilDiv at hCap
+  have hFour : 0 < 4 := by decide
+  simp at hCap
+  have hMul :=
+    (Nat.le_div_iff_mul_le hFour).mp hCap
+  omega
+
+theorem quorumThreshold_mul_five_ge_four_mul (n : Nat) :
+    4 * n <= 5 * quorumThreshold n := by
+  unfold quorumThreshold
+  have hHundred : 0 < 100 := by decide
+  have hDiv :
+      (n * 80 + 99) / 100 <= (n * 80 + 99) / 100 :=
+    Nat.le_refl _
+  have hBound :=
+    (Nat.div_le_iff_le_mul hHundred).mp hDiv
+  omega
+
+theorem byzantineBound_mul_five_le (n : Nat) :
+    byzantineBound n * 5 <= n := by
+  unfold byzantineBound
+  exact Nat.div_mul_le_self n 5
+
+/-- Two 80% export quorums in one active universe overlap by at least
+`2 * quorumThreshold n - n`. -/
+theorem two_export_quorums_overlap_lower_bound
+    {n a b overlap : Nat}
+    (hCardinality : a + b <= n + overlap)
+    (hA : quorumThreshold n <= a)
+    (hB : quorumThreshold n <= b) :
+    2 * quorumThreshold n - n <= overlap := by
+  omega
+
+/-- The 80% quorum threshold is intersection-safe against the standard
+`floor(n / 5)` fault bound for every nonempty active universe. -/
+theorem quorumThreshold_intersection_safe
+    {n : Nat} (hPositive : 0 < n) :
+    n + byzantineBound n < 2 * quorumThreshold n := by
+  unfold quorumThreshold byzantineBound
+  omega
+
+/-- The unconditional version is false: the empty active universe has raw
+quorum threshold zero, so there is no strict intersection margin. -/
+theorem quorumThreshold_empty_not_intersection_safe :
+    ¬ 0 + byzantineBound 0 < 2 * quorumThreshold 0 := by
+  native_decide
+
+/-- Two export sidecar hashes both clearing 80% quorum in the same nonempty
+active universe must have overlap larger than the standard fault bound. -/
+theorem export_hash_quorums_overlap_gt_byzantine
+    {n a b overlap : Nat}
+    (hPositive : 0 < n)
+    (hCardinality : a + b <= n + overlap)
+    (hA : quorumThreshold n <= a)
+    (hB : quorumThreshold n <= b) :
+    byzantineBound n < overlap := by
+  exact overlap_gt_fault_of_two_threshold_cohorts
+    hCardinality
+    hA
+    hB
+    (quorumThreshold_intersection_safe hPositive)
+
+/-- If the overlap between two quorum-clearing export hashes is split into
+faulty and honest validators, and at most `floor(n / 5)` validators in that
+overlap are faulty, then the overlap contains an honest validator. -/
+theorem export_hash_quorums_force_honest_overlap
+    {n a b overlap faultyOverlap honestOverlap : Nat}
+    (hPositive : 0 < n)
+    (hCardinality : a + b <= n + overlap)
+    (hA : quorumThreshold n <= a)
+    (hB : quorumThreshold n <= b)
+    (hSplit : overlap = faultyOverlap + honestOverlap)
+    (hFaulty : faultyOverlap <= byzantineBound n) :
+    0 < honestOverlap := by
+  have hOverlap :
+      byzantineBound n < overlap :=
+    export_hash_quorums_overlap_gt_byzantine
+      hPositive
+      hCardinality
+      hA
+      hB
+  omega
+
+/-- Export quorum intersection remains above the original-view Byzantine bound
+when nUNL shrinkage is within the protocol's ceil-25% cap. -/
+theorem export_quorum_intersection_safe_under_nunl_cap
+    {originalView effectiveView disabled : Nat}
+    (hEffective : effectiveView = originalView - disabled)
+    (hCap : disabled <= disabledCap originalView)
+    (hPositive : 0 < effectiveView) :
+    effectiveView + byzantineBound originalView <
+      2 * quorumThreshold effectiveView := by
+  have hCapBound :
+      disabled * 4 <= originalView + 3 :=
+    disabled_le_cap_mul_four_le hCap
+  have hQuorumBound :
+      4 * effectiveView <= 5 * quorumThreshold effectiveView :=
+    quorumThreshold_mul_five_ge_four_mul effectiveView
+  have hByzBound :
+      byzantineBound originalView * 5 <= originalView :=
+    byzantineBound_mul_five_le originalView
+  omega
+
+/-- Two export sidecar hashes both clearing 80% quorum in an nUNL-shrunk
+effective view must still overlap above the original-view Byzantine bound,
+provided the shrinkage stays within the protocol cap. -/
+theorem export_hash_quorums_overlap_gt_original_byzantine_under_nunl_cap
+    {originalView effectiveView disabled a b overlap : Nat}
+    (hEffective : effectiveView = originalView - disabled)
+    (hCap : disabled <= disabledCap originalView)
+    (hPositive : 0 < effectiveView)
+    (hCardinality : a + b <= effectiveView + overlap)
+    (hA : quorumThreshold effectiveView <= a)
+    (hB : quorumThreshold effectiveView <= b) :
+    byzantineBound originalView < overlap := by
+  exact overlap_gt_fault_of_two_threshold_cohorts
+    hCardinality
+    hA
+    hB
+    (export_quorum_intersection_safe_under_nunl_cap
+      hEffective
+      hCap
+      hPositive)
+
+/-- A Byzantine minority at the standard bound cannot veto export quorum:
+after removing `floor(n / 5)` validators, enough validators remain to meet the
+80% quorum threshold. -/
+theorem byzantineBound_cannot_veto_quorum (n : Nat) :
+    byzantineBound n + quorumThreshold n <= n := by
+  unfold byzantineBound quorumThreshold
+  omega
+
+/-- Equivalent no-veto form using subtraction. -/
+theorem quorumThreshold_le_universe_minus_byzantineBound (n : Nat) :
+    quorumThreshold n <= n - byzantineBound n := by
+  have hNoVeto := byzantineBound_cannot_veto_quorum n
+  omega
+
+/-- Concrete regression anchor: in a 5-validator active universe, two 80%
+export quorums overlap in at least three validators. -/
+theorem export_quorum_five_overlap_at_least_three
+    {a b overlap : Nat}
+    (hCardinality : a + b <= 5 + overlap)
+    (hA : quorumThreshold 5 <= a)
+    (hB : quorumThreshold 5 <= b) :
+    3 <= overlap := by
+  have hLower :
+      2 * quorumThreshold 5 - 5 <= overlap :=
+    two_export_quorums_overlap_lower_bound
+      hCardinality
+      hA
+      hB
+  have hExact : 2 * quorumThreshold 5 - 5 = 3 := by
+    native_decide
+  omega
+
+/-- Concrete regression anchor: in a 10-validator active universe, two 80%
+export quorums overlap in at least six validators. -/
+theorem export_quorum_ten_overlap_at_least_six
+    {a b overlap : Nat}
+    (hCardinality : a + b <= 10 + overlap)
+    (hA : quorumThreshold 10 <= a)
+    (hB : quorumThreshold 10 <= b) :
+    6 <= overlap := by
+  have hLower :
+      2 * quorumThreshold 10 - 10 <= overlap :=
+    two_export_quorums_overlap_lower_bound
+      hCardinality
+      hA
+      hB
+  have hExact : 2 * quorumThreshold 10 - 10 = 6 := by
+    native_decide
+  omega
+
+/-- Concrete regression anchor: in a 20-validator active universe, two 80%
+export quorums overlap in at least twelve validators. -/
+theorem export_quorum_twenty_overlap_at_least_twelve
+    {a b overlap : Nat}
+    (hCardinality : a + b <= 20 + overlap)
+    (hA : quorumThreshold 20 <= a)
+    (hB : quorumThreshold 20 <= b) :
+    12 <= overlap := by
+  have hLower :
+      2 * quorumThreshold 20 - 20 <= overlap :=
+    two_export_quorums_overlap_lower_bound
+      hCardinality
+      hA
+      hB
+  have hExact : 2 * quorumThreshold 20 - 20 = 12 := by
+    native_decide
+  omega
+
+/-- On exact multiples of five, two 80% export quorums overlap in at least
+`3 * k` validators. -/
+theorem export_quorum_five_mul_overlap_at_least_three_mul
+    {k a b overlap : Nat}
+    (hCardinality : a + b <= 5 * k + overlap)
+    (hA : quorumThreshold (5 * k) <= a)
+    (hB : quorumThreshold (5 * k) <= b) :
+    3 * k <= overlap := by
+  have hLower :
+      2 * quorumThreshold (5 * k) - 5 * k <= overlap :=
+    two_export_quorums_overlap_lower_bound
+      hCardinality
+      hA
+      hB
+  rw [quorumThreshold_five_mul] at hLower
+  omega
+
+/-- On exact multiples of five, quorum overlap strictly exceeds the standard
+fault bound by at least `2 * k`. For `k = 0` this is only a non-strict
+difference statement; strict safety is provided by
+`export_hash_quorums_overlap_gt_byzantine` for nonempty universes. -/
+theorem export_quorum_five_mul_overlap_margin
+    {k a b overlap : Nat}
+    (hCardinality : a + b <= 5 * k + overlap)
+    (hA : quorumThreshold (5 * k) <= a)
+    (hB : quorumThreshold (5 * k) <= b) :
+    byzantineBound (5 * k) + 2 * k <= overlap := by
+  have hOverlap :
+      3 * k <= overlap :=
+    export_quorum_five_mul_overlap_at_least_three_mul
+      hCardinality
+      hA
+      hB
+  rw [byzantineBound_five_mul]
+  omega
+
+end XahauConsensus

formal_verification/XahauConsensus/FFI.lean

@@ -0,0 +1,188 @@
+import XahauConsensus.Threshold
+import XahauConsensus.Invariants
+import XahauConsensus.NunlCap
+import XahauConsensus.SidecarAlignment
+import XahauConsensus.ViewUniverse
+import XahauConsensus.ExportQuorum
+import XahauConsensus.SixtyPercent
+
+namespace XahauConsensus
+
+/-! Scalar C ABI exports used by the optional C++ drift tests.
+
+These functions intentionally expose only plain integer formulas. The broader
+Lean project proves properties about these definitions; the C++ tests then
+check that selected production formulas and helper predicates still compute the
+same values.
+-/
+
+-- @@start ffi-scalar-export-surface
+@[export xahau_byzantine_bound]
+def xahauByzantineBound (count : UInt64) : UInt64 :=
+  (byzantineBound count.toNat).toUInt64
+
+@[export xahau_participant_threshold]
+def xahauParticipantThreshold (count : UInt64) : UInt64 :=
+  (participantThreshold count.toNat).toUInt64
+
+@[export xahau_quorum_threshold]
+def xahauQuorumThreshold (count : UInt64) : UInt64 :=
+  (quorumThreshold count.toNat).toUInt64
+
+@[export xahau_safe_quorum_threshold]
+def xahauSafeQuorumThreshold (count : UInt64) : UInt64 :=
+  (safeQuorumThreshold count.toNat).toUInt64
+
+@[export xahau_safe_participant_threshold]
+def xahauSafeParticipantThreshold (count : UInt64) : UInt64 :=
+  (safeParticipantThreshold count.toNat).toUInt64
+
+@[export xahau_entropy_gate_threshold_for_view]
+def xahauEntropyGateThresholdForView
+    (effectiveView originalView : UInt64) : UInt64 :=
+  (entropyGateThresholdForView effectiveView.toNat originalView.toNat).toUInt64
+
+def entropyTierCode : EntropyTier → UInt8
+  | EntropyTier.consensusFallback => 1
+  | EntropyTier.participantAligned => 2
+  | EntropyTier.validatorQuorum => 3
+
+@[export xahau_select_entropy_tier]
+def xahauSelectEntropyTier
+    (fromUNLReport participantCount effectiveView originalView : UInt64) : UInt8 :=
+  entropyTierCode <|
+    selectEntropyTier
+      (fromUNLReport != 0)
+      participantCount.toNat
+      effectiveView.toNat
+      originalView.toNat
+
+@[export xahau_aligned_participants]
+def xahauAlignedParticipants
+    (aligned localIsMember localPublished : UInt64) : UInt64 :=
+  (alignedParticipants
+      aligned.toNat
+      (localIsMember != 0)
+      (localPublished != 0)).toUInt64
+
+@[export xahau_quorum_aligned]
+def xahauQuorumAligned
+    (threshold aligned localIsMember localPublished : UInt64) : UInt8 :=
+  if quorumAligned
+      threshold.toNat
+      aligned.toNat
+      (localIsMember != 0)
+      (localPublished != 0) then
+    1
+  else
+    0
+
+@[export xahau_full_observation]
+def xahauFullObservation (peersSeen txConverged : UInt64) : UInt8 :=
+  if fullObservation peersSeen.toNat txConverged.toNat then 1 else 0
+
+@[export xahau_export_gate_proceed]
+def xahauExportGateProceed
+    (alignedParticipants quorumThreshold fullObservation : UInt64) : UInt8 :=
+  if (ExportGate.mk
+        alignedParticipants.toNat
+        quorumThreshold.toNat
+        (fullObservation != 0)).proceed then
+    1
+  else
+    0
+
+
+@[export xahau_strict_intersection_safe]
+def xahauStrictIntersectionSafe
+    (activeView byzantineUniverse threshold : UInt64) : UInt8 :=
+  if activeView.toNat + byzantineBound byzantineUniverse.toNat <
+      2 * threshold.toNat then
+    1
+  else
+    0
+
+@[export xahau_nonvacuous_strict_intersection_safe]
+def xahauNonvacuousStrictIntersectionSafe
+    (activeView byzantineUniverse threshold : UInt64) : UInt8 :=
+  if threshold.toNat <= activeView.toNat ∧
+      activeView.toNat + byzantineBound byzantineUniverse.toNat <
+        2 * threshold.toNat then
+    1
+  else
+    0
+
+@[export xahau_participant_band_nonempty]
+def xahauParticipantBandNonempty
+    (effectiveView originalView : UInt64) : UInt8 :=
+  if participantThreshold originalView.toNat < quorumThreshold effectiveView.toNat then
+    1
+  else
+    0
+
+@[export xahau_export_quorum_overlap_lower_bound]
+def xahauExportQuorumOverlapLowerBound (activeView : UInt64) : UInt64 :=
+  (2 * quorumThreshold activeView.toNat - activeView.toNat).toUInt64
+
+@[export xahau_export_quorum_safe_under_nunl_cap]
+def xahauExportQuorumSafeUnderNunlCap
+    (originalView effectiveView disabled : UInt64) : UInt8 :=
+  if effectiveView.toNat = originalView.toNat - disabled.toNat ∧
+      disabled.toNat <= disabledCap originalView.toNat ∧
+      0 < effectiveView.toNat ∧
+      effectiveView.toNat + byzantineBound originalView.toNat <
+        2 * quorumThreshold effectiveView.toNat then
+    1
+  else
+    0
+
+private def maskBit (mask : UInt64) (peer : Nat) : Bool :=
+  ((mask.toNat / (2 ^ peer)) % 2) == 1
+
+@[export xahau_active_aligned_count_mask]
+def xahauActiveAlignedCountMask
+    (count activeMask alignedMask : UInt64) : UInt64 :=
+  (activeAlignedCount
+      (maskBit activeMask)
+      (maskBit alignedMask)
+      count.toNat).toUInt64
+
+@[export xahau_quorum_aligned_mask]
+def xahauQuorumAlignedMask
+    (threshold count activeMask alignedMask localIsMember localPublished : UInt64) : UInt8 :=
+  let aligned :=
+    activeAlignedCount
+      (maskBit activeMask)
+      (maskBit alignedMask)
+      count.toNat
+  if quorumAligned
+      threshold.toNat
+      aligned
+      (localIsMember != 0)
+      (localPublished != 0) then
+    1
+  else
+    0
+
+@[export xahau_naive_sixty_percent_threshold]
+def xahauNaiveSixtyPercentThreshold (count : UInt64) : UInt64 :=
+  (naiveSixtyPercentThreshold count.toNat).toUInt64
+
+@[export xahau_naive_sixty_percent_is_safe]
+def xahauNaiveSixtyPercentIsSafe (count : UInt64) : UInt8 :=
+  if count.toNat + byzantineBound count.toNat <
+      2 * naiveSixtyPercentThreshold count.toNat then
+    1
+  else
+    0
+
+@[export xahau_disabled_cap]
+def xahauDisabledCap (originalView : UInt64) : UInt64 :=
+  (disabledCap originalView.toNat).toUInt64
+
+@[export xahau_effective_view]
+def xahauEffectiveView (originalView disabled : UInt64) : UInt64 :=
+  (effectiveView originalView.toNat disabled.toNat).toUInt64
+-- @@end ffi-scalar-export-surface
+
+end XahauConsensus

formal_verification/XahauConsensus/FinsetIntersection.lean

@@ -0,0 +1,88 @@
+import Mathlib.Data.Finset.Card
+import XahauConsensus.ExportQuorum
+import XahauConsensus.Intersection
+
+namespace XahauConsensus
+
+/-!
+Finite-set bridge for the quorum-intersection arithmetic.
+
+The arithmetic modules prove useful facts from the premise
+`a + b <= n + overlap`. This module discharges that premise for actual finite
+cohorts `A` and `B` that are both subsets of a common validator universe `U`.
+-/
+
+open Finset
+
+/-- Inclusion-exclusion bridge: two finite cohorts inside one universe satisfy
+the cardinality premise used by `Intersection.lean`. -/
+theorem finset_cardinality_bound
+    [DecidableEq α]
+    {U A B : Finset α}
+    (hA : A ⊆ U)
+    (hB : B ⊆ U) :
+    A.card + B.card <= U.card + (A ∩ B).card := by
+  have hUnionSubset : A ∪ B ⊆ U := by
+    intro x hx
+    rcases Finset.mem_union.mp hx with hxA | hxB
+    · exact hA hxA
+    · exact hB hxB
+  have hUnionCard : (A ∪ B).card <= U.card :=
+    Finset.card_le_card hUnionSubset
+  have hInclusion :
+      (A ∪ B).card + (A ∩ B).card = A.card + B.card :=
+    Finset.card_union_add_card_inter A B
+  omega
+
+/-- Set-level Tier-2 form: two participant-threshold cohorts in the same
+validator universe overlap above the Byzantine bound. -/
+theorem finset_participant_threshold_cohorts_overlap_gt_byzantine
+    [DecidableEq α]
+    {U A B : Finset α}
+    (hAUniverse : A ⊆ U)
+    (hBUniverse : B ⊆ U)
+    (hAThreshold : participantThreshold U.card <= A.card)
+    (hBThreshold : participantThreshold U.card <= B.card) :
+    byzantineBound U.card < (A ∩ B).card := by
+  exact participant_threshold_cohorts_overlap_gt_byzantine
+    (finset_cardinality_bound hAUniverse hBUniverse)
+    hAThreshold
+    hBThreshold
+
+/-- nUNL/set-level form: two original-view participant-threshold cohorts in a
+shrunk effective universe still overlap above the original Byzantine bound. -/
+theorem finset_participant_threshold_cohorts_overlap_gt_byzantine_under_shrink
+    [DecidableEq α]
+    {Original Effective A B : Finset α}
+    (hEffectiveSubset : Effective ⊆ Original)
+    (hAUniverse : A ⊆ Effective)
+    (hBUniverse : B ⊆ Effective)
+    (hAThreshold : participantThreshold Original.card <= A.card)
+    (hBThreshold : participantThreshold Original.card <= B.card) :
+    byzantineBound Original.card < (A ∩ B).card := by
+  have hShrink : Effective.card <= Original.card :=
+    Finset.card_le_card hEffectiveSubset
+  exact participant_threshold_cohorts_overlap_gt_byzantine_under_shrink
+    hShrink
+    (finset_cardinality_bound hAUniverse hBUniverse)
+    hAThreshold
+    hBThreshold
+
+/-- Set-level export form: two 80% export sidecar quorums in the same nonempty
+active universe overlap above the standard Byzantine bound. -/
+theorem finset_export_hash_quorums_overlap_gt_byzantine
+    [DecidableEq α]
+    {U A B : Finset α}
+    (hNonempty : 0 < U.card)
+    (hAUniverse : A ⊆ U)
+    (hBUniverse : B ⊆ U)
+    (hAThreshold : quorumThreshold U.card <= A.card)
+    (hBThreshold : quorumThreshold U.card <= B.card) :
+    byzantineBound U.card < (A ∩ B).card := by
+  exact export_hash_quorums_overlap_gt_byzantine
+    hNonempty
+    (finset_cardinality_bound hAUniverse hBUniverse)
+    hAThreshold
+    hBThreshold
+
+end XahauConsensus

formal_verification/XahauConsensus/HonestOverlap.lean

@@ -0,0 +1,70 @@
+import XahauConsensus.Intersection
+
+namespace XahauConsensus
+
+/-!
+Bridge from cardinality arithmetic to the consensus-language statement:
+if cohort overlap is larger than the maximum faulty overlap, then the overlap
+contains at least one honest validator.
+-/
+
+/-- If the overlap is larger than the number of faulty validators in it, then
+some honest validator remains in the overlap. -/
+theorem honest_overlap_exists
+    {overlap faultyInOverlap : Nat}
+    (hFaultyLtOverlap : faultyInOverlap < overlap) :
+    0 < overlap - faultyInOverlap := by
+  omega
+
+/-- If total faulty validators are bounded by `faultBound`, and the overlap is
+larger than `faultBound`, then the overlap contains an honest validator. -/
+theorem honest_overlap_exists_of_fault_bound
+    {overlap faultyInOverlap faultBound : Nat}
+    (hFaultyBound : faultyInOverlap <= faultBound)
+    (hOverlapGtFaultBound : faultBound < overlap) :
+    0 < overlap - faultyInOverlap := by
+  omega
+
+/-- Direct bridge from the abstract two-cohort intersection theorem: two
+threshold-sized cohorts under the strict safety inequality have honest overlap,
+provided faulty validators in the overlap are bounded by `f`.
+-/
+theorem honest_overlap_of_two_threshold_cohorts
+    {n a b overlap threshold faultBound faultyInOverlap : Nat}
+    (hCardinality : a + b <= n + overlap)
+    (hA : threshold <= a)
+    (hB : threshold <= b)
+    (hSafety : n + faultBound < 2 * threshold)
+    (hFaultyBound : faultyInOverlap <= faultBound) :
+    0 < overlap - faultyInOverlap := by
+  have hOverlapGtFaultBound :
+      faultBound < overlap :=
+    overlap_gt_fault_of_two_threshold_cohorts
+      hCardinality
+      hA
+      hB
+      hSafety
+  exact honest_overlap_exists_of_fault_bound
+    hFaultyBound
+    hOverlapGtFaultBound
+
+/-- Direct participant-threshold form: two Tier-2-sized cohorts in the same
+view have honest overlap under the `floor(n/5)` Byzantine bound. -/
+theorem honest_overlap_of_participant_threshold_cohorts
+    {count a b overlap faultyInOverlap : Nat}
+    (hCardinality : a + b <= count + overlap)
+    (hA : participantThreshold count <= a)
+    (hB : participantThreshold count <= b)
+    (hFaultyBound : faultyInOverlap <= byzantineBound count) :
+    0 < overlap - faultyInOverlap := by
+  have hOverlapGtBound :
+      byzantineBound count < overlap :=
+    participant_threshold_cohorts_overlap_gt_byzantine
+      hCardinality
+      hA
+      hB
+  exact honest_overlap_exists_of_fault_bound
+    hFaultyBound
+    hOverlapGtBound
+
+end XahauConsensus

formal_verification/XahauConsensus/Intersection.lean

@@ -0,0 +1,96 @@
+import XahauConsensus.Threshold
+
+namespace XahauConsensus
+
+/-!
+Abstract cardinality arithmetic for quorum intersection arguments.
+
+The variables are plain natural-number cardinalities:
+
+* `n`: universe size
+* `a`, `b`: cohort sizes
+* `o`: overlap size
+* `t`: quorum threshold
+* `f`: tolerated faulty overlap
+
+The shape `a + b <= n + o` captures the inclusion-exclusion upper bound
+without committing to a concrete `Finset` model.
+-/
+
+/-- If two threshold-sized cohorts fit in an `n`-sized universe only by
+overlapping by `o`, and `n + f < 2 * t`, then the overlap is larger than the
+fault bound `f`. -/
+theorem overlap_gt_fault_of_two_threshold_cohorts
+    {n a b o t f : Nat}
+    (hCardinality : a + b <= n + o)
+    (hA : t <= a)
+    (hB : t <= b)
+    (hSafety : n + f < 2 * t) :
+    f < o := by
+  omega
+
+/-- Reviewer-facing contrapositive form: if the overlap is no larger than the
+fault bound, then under the strict safety inequality the two cohorts cannot
+both meet threshold. -/
+theorem not_both_threshold_cohorts_of_overlap_le_fault
+    {n a b o t f : Nat}
+    (hOverlap : o <= f)
+    (hCardinality : a + b <= n + o)
+    (hSafety : n + f < 2 * t) :
+    ¬ (t <= a ∧ t <= b) := by
+  intro hBoth
+  have hStrict :
+      f < o :=
+    overlap_gt_fault_of_two_threshold_cohorts
+      hCardinality hBoth.1 hBoth.2 hSafety
+  omega
+
+/-- Equivalent disjunctive form of the reviewer fact: with insufficient
+overlap, at least one candidate cohort must be below threshold. -/
+theorem overlap_le_fault_forces_cohort_below_threshold
+    {n a b o t f : Nat}
+    (hOverlap : o <= f)
+    (hCardinality : a + b <= n + o)
+    (hSafety : n + f < 2 * t) :
+    a < t ∨ b < t := by
+  have hNotBoth :
+      ¬ (t <= a ∧ t <= b) :=
+    not_both_threshold_cohorts_of_overlap_le_fault
+      hOverlap hCardinality hSafety
+  omega
+
+/-- Direct Tier-2 form: two cohorts at the participant threshold in the same
+original-view universe must overlap by more than the tolerated Byzantine bound.
+-/
+theorem participant_threshold_cohorts_overlap_gt_byzantine
+    {count a b overlap : Nat}
+    (hCardinality : a + b <= count + overlap)
+    (hA : participantThreshold count <= a)
+    (hB : participantThreshold count <= b) :
+    byzantineBound count < overlap := by
+  exact overlap_gt_fault_of_two_threshold_cohorts
+    hCardinality
+    hA
+    hB
+    (participantThreshold_intersection_safe count)
+
+/-- nUNL form: when the effective universe shrinks, the original-view
+participant threshold still forces overlap above the original Byzantine bound.
+-/
+theorem participant_threshold_cohorts_overlap_gt_byzantine_under_shrink
+    {originalView effectiveView a b overlap : Nat}
+    (hShrink : effectiveView <= originalView)
+    (hCardinality : a + b <= effectiveView + overlap)
+    (hA : participantThreshold originalView <= a)
+    (hB : participantThreshold originalView <= b) :
+    byzantineBound originalView < overlap := by
+  exact overlap_gt_fault_of_two_threshold_cohorts
+    hCardinality
+    hA
+    hB
+    (participantThreshold_safe_under_effective_shrink
+      originalView
+      effectiveView
+      hShrink)
+
+end XahauConsensus

formal_verification/XahauConsensus/Invariants.lean

@@ -0,0 +1,112 @@
+import XahauConsensus.Threshold
+import XahauConsensus.EntropySelector
+import XahauConsensus.ExportGate
+
+namespace XahauConsensus
+
+/-!
+Small cross-module invariants that state the design contract in one place.
+
+These do not verify C++ directly. They pin the consensus arguments that the C++
+is intended to implement.
+-/
+
+/-- Same-count band fact: with both thresholds computed from one view size,
+Tier 2 is never stricter than validator quorum. Production nUNL rounds use
+cross-view thresholds instead; see `entropyGateThresholdForView`. -/
+theorem same_count_tier2_not_stricter_than_validator_quorum (count : Nat) :
+    safeParticipantThreshold count <= safeQuorumThreshold count :=
+  safeParticipantThreshold_le_safeQuorumThreshold count
+
+/-- Same-view shorthand: the live entropy gate is the weaker of Tier 2 and
+validator quorum, so it is never above validator quorum. -/
+def entropyGateThresholdModel (count : Nat) : Nat :=
+  min (safeQuorumThreshold count) (safeParticipantThreshold count)
+
+theorem entropy_gate_le_validator_quorum (count : Nat) :
+    entropyGateThresholdModel count <= safeQuorumThreshold count := by
+  unfold entropyGateThresholdModel
+  exact Nat.min_le_left _ _
+
+theorem entropy_gate_le_participant_threshold (count : Nat) :
+    entropyGateThresholdModel count <= safeParticipantThreshold count := by
+  unfold entropyGateThresholdModel
+  exact Nat.min_le_right _ _
+
+/-- Production shape: validator quorum is over the effective post-nUNL view,
+while Tier 2 is over the original pre-nUNL view. -/
+def entropyGateThresholdForView (effectiveView originalView : Nat) : Nat :=
+  min (safeQuorumThreshold effectiveView) (safeParticipantThreshold originalView)
+
+theorem entropy_gate_for_view_le_validator_quorum
+    (effectiveView originalView : Nat) :
+    entropyGateThresholdForView effectiveView originalView <=
+      safeQuorumThreshold effectiveView := by
+  unfold entropyGateThresholdForView
+  exact Nat.min_le_left _ _
+
+theorem entropy_gate_for_view_le_participant_threshold
+    (effectiveView originalView : Nat) :
+    entropyGateThresholdForView effectiveView originalView <=
+      safeParticipantThreshold originalView := by
+  unfold entropyGateThresholdForView
+  exact Nat.min_le_right _ _
+
+/-- The entropy gate is exactly the selector's non-fallback boundary: reaching
+the lower of the validator-quorum and participant-aligned thresholds is enough
+to select a non-fallback tier, and below it the selector falls back. -/
+theorem selectEntropyTier_nonfallback_iff_entropy_gate
+    (participantCount effectiveView originalView : Nat) :
+    selectEntropyTier true participantCount effectiveView originalView ≠
+        EntropyTier.consensusFallback ↔
+      entropyGateThresholdForView effectiveView originalView <=
+        participantCount := by
+  unfold selectEntropyTier entropyGateThresholdForView
+  by_cases hQuorum : safeQuorumThreshold effectiveView <= participantCount
+  · constructor
+    · intro _
+      exact Nat.le_trans (Nat.min_le_left _ _) hQuorum
+    · intro _
+      simp [hQuorum]
+  · by_cases hParticipant :
+      safeParticipantThreshold originalView <= participantCount
+    · constructor
+      · intro _
+        exact Nat.le_trans (Nat.min_le_right _ _) hParticipant
+      · intro _
+        simp [hQuorum, hParticipant]
+    · constructor
+      · intro hNonfallback
+        simp [hQuorum, hParticipant] at hNonfallback
+      · intro hGate
+        have hBelowQuorum :
+            participantCount < safeQuorumThreshold effectiveView :=
+          Nat.lt_of_not_ge hQuorum
+        have hBelowParticipant :
+            participantCount < safeParticipantThreshold originalView :=
+          Nat.lt_of_not_ge hParticipant
+        have hBelowGate :
+            participantCount <
+              min (safeQuorumThreshold effectiveView)
+                (safeParticipantThreshold originalView) :=
+          (Nat.lt_min).mpr ⟨hBelowQuorum, hBelowParticipant⟩
+        exact False.elim (Nat.not_lt_of_ge hGate hBelowGate)
+
+/-- Until the view is ledger-anchored, entropy tier labeling fails closed. -/
+theorem non_unl_report_cannot_mint_nonfallback
+    (participantCount effectiveView originalView : Nat) :
+    selectEntropyTier false participantCount effectiveView originalView =
+      EntropyTier.consensusFallback :=
+  no_unl_report_selects_fallback participantCount effectiveView originalView
+
+/-- Export success is a quorum-alignment property, not a full-observation
+property. -/
+theorem export_success_independent_of_full_observation
+    (alignedParticipants quorumThreshold : Nat) :
+    (ExportGate.mk alignedParticipants quorumThreshold true).proceed =
+      (ExportGate.mk alignedParticipants quorumThreshold false).proceed :=
+  changing_fullObservation_alone_does_not_change_proceed
+    alignedParticipants
+    quorumThreshold
+
+end XahauConsensus

formal_verification/XahauConsensus/NunlCap.lean

@@ -0,0 +1,147 @@
+import XahauConsensus.Threshold
+
+namespace XahauConsensus
+
+/-!
+Arithmetic facts for nUNL-capped view shrinkage.
+
+The examples here intentionally use the original view for the participant
+floor and the effective post-nUNL view for validator quorum.  That is the
+cross-view comparison that matters when disabled validators collapse the space
+between the Tier-2 participant floor and the Tier-3 validator-quorum floor.
+-/
+
+/-- Integer ceiling division, defined defensively for `d = 0`. -/
+def ceilDiv (n d : Nat) : Nat :=
+  if d = 0 then 0 else (n + d - 1) / d
+
+/-- The protocol's ceil-25% nUNL disablement cap for an original validator view. -/
+def disabledCap (originalView : Nat) : Nat :=
+  ceilDiv originalView 4
+
+/-- The post-nUNL effective validator view after `disabled` validators drop. -/
+def effectiveView (originalView disabled : Nat) : Nat :=
+  originalView - disabled
+
+theorem ceilDiv_zero_right (n : Nat) : ceilDiv n 0 = 0 := by
+  simp [ceilDiv]
+
+theorem ceilDiv_four_eight : ceilDiv 8 4 = 2 := by
+  native_decide
+
+theorem ceilDiv_four_ten : ceilDiv 10 4 = 3 := by
+  native_decide
+
+theorem ceilDiv_four_twenty : ceilDiv 20 4 = 5 := by
+  native_decide
+
+theorem disabledCap_eight : disabledCap 8 = 2 := by
+  native_decide
+
+theorem disabledCap_ten : disabledCap 10 = 3 := by
+  native_decide
+
+theorem disabledCap_twenty : disabledCap 20 = 5 := by
+  native_decide
+
+theorem effectiveView_eight_at_disabledCap :
+    effectiveView 8 (disabledCap 8) = 6 := by
+  native_decide
+
+theorem effectiveView_ten_at_disabledCap :
+    effectiveView 10 (disabledCap 10) = 7 := by
+  native_decide
+
+theorem effectiveView_twenty_at_disabledCap :
+    effectiveView 20 (disabledCap 20) = 15 := by
+  native_decide
+
+/-- Original 8 with two disabled validators collapses the participant/quorum band. -/
+theorem band_collapse_original8_effective6 :
+    quorumThreshold 6 = participantThreshold 8 := by
+  native_decide
+
+theorem quorum_original8_effective6_meets_participant_floor :
+    participantThreshold 8 <= quorumThreshold 6 := by
+  native_decide
+
+/-- Original 10 with two disabled validators collapses the participant/quorum band. -/
+theorem band_collapse_original10_effective8 :
+    quorumThreshold 8 = participantThreshold 10 := by
+  native_decide
+
+theorem quorum_original10_effective8_meets_participant_floor :
+    participantThreshold 10 <= quorumThreshold 8 := by
+  native_decide
+
+/-- Original 10 at the full ceil-25% cap leaves effective view 7, below the participant floor. -/
+theorem quorum_original10_effective7_below_participant_floor :
+    quorumThreshold 7 < participantThreshold 10 := by
+  native_decide
+
+theorem max_cap_original10_below_participant_floor :
+    quorumThreshold (effectiveView 10 (disabledCap 10)) <
+      participantThreshold 10 := by
+  native_decide
+
+/-- At original 20, the full ceil-25% cap leaves effective view 15, which is too small. -/
+theorem quorum_original20_effective15_below_participant_floor :
+    quorumThreshold 15 < participantThreshold 20 := by
+  native_decide
+
+theorem quorum_original20_effective15_does_not_meet_participant_floor :
+    ¬ participantThreshold 20 <= quorumThreshold 15 := by
+  native_decide
+
+/-- Original 20 with four disabled validators collapses the participant/quorum band. -/
+theorem band_collapse_original20_effective16 :
+    quorumThreshold 16 = participantThreshold 20 := by
+  native_decide
+
+theorem quorum_original20_effective16_meets_participant_floor :
+    participantThreshold 20 <= quorumThreshold 16 := by
+  native_decide
+
+/-- The ceil-25% cap does not by itself guarantee collapse at size 20. -/
+theorem max_cap_original20_below_participant_floor :
+    quorumThreshold (effectiveView 20 (disabledCap 20)) <
+      participantThreshold 20 := by
+  native_decide
+
+/--
+General cross-view comparison: an effective-view quorum satisfies the
+original-view participant floor whenever that quorum clears the original
+intersection boundary.
+-/
+theorem quorumThreshold_meets_participantThreshold_of_intersection_premise
+    {originalView effectiveView : Nat}
+    (h :
+      originalView + byzantineBound originalView <
+        2 * quorumThreshold effectiveView) :
+    participantThreshold originalView <= quorumThreshold effectiveView := by
+  exact participantThreshold_minimal originalView (quorumThreshold effectiveView) h
+
+/--
+Once the effective-view quorum threshold meets the original-view participant
+floor, any validator count meeting validator quorum also meets the participant
+floor anchored to the original view.
+-/
+theorem validators_meet_participant_floor_of_meet_quorum
+    {originalView effectiveView validators : Nat}
+    (hBand : participantThreshold originalView <= quorumThreshold effectiveView)
+    (hQuorum : quorumThreshold effectiveView <= validators) :
+    participantThreshold originalView <= validators :=
+  Nat.le_trans hBand hQuorum
+
+/-- If cross-view quorum is no higher than the participant floor, the in-between band is empty. -/
+theorem cross_view_participant_band_empty
+    {originalView effectiveView : Nat}
+    (hCollapse : quorumThreshold effectiveView <= participantThreshold originalView) :
+    ¬ ∃ participants,
+      participantThreshold originalView <= participants ∧
+        participants < quorumThreshold effectiveView := by
+  intro hExists
+  rcases hExists with ⟨participants, hParticipant, hBelowQuorum⟩
+  omega
+
+end XahauConsensus

formal_verification/XahauConsensus/SelectorDeterminism.lean

@@ -0,0 +1,64 @@
+import XahauConsensus.EntropySelector
+
+namespace XahauConsensus
+
+/-- A minimal digest model: the payload is opaque to the selector, while the
+label is the entropy tier chosen from the consensus metadata. -/
+structure LabeledDigest (α : Type) where
+  payload : α
+  label : EntropyTier
+  deriving Repr
+
+def labelDigest
+    (fromUNLReport : Bool)
+    (participantCount effectiveView originalView : Nat)
+    (payload : α) : LabeledDigest α :=
+  { payload
+    label :=
+      selectEntropyTier
+        fromUNLReport
+        participantCount
+        effectiveView
+        originalView }
+
+/-- The digest payload itself does not affect the selected tier. The label is
+entirely determined by the consensus metadata. -/
+theorem payload_does_not_affect_tier
+    {α : Type}
+    {payloadA payloadB : α}
+    (fromUNLReport : Bool)
+    (participantCount effectiveView originalView : Nat) :
+    (labelDigest
+        fromUNLReport
+        participantCount
+        effectiveView
+        originalView
+        payloadA).label =
+      (labelDigest
+        fromUNLReport
+        participantCount
+        effectiveView
+        originalView
+        payloadB).label := by
+  rfl
+
+/-- Without a UNLReport anchor the same count and views can receive a different
+label. -/
+theorem label_can_differ_when_fromUNLReport_differs :
+    (labelDigest true 8 10 10 0).label ≠
+      (labelDigest false 8 10 10 0).label := by
+  native_decide
+
+/-- Changing the effective validator view can change the digest label. -/
+theorem label_can_differ_when_effective_view_differs :
+    (labelDigest true 7 8 10 0).label ≠
+      (labelDigest true 7 10 10 0).label := by
+  native_decide
+
+/-- Changing the original validator view can change the digest label. -/
+theorem label_can_differ_when_original_view_differs :
+    (labelDigest true 6 10 8 0).label ≠
+      (labelDigest true 6 10 10 0).label := by
+  native_decide
+
+end XahauConsensus

formal_verification/XahauConsensus/SidecarAlignment.lean

@@ -0,0 +1,241 @@
+namespace XahauConsensus
+
+/-- Count a local boolean contribution as the `Nat` value used in threshold
+comparisons. -/
+def localPublishedCount (localPublished : Bool) : Nat :=
+  if localPublished then 1 else 0
+
+/-- The proof-level participant count behind sidecar alignment.
+
+`aligned` is the count of aligned remote active-view participants; a local
+publication contributes one more participant. -/
+def alignedParticipants
+    (aligned : Nat)
+    (localIsMember localPublished : Bool) : Nat :=
+  aligned + localPublishedCount (localIsMember && localPublished)
+
+/-- Sidecar quorum predicate, kept boolean to mirror the implementation check. -/
+def quorumAligned
+    (threshold aligned : Nat)
+    (localIsMember localPublished : Bool) : Bool :=
+  decide (threshold <= alignedParticipants aligned localIsMember localPublished)
+
+/-- Full sidecar observation means every converged transaction has been seen. -/
+def fullObservation (peersSeen txConverged : Nat) : Bool :=
+  peersSeen == txConverged
+
+/-- Count aligned peers from a finite peer prefix, filtering through the active
+view before any alignment bit contributes. -/
+def activeAlignedCount
+    (inActiveView peerAligned : Nat → Bool) : Nat → Nat
+  | 0 => 0
+  | peer + 1 =>
+      activeAlignedCount inActiveView peerAligned peer +
+        localPublishedCount (inActiveView peer && peerAligned peer)
+
+theorem localPublishedCount_true :
+    localPublishedCount true = 1 := by
+  rfl
+
+theorem localPublishedCount_false :
+    localPublishedCount false = 0 := by
+  rfl
+
+theorem localPublishedCount_le_one (published : Bool) :
+    localPublishedCount published <= 1 := by
+  cases published <;> simp [localPublishedCount]
+
+/-- Core participant-count equation: aligned remotes plus the local published
+contribution. -/
+theorem alignedParticipants_eq_aligned_plus_localPublished
+    (aligned : Nat) (localIsMember localPublished : Bool) :
+    alignedParticipants aligned localIsMember localPublished =
+      aligned + localPublishedCount (localIsMember && localPublished) := by
+  rfl
+
+/-- A non-active local node cannot pad the participant count. -/
+theorem alignedParticipants_local_nonmember
+    (aligned : Nat) (localPublished : Bool) :
+    alignedParticipants aligned false localPublished = aligned := by
+  cases localPublished <;> rfl
+
+/-- An active local node contributes exactly when it published the sidecar hash. -/
+theorem alignedParticipants_local_member
+    (aligned : Nat) (localPublished : Bool) :
+    alignedParticipants aligned true localPublished =
+      aligned + localPublishedCount localPublished := by
+  cases localPublished <;> rfl
+
+/-- The local node can add at most one participant to the remote aligned count. -/
+theorem alignedParticipants_le_aligned_succ
+    (aligned : Nat) (localIsMember localPublished : Bool) :
+    alignedParticipants aligned localIsMember localPublished <= aligned + 1 := by
+  cases localIsMember <;> cases localPublished <;>
+    simp [alignedParticipants, localPublishedCount]
+
+/-- The boolean quorum predicate is exactly the threshold comparison over
+`alignedParticipants`. -/
+theorem quorumAligned_iff_threshold_le_alignedParticipants
+    (threshold aligned : Nat) (localIsMember localPublished : Bool) :
+    quorumAligned threshold aligned localIsMember localPublished = true ↔
+      threshold <= alignedParticipants aligned localIsMember localPublished := by
+  unfold quorumAligned
+  simp
+
+/-- The boolean full-observation predicate is exactly equality of the observed
+and converged counts. -/
+theorem fullObservation_iff_peersSeen_eq_txConverged
+    (peersSeen txConverged : Nat) :
+    fullObservation peersSeen txConverged = true ↔
+      peersSeen = txConverged := by
+  unfold fullObservation
+  simp
+
+/-- A peer outside the active view contributes zero, even if its sidecar
+alignment bit is set. -/
+theorem activeAlignedCount_succ_nonmember
+    {inActiveView peerAligned : Nat → Bool} {peer : Nat}
+    (hNonmember : inActiveView peer = false) :
+    activeAlignedCount inActiveView peerAligned (peer + 1) =
+      activeAlignedCount inActiveView peerAligned peer := by
+  simp [activeAlignedCount, hNonmember, localPublishedCount]
+
+/-- A prefix of `n` peer positions can contribute at most `n` aligned active
+remote participants. -/
+theorem activeAlignedCount_le_prefix
+    (inActiveView peerAligned : Nat → Bool) (n : Nat) :
+    activeAlignedCount inActiveView peerAligned n <= n := by
+  induction n with
+  | zero =>
+      simp [activeAlignedCount]
+  | succ n ih =>
+      cases hAligned : inActiveView n && peerAligned n
+      · simp [activeAlignedCount, hAligned, localPublishedCount]
+        exact Nat.le_trans ih (Nat.le_succ n)
+      · simp [activeAlignedCount, hAligned, localPublishedCount]
+        exact ih
+
+/-- With the optional local contribution included, the participant count is
+bounded by the inspected remote prefix plus one. -/
+theorem alignedParticipants_le_prefix_succ
+    (inActiveView peerAligned : Nat → Bool)
+    (n : Nat)
+    (localIsMember localPublished : Bool) :
+    alignedParticipants
+        (activeAlignedCount inActiveView peerAligned n)
+        localIsMember
+        localPublished <= n + 1 := by
+  have hRemote := activeAlignedCount_le_prefix inActiveView peerAligned n
+  cases localIsMember <;> cases localPublished <;>
+    simp [alignedParticipants, localPublishedCount]
+  · exact Nat.le_trans hRemote (Nat.le_succ n)
+  · exact Nat.le_trans hRemote (Nat.le_succ n)
+  · exact Nat.le_trans hRemote (Nat.le_succ n)
+  · exact hRemote
+
+/-- Adding a nonmember peer to the inspected prefix cannot increase
+`alignedParticipants`. -/
+theorem alignedParticipants_succ_nonmember
+    {inActiveView peerAligned : Nat → Bool} {peer : Nat}
+    (localIsMember localPublished : Bool)
+    (hNonmember : inActiveView peer = false) :
+    alignedParticipants
+        (activeAlignedCount inActiveView peerAligned (peer + 1))
+        localIsMember
+        localPublished =
+      alignedParticipants
+        (activeAlignedCount inActiveView peerAligned peer)
+        localIsMember
+        localPublished := by
+  simp [alignedParticipants, activeAlignedCount_succ_nonmember hNonmember]
+
+/-- Consequently, a nonmember peer cannot change the quorum-aligned result. -/
+theorem quorumAligned_succ_nonmember
+    {inActiveView peerAligned : Nat → Bool} {peer threshold : Nat}
+    (localIsMember localPublished : Bool)
+    (hNonmember : inActiveView peer = false) :
+    quorumAligned threshold
+        (activeAlignedCount inActiveView peerAligned (peer + 1))
+        localIsMember
+        localPublished =
+      quorumAligned threshold
+        (activeAlignedCount inActiveView peerAligned peer)
+        localIsMember
+        localPublished := by
+  simp [
+    quorumAligned,
+    alignedParticipants_succ_nonmember
+      localIsMember
+      localPublished
+      hNonmember]
+
+/-- Active-view filtering: only member peers' alignment bits can affect the
+aligned remote count. -/
+theorem activeAlignedCount_ext_on_members
+    {n : Nat} {inActiveView alignedA alignedB : Nat → Bool}
+    (hSameOnMembers :
+      ∀ peer, peer < n → inActiveView peer = true →
+        alignedA peer = alignedB peer) :
+    activeAlignedCount inActiveView alignedA n =
+      activeAlignedCount inActiveView alignedB n := by
+  induction n with
+  | zero =>
+      rfl
+  | succ n ih =>
+      have hPrefix :
+          ∀ peer, peer < n → inActiveView peer = true →
+            alignedA peer = alignedB peer := by
+        intro peer hLt hMember
+        exact hSameOnMembers peer (Nat.lt_trans hLt (Nat.lt_succ_self n)) hMember
+      have hAt :
+          localPublishedCount (inActiveView n && alignedA n) =
+            localPublishedCount (inActiveView n && alignedB n) := by
+        cases hMember : inActiveView n
+        · simp [localPublishedCount]
+        · have hEq := hSameOnMembers n (Nat.lt_succ_self n) hMember
+          simp [hEq, localPublishedCount]
+      simp [activeAlignedCount, ih hPrefix, hAt]
+
+/-- Changing sidecar alignment reports for nonmembers cannot change the final
+participant count. -/
+theorem alignedParticipants_ext_on_members
+    {n : Nat} {inActiveView alignedA alignedB : Nat → Bool}
+    {localIsMember : Bool}
+    {localPublished : Bool}
+    (hSameOnMembers :
+      ∀ peer, peer < n → inActiveView peer = true →
+        alignedA peer = alignedB peer) :
+    alignedParticipants
+        (activeAlignedCount inActiveView alignedA n)
+        localIsMember
+        localPublished =
+      alignedParticipants
+        (activeAlignedCount inActiveView alignedB n)
+        localIsMember
+        localPublished := by
+  simp [
+    alignedParticipants,
+    activeAlignedCount_ext_on_members hSameOnMembers]
+
+/-- Changing sidecar alignment reports for nonmembers cannot turn quorum on or
+off. -/
+theorem quorumAligned_ext_on_members
+    {n threshold : Nat} {inActiveView alignedA alignedB : Nat → Bool}
+    {localIsMember : Bool}
+    {localPublished : Bool}
+    (hSameOnMembers :
+      ∀ peer, peer < n → inActiveView peer = true →
+        alignedA peer = alignedB peer) :
+    quorumAligned threshold
+        (activeAlignedCount inActiveView alignedA n)
+        localIsMember
+        localPublished =
+      quorumAligned threshold
+        (activeAlignedCount inActiveView alignedB n)
+        localIsMember
+        localPublished := by
+  simp [
+    quorumAligned,
+    alignedParticipants_ext_on_members hSameOnMembers]
+
+end XahauConsensus

formal_verification/XahauConsensus/SixtyPercent.lean

@@ -0,0 +1,56 @@
+import XahauConsensus.Threshold
+
+namespace XahauConsensus
+
+/-!
+Review-oriented facts about the tempting `ceil(60%)` participant threshold.
+
+The live `participantThreshold` is one higher than naive 60% at exact
+multiples of five. That extra vote is what turns equality at the
+Byzantine-overlap boundary into strict intersection safety.
+-/
+
+/-- A naive `ceil(0.6 * count)` threshold. -/
+def naiveSixtyPercentThreshold (count : Nat) : Nat :=
+  (count * 60 + 99) / 100
+
+theorem naiveSixtyPercentThreshold_five_mul (k : Nat) :
+    naiveSixtyPercentThreshold (5 * k) = 3 * k := by
+  unfold naiveSixtyPercentThreshold
+  omega
+
+theorem participantThreshold_five_mul_eq_naiveSixtyPercentThreshold_succ
+    (k : Nat) :
+    participantThreshold (5 * k) =
+      naiveSixtyPercentThreshold (5 * k) + 1 := by
+  unfold participantThreshold byzantineBound naiveSixtyPercentThreshold
+  omega
+
+/-- At exact multiples of five, naive 60% only reaches the unsafe boundary. -/
+theorem naiveSixtyPercentThreshold_five_mul_hits_intersection_boundary
+    (k : Nat) :
+    2 * naiveSixtyPercentThreshold (5 * k) =
+      5 * k + byzantineBound (5 * k) := by
+  unfold naiveSixtyPercentThreshold byzantineBound
+  omega
+
+theorem naiveSixtyPercentThreshold_five_mul_not_intersection_safe
+    (k : Nat) :
+    ¬ 5 * k + byzantineBound (5 * k) <
+      2 * naiveSixtyPercentThreshold (5 * k) := by
+  rw [naiveSixtyPercentThreshold_five_mul_hits_intersection_boundary k]
+  omega
+
+theorem participantThreshold_five_mul_intersection_safe (k : Nat) :
+    5 * k + byzantineBound (5 * k) <
+      2 * participantThreshold (5 * k) := by
+  exact participantThreshold_intersection_safe (5 * k)
+
+/-- At exact multiples of five, the live threshold clears the boundary by two. -/
+theorem participantThreshold_five_mul_intersection_margin (k : Nat) :
+    2 * participantThreshold (5 * k) =
+      (5 * k + byzantineBound (5 * k)) + 2 := by
+  unfold participantThreshold byzantineBound
+  omega
+
+end XahauConsensus

formal_verification/XahauConsensus/Threshold.lean

@@ -0,0 +1,124 @@
+namespace XahauConsensus
+
+/-- C++: `count / 5`, the conservative Byzantine bound used by
+`calculateParticipantThreshold`. -/
+def byzantineBound (count : Nat) : Nat :=
+  count / 5
+
+/-- C++: `calculateParticipantThreshold(count)`.
+
+This is the smallest integer `t` satisfying `2 * t > count + floor(count / 5)`.
+-/
+def participantThreshold (count : Nat) : Nat :=
+  (count + byzantineBound count) / 2 + 1
+
+/-- C++: `calculateQuorumThreshold(count)`, i.e. `ceil(0.8 * count)`. -/
+def quorumThreshold (count : Nat) : Nat :=
+  (count * 80 + 99) / 100
+
+/-- C++: `ConsensusExtensions::quorumThreshold()`.
+
+The raw formula gives `0` for an empty view, but the live consensus-extension
+gate requires at least one aligned participant for safety.
+-/
+def safeQuorumThreshold (count : Nat) : Nat :=
+  if count = 0 then 1 else quorumThreshold count
+
+/-- C++: `ConsensusExtensions::tier2Threshold()`.
+
+`participantThreshold 0` already returns `1`; this wrapper makes the
+zero-view safety rule explicit and mirrors the C++ method shape.
+-/
+def safeParticipantThreshold (count : Nat) : Nat :=
+  if count = 0 then 1 else participantThreshold count
+
+/-- The Tier-2 threshold strictly exceeds the Byzantine-overlap boundary.
+
+This is the load-bearing equivocation invariant behind participant-aligned
+entropy: two cohorts of this size in a `count`-sized universe overlap in more
+than `floor(count / 5)` validators.
+-/
+theorem participantThreshold_intersection_safe (count : Nat) :
+    count + byzantineBound count < 2 * participantThreshold count := by
+  unfold participantThreshold byzantineBound
+  omega
+
+/-- Anchoring the Tier-2 threshold to the original pre-nUNL view remains safe
+when the effective post-nUNL view shrinks.
+
+This is the arithmetic reason `originalViewSize` is the right denominator:
+smaller effective universes only increase the intersection margin.
+-/
+theorem participantThreshold_safe_under_effective_shrink
+    (originalView effectiveView : Nat)
+    (hShrink : effectiveView <= originalView) :
+    effectiveView + byzantineBound originalView <
+      2 * participantThreshold originalView := by
+  have hSafe := participantThreshold_intersection_safe originalView
+  omega
+
+/-- Concrete regression example: if `originalView = 10` and `effectiveView = 8`,
+using the effective view's participant threshold (`5`) leaves the overlap equal
+to the original-view Byzantine bound (`2`), not strictly greater than it.
+
+This is why the C++ must not replace `originalViewSize` with `size()` for the
+Tier-2 floor.
+-/
+theorem effective_threshold_regression_hits_boundary_example :
+    2 * participantThreshold 8 <= 8 + byzantineBound 10 := by
+  native_decide
+
+theorem threshold_minimal_for_boundary (boundary threshold : Nat) :
+    boundary < 2 * threshold → boundary / 2 + 1 <= threshold := by
+  omega
+
+theorem below_threshold_not_safe_for_boundary (boundary threshold : Nat) :
+    threshold < boundary / 2 + 1 → 2 * threshold <= boundary := by
+  omega
+
+/-- `participantThreshold` is the smallest threshold satisfying the strict
+intersection-safety inequality. -/
+theorem participantThreshold_minimal (count threshold : Nat) :
+    count + byzantineBound count < 2 * threshold →
+      participantThreshold count <= threshold := by
+  intro hSafe
+  unfold participantThreshold
+  exact threshold_minimal_for_boundary
+    (count + byzantineBound count)
+    threshold
+    hSafe
+
+/-- Anything below `participantThreshold` fails the strict intersection-safety
+inequality. -/
+theorem below_participantThreshold_not_safe (count threshold : Nat) :
+    threshold < participantThreshold count →
+      2 * threshold <= count + byzantineBound count := by
+  intro hBelow
+  unfold participantThreshold at hBelow
+  exact below_threshold_not_safe_for_boundary
+    (count + byzantineBound count)
+    threshold
+    hBelow
+
+/-- The participant threshold never exceeds the 80% validator-quorum threshold.
+
+This is useful because Tier 2 should form a band below Tier 3, not a stricter
+condition than validator quorum.
+-/
+theorem participantThreshold_le_quorumThreshold (count : Nat) :
+    0 < count → participantThreshold count <= quorumThreshold count := by
+  intro hCount
+  unfold participantThreshold quorumThreshold byzantineBound
+  omega
+
+/-- With the live safety wrappers, the participant threshold never exceeds the
+validator-quorum threshold, including the empty-view edge case. -/
+theorem safeParticipantThreshold_le_safeQuorumThreshold (count : Nat) :
+    safeParticipantThreshold count <= safeQuorumThreshold count := by
+  unfold safeParticipantThreshold safeQuorumThreshold
+  by_cases hZero : count = 0
+  · simp [hZero]
+  · have hPositive : 0 < count := Nat.pos_of_ne_zero hZero
+    simp [hZero, participantThreshold_le_quorumThreshold count hPositive]
+
+end XahauConsensus

formal_verification/XahauConsensus/ThresholdFacts.lean

@@ -0,0 +1,223 @@
+import XahauConsensus.Threshold
+
+namespace XahauConsensus
+
+/-!
+Additional arithmetic facts about the Xahau consensus thresholds.
+
+These lemmas are deliberately small and review-oriented: they expose concrete
+edge cases, exact multiples-of-five behavior, participant/quorum band facts,
+and monotonicity of the threshold functions.
+-/
+
+theorem byzantineBound_zero : byzantineBound 0 = 0 := by
+  native_decide
+
+theorem participantThreshold_zero : participantThreshold 0 = 1 := by
+  native_decide
+
+theorem quorumThreshold_zero : quorumThreshold 0 = 0 := by
+  native_decide
+
+theorem safeQuorumThreshold_zero : safeQuorumThreshold 0 = 1 := by
+  native_decide
+
+theorem safeParticipantThreshold_zero : safeParticipantThreshold 0 = 1 := by
+  native_decide
+
+theorem byzantineBound_one : byzantineBound 1 = 0 := by
+  native_decide
+
+theorem participantThreshold_one : participantThreshold 1 = 1 := by
+  native_decide
+
+theorem quorumThreshold_one : quorumThreshold 1 = 1 := by
+  native_decide
+
+theorem safeQuorumThreshold_one : safeQuorumThreshold 1 = 1 := by
+  native_decide
+
+theorem safeParticipantThreshold_one : safeParticipantThreshold 1 = 1 := by
+  native_decide
+
+theorem participantThreshold_two : participantThreshold 2 = 2 := by
+  native_decide
+
+theorem quorumThreshold_two : quorumThreshold 2 = 2 := by
+  native_decide
+
+theorem participantThreshold_three : participantThreshold 3 = 2 := by
+  native_decide
+
+theorem quorumThreshold_three : quorumThreshold 3 = 3 := by
+  native_decide
+
+theorem participantThreshold_four : participantThreshold 4 = 3 := by
+  native_decide
+
+theorem quorumThreshold_four : quorumThreshold 4 = 4 := by
+  native_decide
+
+theorem byzantineBound_five : byzantineBound 5 = 1 := by
+  native_decide
+
+theorem participantThreshold_five : participantThreshold 5 = 4 := by
+  native_decide
+
+theorem quorumThreshold_five : quorumThreshold 5 = 4 := by
+  native_decide
+
+theorem byzantineBound_ten : byzantineBound 10 = 2 := by
+  native_decide
+
+theorem participantThreshold_ten : participantThreshold 10 = 7 := by
+  native_decide
+
+theorem quorumThreshold_ten : quorumThreshold 10 = 8 := by
+  native_decide
+
+theorem byzantineBound_twenty : byzantineBound 20 = 4 := by
+  native_decide
+
+theorem participantThreshold_twenty : participantThreshold 20 = 13 := by
+  native_decide
+
+theorem quorumThreshold_twenty : quorumThreshold 20 = 16 := by
+  native_decide
+
+theorem byzantineBound_five_mul (k : Nat) :
+    byzantineBound (5 * k) = k := by
+  unfold byzantineBound
+  omega
+
+theorem participantThreshold_five_mul (k : Nat) :
+    participantThreshold (5 * k) = 3 * k + 1 := by
+  unfold participantThreshold byzantineBound
+  omega
+
+theorem quorumThreshold_five_mul (k : Nat) :
+    quorumThreshold (5 * k) = 4 * k := by
+  unfold quorumThreshold
+  omega
+
+/-- On exact multiples of five, the strict safety margin is exactly two. -/
+theorem participantThreshold_five_mul_margin (k : Nat) :
+    2 * participantThreshold (5 * k) =
+      (5 * k + byzantineBound (5 * k)) + 2 := by
+  rw [participantThreshold_five_mul, byzantineBound_five_mul]
+  omega
+
+/-- One below the multiple-of-five participant threshold reaches only equality
+with the unsafe boundary, so the strict safety inequality fails. -/
+theorem below_participantThreshold_five_mul_hits_boundary (k : Nat) :
+    2 * (participantThreshold (5 * k) - 1) =
+      5 * k + byzantineBound (5 * k) := by
+  rw [participantThreshold_five_mul, byzantineBound_five_mul]
+  omega
+
+theorem participantThreshold_five_mul_lt_quorumThreshold_five_mul
+    {k : Nat} (h : 1 < k) :
+    participantThreshold (5 * k) < quorumThreshold (5 * k) := by
+  rw [participantThreshold_five_mul, quorumThreshold_five_mul]
+  omega
+
+theorem participantThreshold_five_eq_quorumThreshold_five :
+    participantThreshold 5 = quorumThreshold 5 := by
+  native_decide
+
+theorem participantThreshold_ten_lt_quorumThreshold_ten :
+    participantThreshold 10 < quorumThreshold 10 := by
+  native_decide
+
+theorem participant_band_nonempty {count : Nat}
+    (h : participantThreshold count < quorumThreshold count) :
+    ∃ participants,
+      participantThreshold count <= participants ∧
+        participants < quorumThreshold count := by
+  exact ⟨participantThreshold count, Nat.le_refl _, h⟩
+
+theorem participant_band_empty {count : Nat}
+    (h : quorumThreshold count <= participantThreshold count) :
+    ¬ ∃ participants,
+      participantThreshold count <= participants ∧
+        participants < quorumThreshold count := by
+  intro hExists
+  rcases hExists with ⟨participants, hParticipant, hBelowQuorum⟩
+  omega
+
+theorem participant_band_empty_zero :
+    ¬ ∃ participants,
+      participantThreshold 0 <= participants ∧
+        participants < quorumThreshold 0 := by
+  apply participant_band_empty
+  native_decide
+
+theorem participant_band_empty_one :
+    ¬ ∃ participants,
+      participantThreshold 1 <= participants ∧
+        participants < quorumThreshold 1 := by
+  apply participant_band_empty
+  native_decide
+
+theorem participant_band_empty_two :
+    ¬ ∃ participants,
+      participantThreshold 2 <= participants ∧
+        participants < quorumThreshold 2 := by
+  apply participant_band_empty
+  native_decide
+
+theorem participant_band_empty_five :
+    ¬ ∃ participants,
+      participantThreshold 5 <= participants ∧
+        participants < quorumThreshold 5 := by
+  apply participant_band_empty
+  native_decide
+
+theorem participant_band_nonempty_three :
+    ∃ participants,
+      participantThreshold 3 <= participants ∧
+        participants < quorumThreshold 3 := by
+  apply participant_band_nonempty
+  native_decide
+
+theorem participant_band_nonempty_four :
+    ∃ participants,
+      participantThreshold 4 <= participants ∧
+        participants < quorumThreshold 4 := by
+  apply participant_band_nonempty
+  native_decide
+
+theorem participant_band_nonempty_ten :
+    ∃ participants,
+      participantThreshold 10 <= participants ∧
+        participants < quorumThreshold 10 := by
+  apply participant_band_nonempty
+  native_decide
+
+theorem participant_band_nonempty_five_mul {k : Nat} (h : 1 < k) :
+    ∃ participants,
+      participantThreshold (5 * k) <= participants ∧
+        participants < quorumThreshold (5 * k) := by
+  exact participant_band_nonempty
+    (participantThreshold_five_mul_lt_quorumThreshold_five_mul h)
+
+theorem byzantineBound_mono {a b : Nat} (h : a <= b) :
+    byzantineBound a <= byzantineBound b := by
+  unfold byzantineBound
+  exact Nat.div_le_div_right h
+
+theorem participantThreshold_mono {a b : Nat} (h : a <= b) :
+    participantThreshold a <= participantThreshold b := by
+  unfold participantThreshold
+  apply Nat.succ_le_succ
+  apply Nat.div_le_div_right
+  have hByzantine := byzantineBound_mono h
+  omega
+
+theorem quorumThreshold_mono {a b : Nat} (h : a <= b) :
+    quorumThreshold a <= quorumThreshold b := by
+  unfold quorumThreshold
+  apply Nat.div_le_div_right
+  omega
+
+end XahauConsensus

formal_verification/XahauConsensus/ViewUniverse.lean

@@ -0,0 +1,201 @@
+import XahauConsensus.ThresholdFacts
+
+namespace XahauConsensus
+
+/-!
+Concrete arithmetic examples for the distinction between the active effective
+view, the original pre-nUNL view, and any larger trusted counting universe.
+
+The safety shape is deliberately Nat-only: two cohorts of size `threshold` in
+an `activeView` overlap strictly beyond the Byzantine bound charged to
+`byzantineUniverse` when
+
+  `activeView + byzantineBound byzantineUniverse < 2 * threshold`.
+-/
+
+def strictIntersectionSafe
+    (activeView byzantineUniverse threshold : Nat) : Prop :=
+  activeView + byzantineBound byzantineUniverse < 2 * threshold
+
+/-- Strict intersection safety plus reachability of the threshold inside the
+active view. This separates "safe if it happens" from "possible to happen". -/
+def nonvacuousStrictIntersectionSafe
+    (activeView byzantineUniverse threshold : Nat) : Prop :=
+  threshold <= activeView ∧ strictIntersectionSafe activeView byzantineUniverse threshold
+
+/-- Cross-view Tier-2 band: participant floor is anchored to the original view,
+validator quorum to the effective view. -/
+def participantBandNonempty
+    (effectiveView originalView : Nat) : Prop :=
+  ∃ participants,
+    participantThreshold originalView <= participants ∧
+      participants < quorumThreshold effectiveView
+
+theorem participantBandNonempty_iff
+    (effectiveView originalView : Nat) :
+    participantBandNonempty effectiveView originalView ↔
+      participantThreshold originalView < quorumThreshold effectiveView := by
+  constructor
+  · intro h
+    rcases h with ⟨participants, hParticipant, hBelowQuorum⟩
+    omega
+  · intro h
+    exact ⟨participantThreshold originalView, Nat.le_refl _, h⟩
+
+/-- The original-view participant threshold remains safe when nUNL shrinks the
+active effective view. -/
+theorem original_threshold_safe_under_nunl_shrink
+    {originalView effectiveView : Nat}
+    (hShrink : effectiveView <= originalView) :
+    strictIntersectionSafe
+      effectiveView
+      originalView
+      (participantThreshold originalView) := by
+  unfold strictIntersectionSafe
+  exact participantThreshold_safe_under_effective_shrink
+    originalView
+    effectiveView
+    hShrink
+
+theorem original_threshold_nonvacuous_under_nunl_shrink
+    {originalView effectiveView : Nat}
+    (hShrink : effectiveView <= originalView)
+    (hReachable : participantThreshold originalView <= effectiveView) :
+    nonvacuousStrictIntersectionSafe
+      effectiveView
+      originalView
+      (participantThreshold originalView) := by
+  constructor
+  · exact hReachable
+  · exact original_threshold_safe_under_nunl_shrink hShrink
+
+/-- The original-view threshold is also safe if the Byzantine counting universe
+is no larger than the original view. -/
+theorem original_threshold_safe_for_no_larger_counting_universe
+    {originalView effectiveView countingUniverse : Nat}
+    (hShrink : effectiveView <= originalView)
+    (hCounting : countingUniverse <= originalView) :
+    strictIntersectionSafe
+      effectiveView
+      countingUniverse
+      (participantThreshold originalView) := by
+  unfold strictIntersectionSafe
+  have hOriginal :=
+    participantThreshold_safe_under_effective_shrink
+      originalView
+      effectiveView
+      hShrink
+  have hBound := byzantineBound_mono hCounting
+  omega
+
+/-- Any threshold at or below the overlap boundary is not strictly safe. -/
+theorem not_strictIntersectionSafe_of_threshold_le_boundary
+    {activeView byzantineUniverse threshold : Nat}
+    (hBoundary : 2 * threshold <= activeView + byzantineBound byzantineUniverse) :
+    ¬ strictIntersectionSafe activeView byzantineUniverse threshold := by
+  unfold strictIntersectionSafe
+  omega
+
+/-- If the effective-view threshold is below what the original Byzantine bound
+requires, it cannot prove strict intersection safety against that original
+bound. -/
+theorem effective_threshold_not_safe_against_original_bound
+    {originalView effectiveView : Nat}
+    (hBelow :
+      participantThreshold effectiveView <
+        (effectiveView + byzantineBound originalView) / 2 + 1) :
+    ¬ strictIntersectionSafe
+      effectiveView
+      originalView
+      (participantThreshold effectiveView) := by
+  apply not_strictIntersectionSafe_of_threshold_le_boundary
+  exact below_threshold_not_safe_for_boundary
+    (effectiveView + byzantineBound originalView)
+    (participantThreshold effectiveView)
+    hBelow
+
+/-- A larger trusted counting universe increases the Byzantine side of the
+boundary, eroding the strict-intersection margin. -/
+theorem original_boundary_le_trusted_superset_boundary
+    {originalView effectiveView trustedUniverse : Nat}
+    (hSuperset : originalView <= trustedUniverse) :
+    effectiveView + byzantineBound originalView <=
+      effectiveView + byzantineBound trustedUniverse := by
+  have hBound := byzantineBound_mono hSuperset
+  omega
+
+/-- Concrete nUNL example: `originalView = 10`, `effectiveView = 8`, and the
+original threshold still clears the original Byzantine bound. -/
+theorem original_ten_effective_eight_original_threshold_safe :
+    strictIntersectionSafe 8 10 (participantThreshold 10) := by
+  unfold strictIntersectionSafe
+  native_decide
+
+theorem original_ten_effective_eight_participant_band_empty :
+    ¬ participantBandNonempty 8 10 := by
+  rw [participantBandNonempty_iff]
+  native_decide
+
+theorem original_ten_effective_eight_original_threshold_reachable :
+    nonvacuousStrictIntersectionSafe 8 10 (participantThreshold 10) := by
+  apply original_threshold_nonvacuous_under_nunl_shrink
+  · native_decide
+  · native_decide
+
+/-- Concrete regression: for `originalView = 10` and `effectiveView = 8`, the
+effective threshold does not strictly clear the original Byzantine bound. -/
+theorem original_ten_effective_eight_effective_threshold_not_safe :
+    ¬ strictIntersectionSafe 8 10 (participantThreshold 8) := by
+  apply not_strictIntersectionSafe_of_threshold_le_boundary
+  native_decide
+
+/-- The same failure as a direct boundary comparison, useful when reviewing the
+raw arithmetic. -/
+theorem original_ten_effective_eight_effective_threshold_hits_boundary :
+    2 * participantThreshold 8 <= 8 + byzantineBound 10 := by
+  native_decide
+
+/-- Larger concrete nUNL example with the original threshold anchored at
+`20`. -/
+theorem original_twenty_effective_sixteen_original_threshold_safe :
+    strictIntersectionSafe 16 20 (participantThreshold 20) := by
+  unfold strictIntersectionSafe
+  native_decide
+
+theorem original_twenty_effective_sixteen_participant_band_empty :
+    ¬ participantBandNonempty 16 20 := by
+  rw [participantBandNonempty_iff]
+  native_decide
+
+theorem original_twenty_effective_fifteen_participant_band_empty :
+    ¬ participantBandNonempty 15 20 := by
+  rw [participantBandNonempty_iff]
+  native_decide
+
+theorem original_twenty_effective_fifteen_original_threshold_reachable :
+    nonvacuousStrictIntersectionSafe 15 20 (participantThreshold 20) := by
+  apply original_threshold_nonvacuous_under_nunl_shrink
+  · native_decide
+  · native_decide
+
+/-- With `originalView = 20` and `effectiveView = 16`, using the effective
+threshold again reaches the unsafe boundary. -/
+theorem original_twenty_effective_sixteen_effective_threshold_not_safe :
+    ¬ strictIntersectionSafe 16 20 (participantThreshold 16) := by
+  apply not_strictIntersectionSafe_of_threshold_le_boundary
+  native_decide
+
+/-- Counting Byzantine stake over a trusted universe of `20` instead of the
+original view of `10` erodes the margin all the way to equality. -/
+theorem trusted_superset_twenty_erodes_original_ten_margin_to_boundary :
+    2 * participantThreshold 10 = 10 + byzantineBound 20 := by
+  native_decide
+
+/-- The equality above means the original threshold for `10` is not strictly
+safe if Byzantine weight is counted over the larger trusted universe `20`. -/
+theorem trusted_superset_twenty_original_ten_threshold_not_safe :
+    ¬ strictIntersectionSafe 10 20 (participantThreshold 10) := by
+  apply not_strictIntersectionSafe_of_threshold_le_boundary
+  native_decide
+
+end XahauConsensus

formal_verification/lake-manifest.json

@@ -0,0 +1,96 @@
+{"version": "1.2.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.31.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "e3cb2f741431ce31bf73549fb52316a57368b06f",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "fa08db58b30eb033edcdab331bba000827f9f785",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.31.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "xahau_consensus",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}

formal_verification/lakefile.toml

@@ -0,0 +1,11 @@
+name = "xahau_consensus"
+version = "0.1.0"
+defaultTargets = ["XahauConsensus"]
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4.git"
+rev = "v4.31.0"
+
+[[lean_lib]]
+name = "XahauConsensus"

formal_verification/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.31.0

src/test/app/Export_test.cpp

@@ -844,6 +844,76 @@ struct Export_test : public beast::unit_test::suite
                 st->getFieldH256(sfTransactionHash) == expectedSignedTxHash);
     }
 
+    void
+    testExportNetworkApplyDoesNotUseLiveCollectorFallback(
+        FeatureBitset features)
+    {
+        testcase("ttEXPORT network apply does not use live collector fallback");
+
+        using namespace jtx;
+
+        Env env{*this, exportTestConfig(), features};
+
+        Account const alice{"alice"};
+        Account const carol{"carol"};
+
+        env.fund(XRP(10000), alice, carol);
+        env.close();
+
+        auto const& valKeys = env.app().getValidatorKeys();
+        BEAST_EXPECT(valKeys.keys);
+        if (!valKeys.keys)
+            return;
+
+        auto const& valPK = valKeys.keys->publicKey;
+        auto const& valSK = valKeys.keys->secretKey;
+        seedUNLReportLedger(env, {valPK});
+        forceNonStandalone(env.app());
+        BEAST_EXPECT(!env.app().config().standalone());
+
+        auto const seq = env.current()->seq();
+        auto const ticketSeq = std::uint32_t{1};
+        auto const lls = seq + 5;
+        auto innerObj = buildExportedPayment(
+            alice.id(), carol.id(), seq + 1, lls, ticketSeq);
+        auto const innerTx = makeSTTx(innerObj);
+        auto jt = makeExportJTx(env, alice, innerObj, lls);
+        auto const exportTx = jt.stx;
+        BEAST_EXPECT(exportTx);
+        if (!exportTx)
+            return;
+        auto const txHash = exportTx->getTransactionID();
+
+        auto& ce = env.app().getConsensusExtensions();
+        ce.setExportEnabledThisRound(true);
+        ce.cacheUNLReport(env.app().getLedgerMaster().getClosedLedger());
+        auto const view = ce.activeValidatorView();
+        BEAST_EXPECT(view->fromUNLReport);
+        ce.cacheConsensusTxSet(makeRCLTxSet(env.app(), {exportTx}));
+
+        auto const applySeq = env.closed()->seq() + 1;
+        auto const agreedHash = ce.buildExportSigSet(applySeq);
+        BEAST_EXPECT(ce.isSidecarSet(agreedHash));
+
+        // The agreed sidecar snapshot is empty. A later local collector quorum
+        // must not rescue this apply path; network-mode export applies only
+        // from the frozen exportSigSetHash map.
+        auto const lateSig =
+            ExportResultBuilder::signExportedTxn(innerTx, valPK, valSK);
+        ce.exportSigCollector().addVerifiedSignature(
+            txHash, valPK, lateSig, applySeq);
+
+        auto const parent = env.app().getLedgerMaster().getClosedLedger();
+        auto next = std::make_shared<Ledger>(
+            *parent, env.app().timeKeeper().closeTime());
+        OpenView accum(&*next);
+        auto const result =
+            ripple::apply(env.app(), accum, *exportTx, tapNONE, env.journal);
+        BEAST_EXPECT(result.ter == terRETRY_EXPORT);
+        BEAST_EXPECT(!result.applied);
+        BEAST_EXPECT(!next->read(keylet::shadowTicket(alice.id(), ticketSeq)));
+    }
+
     void
     testExportNetworkRetryWithoutUNLReport(FeatureBitset features)
     {
@@ -1449,6 +1519,7 @@ struct Export_test : public beast::unit_test::suite
         testExportTxnOpenLedger(allWithExport);
         testExportNetworkRetryWithoutQuorum(allWithExport);
         testExportNetworkApplyUsesAgreedSidecar(allWithExport);
+        testExportNetworkApplyDoesNotUseLiveCollectorFallback(allWithExport);
         testExportNetworkRetryWithoutUNLReport(allWithExport);
         testExportNetworkLastLedgerSequenceBoundary(allWithExport);
         testOpenLedgerExportLimit(allWithExport);

src/test/consensus/ConsensusExtensions_test.cpp

@@ -1334,6 +1334,118 @@ class ConsensusExtensions_test : public beast::unit_test::suite
             tx->getFieldU8(sfEntropyTier) == entropyTierValidatorQuorum);
     }
 
+    void
+    testOnPreBuildFallsBackWithoutUNLReportEvenWithEntropySet()
+    {
+        testcase("onPreBuild ignores validator entropy without UNLReport view");
+
+        using namespace jtx;
+        Env env{
+            *this,
+            envconfig(validator, ""),
+            supported_amendments() | featureConsensusEntropy,
+            nullptr};
+        forceNonStandalone(env.app());
+        auto const ledger = env.app().getLedgerMaster().getClosedLedger();
+        auto const& valKeys = env.app().getValidatorKeys();
+        BEAST_EXPECT(valKeys.keys);
+        if (!valKeys.keys)
+            return;
+
+        auto const& publicKey = valKeys.keys->publicKey;
+        auto const& secretKey = valKeys.keys->secretKey;
+        auto const nodeId = valKeys.nodeID;
+        auto const prevLedger = ledger->info().hash;
+        auto const seq = ledger->seq() + 1;
+        auto const closeTime = NetClock::time_point{NetClock::duration{322}};
+        auto const txSetHash = makeHash("prebuild-no-unlreport-txset");
+        auto const reveal = makeHash("prebuild-no-unlreport-reveal");
+
+        ConsensusExtensions ce{env.app(), activeNoopJournal()};
+        ce.onRoundStart(RCLCxLedger{ledger}, {});
+        BEAST_EXPECT(!ce.activeValidatorView()->fromUNLReport);
+
+        harvestCommitReveal(
+            ce,
+            nodeId,
+            publicKey,
+            secretKey,
+            txSetHash,
+            seq,
+            closeTime,
+            prevLedger,
+            reveal);
+        auto const entropySetHash = ce.buildEntropySet(seq);
+        BEAST_EXPECT(ce.isSidecarSet(entropySetHash));
+
+        CanonicalTXSet retriableTxs{makeHash("no-unlreport-prebuild-salt")};
+        ce.onPreBuild(retriableTxs, seq, txSetHash);
+
+        auto const tx = singleCanonicalTx(retriableTxs);
+        BEAST_EXPECT(tx);
+        if (!tx)
+            return;
+        auto const expected = sha512Half(
+            HashPrefix::entropyFallback, ledger->info().hash, txSetHash, seq);
+        BEAST_EXPECT(tx->getTxnType() == ttCONSENSUS_ENTROPY);
+        BEAST_EXPECT(tx->getFieldH256(sfDigest) == expected);
+        BEAST_EXPECT(
+            tx->getFieldH256(sfDigest) != expectedEntropy(publicKey, reveal));
+        BEAST_EXPECT(tx->getFieldU16(sfEntropyCount) == 0);
+        BEAST_EXPECT(
+            tx->getFieldU8(sfEntropyTier) == entropyTierConsensusFallback);
+    }
+
+    void
+    testOnPreBuildFallsBackForEmptyEntropySet()
+    {
+        testcase("onPreBuild falls back for empty entropy-set map");
+
+        using namespace jtx;
+        Env env{
+            *this,
+            envconfig(validator, ""),
+            supported_amendments() | featureConsensusEntropy,
+            nullptr};
+        forceNonStandalone(env.app());
+        auto const ledger = env.app().getLedgerMaster().getClosedLedger();
+        auto const& valKeys = env.app().getValidatorKeys();
+        BEAST_EXPECT(valKeys.keys);
+        if (!valKeys.keys)
+            return;
+
+        auto const viewLedger = makeUNLReportLedger(
+            env, std::vector<PublicKey>{valKeys.keys->publicKey});
+        auto const seq = ledger->seq() + 1;
+        auto const txSetHash = makeHash("empty-entropy-map-txset");
+
+        ConsensusExtensions ce{env.app(), activeNoopJournal()};
+        ce.onRoundStart(RCLCxLedger{ledger}, {});
+        ce.cacheUNLReport(viewLedger);
+        BEAST_EXPECT(ce.activeValidatorView()->fromUNLReport);
+
+        // This creates a real entropySetMap_, but with zero parseable leaves.
+        // selectEntropy must treat that residual as fallback, not as a
+        // non-fallback digest over an empty sidecar root.
+        auto const entropySetHash = ce.buildEntropySet(seq);
+        BEAST_EXPECT(ce.isSidecarSet(entropySetHash));
+
+        CanonicalTXSet retriableTxs{makeHash("empty-entropy-map-salt")};
+        ce.onPreBuild(retriableTxs, seq, txSetHash);
+
+        auto const tx = singleCanonicalTx(retriableTxs);
+        BEAST_EXPECT(tx);
+        if (!tx)
+            return;
+        auto const expected = sha512Half(
+            HashPrefix::entropyFallback, ledger->info().hash, txSetHash, seq);
+        BEAST_EXPECT(tx->getTxnType() == ttCONSENSUS_ENTROPY);
+        BEAST_EXPECT(tx->getFieldH256(sfDigest) == expected);
+        BEAST_EXPECT(tx->getFieldU16(sfEntropyCount) == 0);
+        BEAST_EXPECT(
+            tx->getFieldU8(sfEntropyTier) == entropyTierConsensusFallback);
+    }
+
     void
     testOnPreBuildTier2ParticipantAligned()
     {
@@ -3355,6 +3467,8 @@ public:
         testDecoratePositionGeneratesCommitment();
         testOnPreBuildInjectsZeroEntropyFallback();
         testOnPreBuildInjectsEntropySetEntropy();
+        testOnPreBuildFallsBackWithoutUNLReportEvenWithEntropySet();
+        testOnPreBuildFallsBackForEmptyEntropySet();
         testOnPreBuildTier2ParticipantAligned();
         testTier2ThresholdAnchorsToOriginalView();
         testOnPreBuildTier2WithNegativeUNL();

src/test/formal_verification/LeanConsensus_test.cpp

@@ -0,0 +1,616 @@
+//------------------------------------------------------------------------------
+/*
+    This file is part of rippled: https://github.com/ripple/rippled
+
+    Permission to use, copy, modify, and/or distribute this software for any
+    purpose  with  or without fee is hereby granted, provided that the above
+    copyright notice and this permission notice appear in all copies.
+
+    THE  SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+    WITH  REGARD  TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+    MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+    ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+    WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+    ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+    OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+*/
+//==============================================================================
+
+#if defined(XAHAUD_ENABLE_FORMAL_VERIFICATION)
+
+#include <xrpld/app/consensus/ConsensusExtensions.h>
+#include <xrpld/app/misc/NegativeUNLVote.h>
+#include <xrpld/consensus/ConsensusExtensionsTick.h>
+#include <xrpld/consensus/ConsensusParms.h>
+#include <xrpl/beast/unit_test.h>
+
+#include <lean/lean.h>
+
+#include <cstdint>
+#include <limits>
+#include <mutex>
+#include <stdexcept>
+
+extern "C" {
+//@@start formal-ffi-c-abi-decls
+void
+lean_initialize_runtime_module();
+
+lean_object*
+initialize_xahau__consensus_XahauConsensus_FFI(
+    uint8_t builtin,
+    lean_object* world);
+
+std::uint64_t
+xahau_byzantine_bound(std::uint64_t count);
+
+std::uint64_t
+xahau_participant_threshold(std::uint64_t count);
+
+std::uint64_t
+xahau_quorum_threshold(std::uint64_t count);
+
+std::uint64_t
+xahau_safe_quorum_threshold(std::uint64_t count);
+
+std::uint64_t
+xahau_safe_participant_threshold(std::uint64_t count);
+
+std::uint64_t
+xahau_entropy_gate_threshold_for_view(
+    std::uint64_t effectiveView,
+    std::uint64_t originalView);
+
+std::uint8_t
+xahau_select_entropy_tier(
+    std::uint64_t fromUNLReport,
+    std::uint64_t participantCount,
+    std::uint64_t effectiveView,
+    std::uint64_t originalView);
+
+std::uint64_t
+xahau_aligned_participants(
+    std::uint64_t aligned,
+    std::uint64_t localIsMember,
+    std::uint64_t localPublished);
+
+std::uint8_t
+xahau_quorum_aligned(
+    std::uint64_t threshold,
+    std::uint64_t aligned,
+    std::uint64_t localIsMember,
+    std::uint64_t localPublished);
+
+std::uint8_t
+xahau_full_observation(std::uint64_t peersSeen, std::uint64_t txConverged);
+
+std::uint8_t
+xahau_export_gate_proceed(
+    std::uint64_t alignedParticipants,
+    std::uint64_t quorumThreshold,
+    std::uint64_t fullObservation);
+
+std::uint64_t
+xahau_disabled_cap(std::uint64_t originalView);
+
+std::uint64_t
+xahau_effective_view(std::uint64_t originalView, std::uint64_t disabled);
+
+std::uint8_t
+xahau_strict_intersection_safe(
+    std::uint64_t activeView,
+    std::uint64_t byzantineUniverse,
+    std::uint64_t threshold);
+
+std::uint8_t
+xahau_nonvacuous_strict_intersection_safe(
+    std::uint64_t activeView,
+    std::uint64_t byzantineUniverse,
+    std::uint64_t threshold);
+
+std::uint8_t
+xahau_participant_band_nonempty(
+    std::uint64_t effectiveView,
+    std::uint64_t originalView);
+
+std::uint64_t
+xahau_export_quorum_overlap_lower_bound(std::uint64_t activeView);
+
+std::uint8_t
+xahau_export_quorum_safe_under_nunl_cap(
+    std::uint64_t originalView,
+    std::uint64_t effectiveView,
+    std::uint64_t disabled);
+
+std::uint64_t
+xahau_active_aligned_count_mask(
+    std::uint64_t count,
+    std::uint64_t activeMask,
+    std::uint64_t alignedMask);
+
+std::uint8_t
+xahau_quorum_aligned_mask(
+    std::uint64_t threshold,
+    std::uint64_t count,
+    std::uint64_t activeMask,
+    std::uint64_t alignedMask,
+    std::uint64_t localIsMember,
+    std::uint64_t localPublished);
+
+std::uint64_t
+xahau_naive_sixty_percent_threshold(std::uint64_t count);
+
+std::uint8_t
+xahau_naive_sixty_percent_is_safe(std::uint64_t count);
+//@@end formal-ffi-c-abi-decls
+}
+
+namespace ripple {
+namespace test {
+
+namespace {
+
+bool
+strictIntersectionSafeCpp(
+    std::uint64_t activeView,
+    std::uint64_t byzantineUniverse,
+    std::uint64_t threshold)
+{
+    return activeView + byzantineUniverse / 5 < 2 * threshold;
+}
+
+bool
+participantBandNonemptyCpp(
+    std::uint64_t effectiveView,
+    std::uint64_t originalView)
+{
+    return calculateParticipantThreshold(originalView) <
+        calculateQuorumThreshold(effectiveView);
+}
+
+bool
+maskBit(std::uint64_t mask, std::uint64_t peer)
+{
+    return ((mask >> peer) & 1) != 0;
+}
+
+std::uint64_t
+activeAlignedCountMaskCpp(
+    std::uint64_t count,
+    std::uint64_t activeMask,
+    std::uint64_t alignedMask)
+{
+    std::uint64_t result = 0;
+    for (std::uint64_t peer = 0; peer < count; ++peer)
+    {
+        if (maskBit(activeMask, peer) && maskBit(alignedMask, peer))
+            ++result;
+    }
+    return result;
+}
+
+void
+initializeLean()
+{
+    static std::once_flag once;
+    std::call_once(once, [] {
+        lean_initialize_runtime_module();
+
+        auto* result = initialize_xahau__consensus_XahauConsensus_FFI(
+            1, lean_io_mk_world());
+        if (lean_io_result_is_error(result))
+        {
+            lean_dec_ref(result);
+            throw std::runtime_error{"failed to initialize XahauConsensus.FFI"};
+        }
+        lean_dec_ref(result);
+    });
+}
+
+}  // namespace
+
+class LeanConsensus_test : public beast::unit_test::suite
+{
+public:
+    void
+    testThresholdFormulaDrift()
+    {
+        testcase("Lean/C++ consensus threshold formula drift");
+
+        initializeLean();
+
+        for (std::uint64_t count = 0; count <= 1024; ++count)
+        {
+            BEAST_EXPECT(xahau_byzantine_bound(count) == count / 5);
+            BEAST_EXPECT(
+                xahau_participant_threshold(count) ==
+                calculateParticipantThreshold(count));
+            BEAST_EXPECT(
+                xahau_quorum_threshold(count) ==
+                calculateQuorumThreshold(count));
+        }
+
+        auto const max = std::numeric_limits<std::uint64_t>::max();
+        for (std::uint64_t count :
+             {max / 100 - 1,
+              max / 100,
+              max / 80 - 1,
+              max / 80,
+              max / 5 - 1,
+              max / 5,
+              max / 2 - 1,
+              max / 2,
+              max - 1,
+              max})
+        {
+            BEAST_EXPECT(xahau_byzantine_bound(count) == count / 5);
+            BEAST_EXPECT(
+                xahau_participant_threshold(count) ==
+                calculateParticipantThreshold(count));
+            BEAST_EXPECT(
+                xahau_quorum_threshold(count) ==
+                calculateQuorumThreshold(count));
+        }
+    }
+
+    void
+    testSelectorAndGateDrift()
+    {
+        testcase("Lean/C++ entropy selector and gate drift");
+
+        initializeLean();
+
+        for (std::uint64_t effectiveView = 0; effectiveView <= 40;
+             ++effectiveView)
+        {
+            auto const expectedQuorum = safeQuorumThreshold(effectiveView);
+            BEAST_EXPECT(
+                xahau_safe_quorum_threshold(effectiveView) == expectedQuorum);
+
+            for (std::uint64_t originalView = 0; originalView <= 40;
+                 ++originalView)
+            {
+                auto const expectedParticipant =
+                    safeParticipantThreshold(originalView);
+
+                BEAST_EXPECT(
+                    xahau_safe_participant_threshold(originalView) ==
+                    expectedParticipant);
+                BEAST_EXPECT(
+                    xahau_entropy_gate_threshold_for_view(
+                        effectiveView, originalView) ==
+                    ConsensusExtensions::entropyGateThresholdForView(
+                        effectiveView, originalView));
+
+                for (std::uint64_t participantCount = 0; participantCount <= 45;
+                     ++participantCount)
+                {
+                    for (bool fromUNLReport : {false, true})
+                    {
+                        BEAST_EXPECT(
+                            xahau_select_entropy_tier(
+                                fromUNLReport ? 1 : 0,
+                                participantCount,
+                                effectiveView,
+                                originalView) ==
+                            static_cast<std::uint8_t>(
+                                ConsensusExtensions::selectEntropyTierForView(
+                                    fromUNLReport,
+                                    participantCount,
+                                    effectiveView,
+                                    originalView)));
+                    }
+                }
+            }
+        }
+    }
+
+    void
+    testSidecarAndExportGateDrift()
+    {
+        testcase("Lean/C++ sidecar alignment and export gate drift");
+
+        initializeLean();
+
+        for (std::uint64_t aligned = 0; aligned <= 12; ++aligned)
+        {
+            for (std::uint64_t threshold = 0; threshold <= 12; ++threshold)
+            {
+                for (bool localIsMember : {false, true})
+                {
+                    for (bool localPublished : {false, true})
+                    {
+                        auto const expectedAligned =
+                            detail::sidecarAlignedParticipants(
+                                aligned, localIsMember, localPublished);
+
+                        BEAST_EXPECT(
+                            xahau_aligned_participants(
+                                aligned,
+                                localIsMember ? 1 : 0,
+                                localPublished ? 1 : 0) == expectedAligned);
+                        BEAST_EXPECT(
+                            (xahau_quorum_aligned(
+                                 threshold,
+                                 aligned,
+                                 localIsMember ? 1 : 0,
+                                 localPublished ? 1 : 0) != 0) ==
+                            detail::sidecarQuorumAligned(
+                                aligned,
+                                localIsMember,
+                                localPublished,
+                                threshold));
+                    }
+                }
+
+                for (bool fullObservation : {false, true})
+                {
+                    BEAST_EXPECT(
+                        (xahau_export_gate_proceed(
+                             aligned, threshold, fullObservation ? 1 : 0) !=
+                         0) ==
+                        detail::exportSigSetQuorumAligned(aligned, threshold));
+                }
+            }
+        }
+
+        for (std::uint64_t peersSeen = 0; peersSeen <= 12; ++peersSeen)
+        {
+            for (std::uint64_t txConverged = 0; txConverged <= 12;
+                 ++txConverged)
+            {
+                detail::SidecarPeerAlignment state;
+                state.peersSeen = peersSeen;
+                state.txConverged = txConverged;
+
+                BEAST_EXPECT(
+                    (xahau_full_observation(peersSeen, txConverged) != 0) ==
+                    detail::sidecarFullObservation(peersSeen, txConverged));
+            }
+        }
+    }
+
+    void
+    testNunlCapDrift()
+    {
+        testcase("Lean/C++ NegativeUNL cap arithmetic drift");
+
+        initializeLean();
+
+        for (std::uint64_t originalView = 0; originalView <= 1024;
+             ++originalView)
+        {
+            auto const expectedCap =
+                NegativeUNLVote::maxNegativeUNLListed(originalView);
+            BEAST_EXPECT(xahau_disabled_cap(originalView) == expectedCap);
+
+            for (std::uint64_t disabled = 0; disabled <= 16; ++disabled)
+            {
+                auto const expectedEffective =
+                    disabled > originalView ? 0 : originalView - disabled;
+                BEAST_EXPECT(
+                    xahau_effective_view(originalView, disabled) ==
+                    expectedEffective);
+            }
+        }
+
+        auto const max = std::numeric_limits<std::uint64_t>::max();
+        for (std::uint64_t originalView :
+             {max / 4 - 1, max / 4, max / 2, max - 1, max})
+        {
+            BEAST_EXPECT(
+                xahau_disabled_cap(originalView) ==
+                NegativeUNLVote::maxNegativeUNLListed(originalView));
+        }
+    }
+
+    void
+    testViewUniverseDrift()
+    {
+        testcase("Lean/C++ view-universe safety predicate drift");
+
+        initializeLean();
+
+        for (std::uint64_t effectiveView = 0; effectiveView <= 40;
+             ++effectiveView)
+        {
+            for (std::uint64_t originalView = 0; originalView <= 40;
+                 ++originalView)
+            {
+                auto const threshold =
+                    calculateParticipantThreshold(originalView);
+                BEAST_EXPECT(
+                    (xahau_strict_intersection_safe(
+                         effectiveView, originalView, threshold) != 0) ==
+                    strictIntersectionSafeCpp(
+                        effectiveView, originalView, threshold));
+                BEAST_EXPECT(
+                    (xahau_nonvacuous_strict_intersection_safe(
+                         effectiveView, originalView, threshold) != 0) ==
+                    (threshold <= effectiveView &&
+                     strictIntersectionSafeCpp(
+                         effectiveView, originalView, threshold)));
+                BEAST_EXPECT(
+                    (xahau_participant_band_nonempty(
+                         effectiveView, originalView) != 0) ==
+                    participantBandNonemptyCpp(effectiveView, originalView));
+            }
+        }
+    }
+
+    void
+    testExportQuorumDrift()
+    {
+        testcase("Lean/C++ export quorum safety predicate drift");
+
+        initializeLean();
+
+        for (std::uint64_t activeView = 0; activeView <= 64; ++activeView)
+        {
+            auto const quorum = calculateQuorumThreshold(activeView);
+            auto const expectedOverlap =
+                2 * quorum > activeView ? 2 * quorum - activeView : 0;
+            BEAST_EXPECT(
+                xahau_export_quorum_overlap_lower_bound(activeView) ==
+                expectedOverlap);
+        }
+
+        for (std::uint64_t originalView = 0; originalView <= 64; ++originalView)
+        {
+            auto const cap =
+                NegativeUNLVote::maxNegativeUNLListed(originalView);
+            for (std::uint64_t disabled = 0; disabled <= cap + 2; ++disabled)
+            {
+                auto const effectiveView =
+                    disabled > originalView ? 0 : originalView - disabled;
+                auto const expected =
+                    disabled <= cap && effectiveView > 0 &&
+                    strictIntersectionSafeCpp(
+                        effectiveView,
+                        originalView,
+                        calculateQuorumThreshold(effectiveView));
+                BEAST_EXPECT(
+                    (xahau_export_quorum_safe_under_nunl_cap(
+                         originalView, effectiveView, disabled) != 0) ==
+                    expected);
+            }
+        }
+
+        struct NunlPremiseCase
+        {
+            std::uint64_t originalView;
+            std::uint64_t effectiveView;
+            std::uint64_t disabled;
+        };
+
+        for (auto const& c : {
+                 NunlPremiseCase{20, 15, 4},  // effective view should be 16
+                 NunlPremiseCase{20, 17, 4},  // effective view should be 16
+                 NunlPremiseCase{20, 14, 6},  // disabled is above cap
+                 NunlPremiseCase{10, 6, 4},   // disabled is above cap
+             })
+        {
+            BEAST_EXPECT(
+                xahau_export_quorum_safe_under_nunl_cap(
+                    c.originalView, c.effectiveView, c.disabled) == 0);
+        }
+    }
+
+    void
+    testSidecarMaskDrift()
+    {
+        testcase("Lean/C++ active-view sidecar mask drift");
+
+        initializeLean();
+
+        struct MaskCase
+        {
+            std::uint64_t count;
+            std::uint64_t activeMask;
+            std::uint64_t alignedMask;
+        };
+
+        auto const checkMaskCase = [&](MaskCase const& c) {
+            auto const aligned =
+                activeAlignedCountMaskCpp(c.count, c.activeMask, c.alignedMask);
+            BEAST_EXPECT(
+                xahau_active_aligned_count_mask(
+                    c.count, c.activeMask, c.alignedMask) == aligned);
+
+            for (std::uint64_t threshold = 0; threshold <= 12; ++threshold)
+            {
+                for (bool localIsMember : {false, true})
+                {
+                    for (bool localPublished : {false, true})
+                    {
+                        BEAST_EXPECT(
+                            (xahau_quorum_aligned_mask(
+                                 threshold,
+                                 c.count,
+                                 c.activeMask,
+                                 c.alignedMask,
+                                 localIsMember ? 1 : 0,
+                                 localPublished ? 1 : 0) != 0) ==
+                            detail::sidecarQuorumAligned(
+                                aligned,
+                                localIsMember,
+                                localPublished,
+                                threshold));
+                    }
+                }
+            }
+        };
+
+        for (std::uint64_t count = 0; count <= 6; ++count)
+        {
+            auto const maxMask = std::uint64_t{1} << count;
+            for (std::uint64_t activeMask = 0; activeMask < maxMask;
+                 ++activeMask)
+            {
+                for (std::uint64_t alignedMask = 0; alignedMask < maxMask;
+                     ++alignedMask)
+                {
+                    checkMaskCase(MaskCase{count, activeMask, alignedMask});
+                }
+            }
+        }
+
+        for (auto const& c : {
+                 MaskCase{8, 0b10110110, 0b11111111},
+                 MaskCase{12, 0b101010101010, 0b111100001111},
+                 MaskCase{63, std::uint64_t{1} << 62, std::uint64_t{1} << 62},
+                 MaskCase{64, std::uint64_t{1} << 63, std::uint64_t{1} << 63},
+                 MaskCase{
+                     64,
+                     (std::uint64_t{1} << 63) | 0b1011,
+                     (std::uint64_t{1} << 63) | 0b0110},
+             })
+        {
+            checkMaskCase(c);
+        }
+    }
+
+    void
+    testNaiveSixtyPercentRegression()
+    {
+        testcase("Lean/C++ naive 60 percent threshold regression anchors");
+
+        initializeLean();
+
+        for (std::uint64_t count = 0; count <= 1024; ++count)
+        {
+            auto const naive = (count * 60 + 99) / 100;
+            BEAST_EXPECT(xahau_naive_sixty_percent_threshold(count) == naive);
+            BEAST_EXPECT(
+                (xahau_naive_sixty_percent_is_safe(count) != 0) ==
+                strictIntersectionSafeCpp(count, count, naive));
+
+            if (count > 0 && count % 5 == 0)
+            {
+                BEAST_EXPECT(!strictIntersectionSafeCpp(count, count, naive));
+                BEAST_EXPECT(strictIntersectionSafeCpp(
+                    count, count, calculateParticipantThreshold(count)));
+            }
+        }
+    }
+
+    void
+    run() override
+    {
+        testThresholdFormulaDrift();
+        testSelectorAndGateDrift();
+        testSidecarAndExportGateDrift();
+        testNunlCapDrift();
+        testViewUniverseDrift();
+        testExportQuorumDrift();
+        testSidecarMaskDrift();
+        testNaiveSixtyPercentRegression();
+    }
+};
+
+BEAST_DEFINE_TESTSUITE(LeanConsensus, consensus, ripple);
+
+}  // namespace test
+}  // namespace ripple
+
+#endif

src/xrpld/consensus/ConsensusParms.h

@@ -226,7 +226,9 @@ struct ConsensusParms
 inline std::size_t
 calculateQuorumThreshold(std::size_t count)
 {
-    return (count * 80 + 99) / 100;
+    auto const whole = count / 100;
+    auto const remainder = count % 100;
+    return whole * 80 + (remainder * 80 + 99) / 100;
 }
 
 /** Safe quorum helper for consensus-extension gates.
@@ -274,7 +276,8 @@ calculateParticipantThreshold(std::size_t count)
     // f = floor(0.2 * count) tolerated Byzantine validators; the smallest t
     // with 2t - count > f is floor((count + f) / 2) + 1.
     auto const byzantine = count / 5;
-    return (count + byzantine) / 2 + 1;
+    auto const carry = (count % 2 + byzantine % 2) / 2;
+    return count / 2 + byzantine / 2 + carry + 1;
 }
 
 /** Safe Tier-2 helper for consensus-extension gates.