Mnehmos · Jul 19, 2026 · Jul 19, 2026 · Jul 19, 2026 · Jul 19, 2026 · Jul 19, 2026
@@ -13,40 +13,96 @@ concurrency:
   cancel-in-progress: true
 
 jobs:
-  verify:
+  rust:
+    name: Rust (${{ matrix.os }})
+    strategy:
+      fail-fast: false
+      matrix:
+        os: [ubuntu-latest, windows-latest]
+    runs-on: ${{ matrix.os }}
+    timeout-minutes: 20
+    steps:
+      - name: Check out source
+        uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+        with:
+          persist-credentials: false
+      - name: Report pinned toolchain
+        run: rustup show active-toolchain
+      - name: Check formatting
+        run: cargo fmt --check
+      - name: Lint with warnings denied
+        run: cargo clippy --workspace --all-targets --all-features -- -D warnings
+      - name: Run unit and integration tests
+        run: cargo test --workspace
+
+  storage-smoke:
+    name: Real storage smoke test
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    steps:
+      - name: Check out source
+        uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+        with:
+          persist-credentials: false
+      - name: Initialize instance
+        run: cargo run -- --root "${{ runner.temp }}/mcl-ci" --json init --actor github-actions --idempotency-key phase1-storage-smoke
+      - name: Check storage health
+        run: cargo run -- --root "${{ runner.temp }}/mcl-ci" --json health
+
+  lean-toolchain:
+    name: Pinned Lean availability
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    steps:
+      - name: Check out source
+        uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+        with:
+          persist-credentials: false
+      - name: Install repository-pinned Lean
+        shell: bash
+        run: |
+          set -euo pipefail
+          archive="${RUNNER_TEMP}/elan.tar.gz"
+          curl --fail --location --proto '=https' --tlsv1.2 \
+            --output "${archive}" \
+            https://github.com/leanprover/elan/releases/download/v4.2.3/elan-x86_64-unknown-linux-gnu.tar.gz
+          echo "df0b2b3a439961ffcbb3985214365ffe40f49bc871df04dff268c7d8e21ca8b2  ${archive}" \
+            | sha256sum --check --strict
+          tar --extract --gzip --file "${archive}" --directory "${RUNNER_TEMP}"
+          "${RUNNER_TEMP}/elan-init" -y --default-toolchain none --no-modify-path
+          echo "${HOME}/.elan/bin" >> "${GITHUB_PATH}"
+          "${HOME}/.elan/bin/elan" toolchain install "$(cat lean-toolchain)"
+      - name: Report exact Lean version
+        shell: bash
+        run: |
+          set -euo pipefail
+          lean --version | tee "${RUNNER_TEMP}/lean-version.txt"
+          grep --fixed-strings "Lean (version 4.32.0," "${RUNNER_TEMP}/lean-version.txt"
+      - name: Run real contained Lean worker integration
+        shell: bash
+        env:
+          MCL_RUN_LEAN_INTEGRATION: "1"
+        run: cargo test --test lean_worker -- --nocapture
+
+  legacy-python-regression:
+    name: Legacy Python regression evidence
     runs-on: ubuntu-latest
     timeout-minutes: 10
     steps:
-      - uses: actions/checkout@v4
+      - name: Check out source
+        uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
         with:
           persist-credentials: false
-      - uses: actions/setup-python@v5
+      - name: Set up Python
+        uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5.6.0
         with:
           python-version: "3.12"
           cache: pip
-      - name: Install MathOS
+      - name: Install legacy package
         run: python -m pip install -e .
-      - name: Compile and test
+      - name: Compile and test legacy slice
         env:
           PYTHONWARNINGS: error::ResourceWarning
         run: |
           python -m compileall -q src tests
           python -m unittest discover -s tests -v
-      - name: Run canonical vertical slice
-        run: mathos demo --workspace .ci-demo --reset
-      - name: Validate every RL export
-        run: |
-          for trajectory in .ci-demo/exports/*.json; do
-            mathos validate-export --input "$trajectory"
-          done
-      - name: Build wheel
-        run: python -m pip wheel --no-deps --wheel-dir dist .
-      - name: Smoke test installed wheel
-        run: |
-          python -m venv .wheel-venv
-          .wheel-venv/bin/python -m pip install --no-index dist/*.whl
-          .wheel-venv/bin/mathos demo --workspace .wheel-demo --reset
-          for trajectory in .wheel-demo/exports/*.json; do
-            .wheel-venv/bin/mathos validate-export --input "$trajectory"
-          done
-          .wheel-venv/bin/python -m pip check
@@ -71,6 +71,10 @@ lake-packages/
 # Rust
 target/
 **/*.rs.bk
+.toolchains/
+
+# Mathematical Claim Engine local state
+.mcl/
 
 # Jupyter
 .ipynb_checkpoints/

@@ -0,0 +1,11 @@
+# Changelog
+
+All notable changes are recorded here. The project follows Semantic Versioning after the `1.0.0` release.
+
+## Unreleased
+
+- Adopt the binding product and implementation specification at the repository root.
+- Begin the canonical Rust `mcl` modular monolith.
+- Reclassify the earlier Python finite-domain implementation as migration input rather than a finished product.
+- Add immutable pinned Lean environments and canonical verifier artifacts.
+- Add durable, idempotent Lean verifier requests with lease recovery and CLI inspection.