feat(python): add asyncio port with shared conformance replay

.github/actions/setup-validation/action.yml

@@ -1,5 +1,5 @@
 name: Set up validation
-description: Install the shared pinned Node/pnpm environment and optional Go/Quint tools.
+description: Install the shared pinned Node/pnpm environment and optional native language and Quint tools.
 inputs:
   go:
     description: Install the pinned Go toolchain.
@@ -13,6 +13,12 @@ inputs:
   rust:
     description: Install the pinned Rust toolchain (rust/rust-toolchain.toml) with clippy and rustfmt.
     default: "false"
+  python:
+    description: Install Python and the editable package with test and Redis dependencies.
+    default: "false"
+  python-version:
+    description: Python version for the native validation lane.
+    default: "3.14"
 runs:
   using: composite
   steps:
@@ -26,6 +32,18 @@ runs:
     - name: Install project dependencies
       shell: bash
       run: corepack pnpm install --frozen-lockfile
+    - uses: actions/setup-python@ece7cb06caefa5fff74198d8649806c4678c61a1 # v6
+      if: inputs.python == 'true'
+      with:
+        python-version: ${{ inputs.python-version }}
+        cache: pip
+        cache-dependency-path: python/pyproject.toml
+    - name: Install Python package and validation dependencies
+      if: inputs.python == 'true'
+      shell: bash
+      run: |
+        python -m venv python/.venv
+        python/.venv/bin/python -m pip install -e './python[test,redis]'
     - uses: actions/setup-go@924ae3a1cded613372ab5595356fb5720e22ba16 # v6
       if: inputs.go == 'true'
       with:

.github/workflows/docs.yaml

@@ -23,6 +23,7 @@ jobs:
         with:
           go: "true"
           rust: "true"
+          python: "true"
       - run: make docs
       - uses: actions/upload-pages-artifact@7b1f4a764d45c48632c6b24a0339c27f5614fb0b # v4
         if: github.ref == 'refs/heads/main' && github.event_name != 'pull_request'

.github/workflows/formal-full.yaml

@@ -33,6 +33,7 @@ jobs:
           quint: "true"
           go: "true"
           rust: "true"
+          python: "true"
       - name: Explore a fresh recorded seed and replay every port
         run: make explore
       - name: Preserve exploratory sources, seed and counterexamples
@@ -288,6 +289,35 @@ jobs:
           if-no-files-found: warn
           retention-days: 14
 
+  python-parity:
+    needs: generate
+    runs-on: ubuntu-latest
+    timeout-minutes: 40
+    steps:
+      - uses: actions/checkout@d23441a48e516b6c34aea4fa41551a30e30af803 # v6.1.0
+      - uses: ./.github/actions/setup-validation
+        with:
+          python: "true"
+      - uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 # v4.3.0
+        with:
+          name: formal-traces
+          path: .formal-traces
+      - name: Require Python replay of every generated obligation
+        run: make formal-python
+      - name: Preserve Python completion evidence
+        if: always()
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
+        with:
+          name: python-parity-evidence
+          path: |
+            .formal-traces/python-replay.jsonl
+            .formal-traces/python-replay-summary.json
+            .formal-traces/python-context.json
+            .formal-traces/python-completion.json
+          include-hidden-files: true
+          if-no-files-found: warn
+          retention-days: 14
+
   # The Go lane bounds the whole workflow: every mutant replays the generated
   # cohort, about 1.6 minutes per mutant on a fast runner and about 3 on the
   # slow class (13 mutants took 25 minutes in run 34660598461 and 47-48 in
@@ -421,7 +451,7 @@ jobs:
   # The mutation lanes count through their merge jobs: a merge succeeds only
   # when every shard's report is present, consistent and free of lost detections.
   formal-full:
-    needs: [check-models, generate, typescript-parity, symbolic, typescript-mutations-merge, go-parity, go-mutations-merge, rust-parity, rust-mutations-merge, exploration]
+    needs: [check-models, generate, typescript-parity, symbolic, typescript-mutations-merge, go-parity, go-mutations-merge, rust-parity, rust-mutations-merge, python-parity, exploration]
     if: always()
     runs-on: ubuntu-latest
     timeout-minutes: 5
@@ -458,6 +488,13 @@ jobs:
         with:
           name: model-check-evidence
           path: formal-summary/model-check
+      - name: Collect Python completion evidence
+        if: always()
+        continue-on-error: true
+        uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 # v4.3.0
+        with:
+          name: python-parity-evidence
+          path: formal-summary/python
       - name: Collect symbolic verification report
         if: always()
         continue-on-error: true
@@ -486,6 +523,9 @@ jobs:
             formal-summary/rust/rust-completion.json
             formal-summary/rust/rust-context.json
             formal-summary/rust/rust-replay-summary.json
+            formal-summary/python/python-completion.json
+            formal-summary/python/python-context.json
+            formal-summary/python/python-replay-summary.json
             formal-summary/model-check/model-properties/report.json
             formal-summary/symbolic/report.json
             formal-summary/exploration/*/report.json
@@ -502,6 +542,7 @@ jobs:
           GO_MUTATIONS_MERGE_RESULT: ${{ needs.go-mutations-merge.result }}
           RUST_MUTATIONS_MERGE_RESULT: ${{ needs.rust-mutations-merge.result }}
           RUST_RESULT: ${{ needs.rust-parity.result }}
+          PYTHON_RESULT: ${{ needs.python-parity.result }}
           SYMBOLIC_RESULT: ${{ needs.symbolic.result }}
           EXPLORATION_RESULT: ${{ needs.exploration.result }}
           EXPLORATION_REQUIRED: ${{ github.event_name == 'schedule' || inputs.exploration == true }}
@@ -514,6 +555,7 @@ jobs:
           test "$GO_MUTATIONS_MERGE_RESULT" = success
           test "$RUST_MUTATIONS_MERGE_RESULT" = success
           test "$RUST_RESULT" = success
+          test "$PYTHON_RESULT" = success
           test "$SYMBOLIC_RESULT" = success
           if [ "$EXPLORATION_REQUIRED" = true ]; then
             test "$EXPLORATION_RESULT" = success

.github/workflows/formal.yaml

@@ -25,6 +25,7 @@ jobs:
         with:
           go: "true"
           rust: "true"
+          python: "true"
       - name: Audit contracts and replay committed Quint smoke in every port
         run: make audit smoke
       - name: Detect changes requiring fresh Quint artifact generation

.github/workflows/python.yml

@@ -0,0 +1,59 @@
+name: Python
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: python-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  native:
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    permissions:
+      contents: read
+      id-token: write
+    strategy:
+      fail-fast: false
+      matrix:
+        python: ["3.11", "3.14"]
+    steps:
+      - uses: actions/checkout@d23441a48e516b6c34aea4fa41551a30e30af803 # v6.1.0
+      - uses: ./.github/actions/setup-validation
+        with:
+          python: "true"
+          python-version: ${{ matrix.python }}
+      - name: Check native behavior, portable wire vectors and shared smoke histories
+        run: make check-python
+      - name: Check Redis, Valkey, Cluster and TypeScript interoperability
+        run: make integration-python
+      - name: Build a distributable wheel
+        run: python/.venv/bin/python -m pip wheel --no-deps ./python --wheel-dir .formal-traces/python-dist
+      - name: Upload Python coverage to Codecov
+        uses: codecov/codecov-action@fb8b3582c8e4def4969c97caa2f19720cb33a72f # v7.0.0
+        with:
+          files: ./coverage/python/native.lcov,./coverage/python/Redis.lcov,./coverage/python/Valkey.lcov
+          flags: python
+          name: python-${{ matrix.python }}
+          disable_search: true
+          use_oidc: true
+          fail_ci_if_error: true
+      - name: Retain the built wheel, coverage and integration diagnostics
+        if: always()
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
+        with:
+          name: python-${{ matrix.python }}-validation
+          path: |
+            .formal-traces/python-dist/
+            .formal-traces/python-integration*
+            coverage/python/*.lcov
+          include-hidden-files: true
+          if-no-files-found: warn
+          retention-days: 14

.gitignore

@@ -15,3 +15,11 @@ docs/generated/
 .vscode/
 *.log
 rust/target/
+python/.venv/
+__pycache__/
+*.py[cod]
+.pytest_cache/
+.ruff_cache/
+*.egg-info/
+python/build/
+python/dist/

AGENTS.md

@@ -2,7 +2,7 @@
 
 ## Project overview
 
-DialCache has TypeScript, Go and Rust implementations with explicit request-scoped enablement, local and Redis layers, runtime rollout controls, request coalescing, targeted invalidation, and adapter-based observability.
+DialCache has TypeScript, Go, Rust and Python implementations with explicit request-scoped enablement, local and Redis layers, runtime rollout controls, request coalescing, targeted invalidation, and adapter-based observability.
 
 ## Structure
 
@@ -31,6 +31,7 @@ typescript/             # Published npm package, README and build configuration
   scripts/              # Package checks and TypeScript benchmarks
 go/                     # Go module, public cache and adapters, shared-corpus replay
 rust/                   # Rust crate, public cache and adapters, shared-corpus replay (tests/conformance.rs)
+python/                 # Async Python package, borrowed Redis adapter, native tests and shared-corpus replay
 formal/                 # Quint behavioral source of truth, contracts and portable vectors
 scripts/                # Shared documentation tools
 package.json            # Private shared tooling and TypeScript command dispatch
@@ -72,17 +73,17 @@ pnpm-lock.yaml          # Shared workspace dependency lockfile
   prose once, import executable native examples by named region, and keep real
   language differences in `LanguageContent` notes or the short native guides.
   `make docs` generates all native references and checks snippet sources and
-  internal links; it requires the pinned Go and Rust toolchains as well as Node.
+  internal links; it requires the pinned Go and Rust toolchains, Python and Node.
   Run changed native examples with assertions (including Redis when relevant).
 - Start formal work at `formal/README.md`. `formal/WALKTHROUGH.md` follows one
-  contract through Quint, generated inputs and all three language replays;
+  contract through Quint, generated inputs and the native language replays;
   `formal/AUTHORING.md` explains how to extend that chain. Read the relevant
   model and profile bindings before opening large generated JSON artifacts.
 - For formal specification changes, follow `formal/AUTHORING.md`: keep models
   readable as behavior definitions, share helpers with identical meaning, retain
   independent property checks, and register executable evidence in the catalogs.
 - Define portable behavior in Quint first. Require consequential generated
-  witnesses and replay the same histories in TypeScript, Go and Rust; keep
+  witnesses and replay the same histories in TypeScript, Go, Rust and Python; keep
   native API, wire and integration tests for their explicit boundaries.
 - Use the shared behavioral testbed for portable features and bug fixes, with
   TypeScript as the executable reference. Follow the workflow in
@@ -100,6 +101,13 @@ make integration
 
 `make check-rust` runs the Rust crate's fmt, clippy, unit, vector, scenario and
 smoke checks; `make formal-rust` completes its replay of the generated corpus.
+For Python, create `python/.venv` with Python 3.11 or later and install
+`python/.venv/bin/python -m pip install -e './python[test,redis]'`.
+`make check-python` runs native, wire and committed smoke tests;
+`make integration-python` provisions isolated Redis/Valkey/Cluster servers;
+`make formal-python` runs the prepared generated corpus and completion checks.
+Set `PYTHON` to use another prepared interpreter. Python's package has no Node
+runtime dependency; the shared replay and validation tools require Node 24.
 Use `make formal` for complete Quint model checks, corpus generation and every
 port's full replay, then `make mutations` for assertion-strength checks.
 `make ci` runs all validation in the required order. `make help` lists targets

Makefile

@@ -5,7 +5,7 @@
 
 NODE ?= node
 
-.PHONY: help check check-ts check-go check-rust docs audit smoke formal formal-check formal-generate formal-ts formal-go formal-rust fixtures-check kernel-fixtures differential mutations mutations-ts mutations-go mutations-merge-ts mutations-merge-go mutations-rust mutations-merge-rust integration integration-ts integration-go integration-rust package-floor ci explore model-check
+.PHONY: help check check-ts check-go check-rust check-python docs audit smoke formal formal-check formal-generate formal-ts formal-go formal-rust formal-python fixtures-check kernel-fixtures differential mutations mutations-ts mutations-go mutations-merge-ts mutations-merge-go mutations-rust mutations-merge-rust integration integration-ts integration-go integration-rust integration-python package-floor ci explore model-check
 
-help check check-ts check-go check-rust docs audit smoke formal formal-check formal-generate formal-ts formal-go formal-rust fixtures-check kernel-fixtures differential mutations mutations-ts mutations-go mutations-merge-ts mutations-merge-go mutations-rust mutations-merge-rust integration integration-ts integration-go integration-rust package-floor ci explore model-check:
+help check check-ts check-go check-rust check-python docs audit smoke formal formal-check formal-generate formal-ts formal-go formal-rust formal-python fixtures-check kernel-fixtures differential mutations mutations-ts mutations-go mutations-merge-ts mutations-merge-go mutations-rust mutations-merge-rust integration integration-ts integration-go integration-rust integration-python package-floor ci explore model-check:
 	$(NODE) formal/validation.mjs $@

README.md

@@ -5,16 +5,19 @@
 [![TypeScript coverage](https://img.shields.io/codecov/c/github/lan17/DialCache/main?flag=typescript&label=TypeScript%20coverage)](https://codecov.io/gh/lan17/DialCache)
 [![Go coverage](https://img.shields.io/codecov/c/github/lan17/DialCache/main?flag=go&label=Go%20coverage)](https://codecov.io/gh/lan17/DialCache)
 [![Rust coverage](https://img.shields.io/codecov/c/github/lan17/DialCache/main?flag=rust&label=Rust%20coverage)](https://codecov.io/gh/lan17/DialCache)
+[![Python coverage](https://img.shields.io/codecov/c/github/lan17/DialCache/main?flag=python&label=Python%20coverage)](https://codecov.io/gh/lan17/DialCache)
 [![OpenSSF Scorecard](https://api.scorecard.dev/projects/github.com/lan17/DialCache/badge)](https://scorecard.dev/viewer/?uri=github.com/lan17/DialCache)
 
 Read the [shared behavior guides](https://lan17.github.io/DialCache/) with a
-language selector for TypeScript, Go and Rust. Native examples in those guides
+language selector for TypeScript, Go, Rust and Python. Native examples in those guides
 are imported from source files that CI executes.
 
-**TypeScript is the reference implementation. Go and Rust are experimental.**
+**TypeScript is the reference implementation. Go, Rust, and Python are experimental.**
+The [Python asyncio guide](python/README.md) covers its native decorator API,
+request scopes, and checkout installation.
 
 DialCache organizes caching into use cases, with runtime control and
-observability for each one. Its TypeScript, Go and Rust implementations share
+observability for each one. Its TypeScript, Go, Rust and Python implementations share
 behavioral contracts and documentation.
 
 - **Off by default:** caching runs only inside an `enable()` scope.
@@ -36,6 +39,7 @@ behavioral contracts and documentation.
 | TypeScript | [`typescript/`](typescript/) — reference implementation | [TypeScript and npm](typescript/README.md) |
 | Go | [`go/`](go/) — experimental | [Go guide](go/README.md) |
 | Rust | [`rust/`](rust/) — experimental | [Rust guide](rust/README.md) · [crates.io](https://crates.io/crates/dialcache) |
+| Python | [`python/`](python/) — experimental | [Python guide](python/README.md) |
 
 Shared contracts and portable test histories live in [`formal/`](formal/).
 Run repository validation from the root; see the
@@ -152,9 +156,9 @@ for sampling and comparison behavior.
 | Recovery from selected source failures | [Stale-on-error](https://lan17.github.io/DialCache/stale-on-error.html) |
 | Shared execution and deadlines | [Coalescing and liveness](https://lan17.github.io/DialCache/coalescing.html) |
 | Methods, options, and exports | [API reference](https://lan17.github.io/DialCache/api.html) |
-| Native implementations and shared behavior contracts | [TypeScript guide](typescript/README.md) · [Go guide](go/README.md) · [Rust guide](rust/README.md) · [Quint specification](formal/README.md) · [Worked walkthrough](formal/WALKTHROUGH.md) |
+| Native implementations and shared behavior contracts | [TypeScript guide](typescript/README.md) · [Go guide](go/README.md) · [Rust guide](rust/README.md) · [Python guide](python/README.md) · [Quint specification](formal/README.md) · [Worked walkthrough](formal/WALKTHROUGH.md) |
 
-The Go port, the Rust port and the TypeScript library replay the same
+The Go, Rust, and Python ports and the TypeScript library replay the same
 Quint-generated histories. Whether those histories reach every required boundary is decided by
 one language-neutral evaluator, `node formal/witnesses.mjs evaluate`, that any
 port runs over the same corpus; no port depends on another port's test suite

docs/.vitepress/config.mts

@@ -28,6 +28,7 @@ export default defineConfig({
           { text: "TypeScript setup", link: "/languages/typescript" },
           { text: "Go setup", link: "/languages/go" },
           { text: "Rust setup", link: "/languages/rust" },
+          { text: "Python setup", link: "/languages/python" },
         ],
       },
       {

docs/api.md

@@ -15,6 +15,7 @@ behavior; the native references give each language's signatures and types.
 | TypeScript | <a href="./reference/typescript/index.html" target="_self">TypeDoc</a> | [TypeScript guide](languages/typescript.md) |
 | Go | <a href="./reference/go/index.html" target="_self">Go package documentation</a> | [Go guide](languages/go.md) |
 | Rust | <a href="./reference/rust/dialcache/index.html" target="_self">rustdoc</a> | [Rust guide](languages/rust.md) |
+| Python | <a href="./reference/python/index.html" target="_self">pydoc</a> | [Python guide](languages/python.md) |
 
 <LanguageContent language="go">
 
@@ -33,6 +34,15 @@ values. [Rust setup](languages/rust.md) explains ownership and feature flags.
 
 </LanguageContent>
 
+<LanguageContent language="python">
+
+Use the generated Python reference for `DialCache`, `Policy`, `Key`, serializers,
+semantic Redis requests and protocol helpers. Methods use Python snake_case;
+cache calls are awaitable. [Python setup](languages/python.md) explains context
+lifetime, argument binding and application-owned clients.
+
+</LanguageContent>
+
 <LanguageContent language="typescript">
 
 The following TypeScript usage notes retain the established guide anchors.