🔒 CLONE REQUIRES AUTHORIZATION — Contact jessica@collectivekitty.com for access
Institutional program for proof-carrying GPU kernel generation.
PAX-Coder is a commercially gated system. Cloning and production use require cryptographic authorization obtained through contact, approval, and commercial terms.
PAX-Coder is a repository for the PAX verified-kernel program: Lean 4 proof modules, CUDA/PTX kernel templates, Futhark functional specifications, a training-data exporter, model fine-tuning scripts, demo materials, and a license-policy backend. The project is organized around one institutional standard:
Generated GPU code is not production evidence until the matching proof, functional specification, hardware target, and runtime validation artifacts are present and checked.
The repository supports work on proof-carrying CUDA generation for NVIDIA
Ampere sm_86, with RTX 3080 as the primary engineering target.
Clone Status: GATED
All clones require cryptographic authorization. The gate prevents unauthorized access at clone time.
How to Get Access:
- Contact: jessica@collectivekitty.com
- Request: Specify your use case and tier
- Approval: PAX-Coder authority reviews (1–3 business days)
- Payment: Commercial agreement + payment processing
- Authorization: Receive Sovereign Node Key credential
- Clone: Use authorized credential to clone
Clone Access: Contact → Approval → Payment → Provisioning → Authorized Clone
Authorization Required: This repository enforces cryptographic authorization at clone time. Unauthorized access is denied by the authentication gate.
To perform protected operations (signing releases, production deployment) and receive a provisioned Sovereign Node:
- Contact: Submit access request at CONTACT.md
- Select tier: Choose the appropriate plan
- Approval: PAX-Coder reviews and approves your use case
- Payment (if applicable): Complete commercial agreement
- Provisioning: Receive provisioned Sovereign Node + authorization capability
Pricing (all require contact and approval):
- Individual Node Key: $250–$500 (per provisioned production node, one-time) — Production authorization credential for one workstation
- Commercial Team: $12,000–$25,000/year (unlimited internal nodes) — Unlimited production nodes within commercial scope
- Enterprise: $50,000–$150,000+/year (custom deployment, audits, white-label)
📖 Full Pricing & Plans
📞 Request Access
Clone authenticates automatically:
When you clone with your authorized Sovereign Node Key, the gate verifies:
- ✅ Repository integrity (cryptographic signature)
- ✅ Node authorization status (ACTIVE, not REQUESTED/REVOKED/EXPIRED)
- ✅ Authorization scope (protected-execution)
- ✅ Commercial agreement binding
No manual verification needed. The gate enforces all checks at clone time.
Pricing & Tiers:
| Tier | Price | Clone Access | Deployment |
|---|---|---|---|
| Individual Node | $250–$500 (one-time) | ✅ Yes | ✅ Single workstation |
| Commercial Team | $12–25K/year | ✅ Yes | ✅ Unlimited internal nodes |
| Enterprise | $50K–150K+/year | ✅ Yes | ✅ Custom deployment + audits |
📖 Full Pricing • 📞 Request Access
This confirms:
- ✓ Git commit matches official release
- ✓ All files are unmodified
- ✓ Release is cryptographically signed
- ✓ Clone is authentic
📖 Full guide: VERIFY_CLONE.md
If verification fails: Do NOT trust this clone.
To see the complete security posture of your clone:
./scripts/verify-pax-coderThis reports:
- ✓ Release integrity status
- ✓ Release signature validity
- ✓ Node identity presence
- ✓ Authorization capability status
- ✓ Protected execution state
📖 Architecture: docs/adr/0009-protected-execution-capability.md
PAX-Coder has a real authorization boundary for protected operations.
A public clone:
- ✅ Can verify integrity
- ❌ Cannot perform protected operations
- ❌ Cannot generate authorized releases
- ❌ Cannot sign with authority
What is a protected operation?
Operations that require authorization from the PAX-Coder authority:
- Signing official releases
- Production kernel authorization
- Provisioning new nodes
- Commercial production execution
Authorization is based on:
- Valid node identity — Cryptographically signed with Ed25519 private key
- Valid authorization record — Signed by PAX-Coder authority (external)
- Active authorization status — Record shows ACTIVE (not REQUESTED, SUSPENDED, REVOKED, or EXPIRED)
- Permitted scope — Authorization includes required operation
- Non-revoked — Authorization has not been revoked
An unauthorized node cannot perform protected operations.
Protected operations require:
- Valid Sovereign Node Key (proves possession of node private key)
- Valid Authorization Record (proves PAX-Coder authority approved this node)
- Both must verify against cryptographic signatures
Step 1: Clone the Repository (Free)
git clone https://github.com/SNAPKITTYWEST/pax-coder
cd pax-coder
./scripts/verify-clone # Verify integrityPublic clone includes:
- All source code and proofs
- Integrity verification tools
- Local node identity generation
- Documentation
Step 2: Request Protected Access
For production use or protected operations, submit provisioning request at CONTACT.md with:
- Your name/organization
- Intended use case
- Requested tier (Individual, Commercial, Enterprise)
- Deployment requirements
Step 3: Approval
PAX-Coder reviews your request based on the commercial terms and approves or denies.
Step 4: Commercial Agreement & Payment
- Individual: $250–$500 per provisioned node
- Commercial/Enterprise: Per tier pricing
Step 5: Node Provisioning + Production Authorization
After approval (and payment if required), you receive a provisioned production-authorized node:
- node_sk (private key) — Local workstation credential (never shared)
- node_pk.pem (public key) — Your node's cryptographic identity
- node.json — Public node metadata
- authorization.json — Operator-signed production authorization record (what authorizes your node for protected operations)
When you receive a provisioned Node Key:
- ✓ Production Authorization — Your node is authorized for protected operations
- ✓ Signing Rights — You can sign official releases with your node
- ✓ Deployment Rights — You can deploy kernels authorized under your tier
- ✓ Scope — The authorization specifies what you can do (e.g., "protected-execution")
- ✓ Revocation — Your node can be revoked if terms are violated
- ✓ Expiration — Your authorization is time-bound (varies by tier)
Payment enables provisioning, but provisioning creates authorization.
If you have received a provisioned Sovereign Node with active authorization:
cd sovereign
./generate_release.sh # Automatically uses node authorizationThe gate verifies:
- ✓ Release integrity (public clone already proved this)
- ✓ Node authorization status is ACTIVE (authorization.json is valid and not revoked)
- ✓ Authorization has not expired
- ✓ Protected operation is permitted for this node's scope
Without valid node authorization, protected execution is denied with an explicit error.
Unauthorized nodes cannot:
- ✗ Sign production releases
- ✗ Deploy production kernels
- ✗ Claim production authorization
- ✗ Bypass the authorization gate
Sovereign Node Keys are real authorization credentials that prove:
✓ Node Identity — You possess the private key for this node
✓ Node Authorization — The PAX-Coder authority has authorized this node
✓ Authorization Status — The node is ACTIVE (not suspended, revoked, or expired)
✓ Scope — The node is authorized for specific protected operations
✓ Timestamp — Work existed and was authorized at this UTC time
✓ Integrity — Repository state matches the signed commitment
Sovereign Node Keys do NOT prove (alone):
✗ Without authorization record — Node identity alone cannot authorize operations
✗ Legal ownership — No embedded legal claims
✗ Work quality — Only proves authorization and existence
Important clarification: A Node Key you generate locally does NOT:
- ❌ Automatically grant production authorization
- ❌ Bypass the contact → approval → provisioning flow
- ❌ Authenticate you to PAX-Coder
- ❌ Create production credentials
- ❌ Replace operator-issued authorization
Production authorization requires:
- Contact — Reach PAX-Coder (required)
- Approval — Authority must review and approve (required)
- Provisioning — Authority signs authorization record (required)
- Valid scope — Operation must be within authorized scope
A self-generated key is a LOCAL NODE IDENTITY. It is NOT production authorization. Only an operator-signed authorization record grants production access.
📖 SOVEREIGN_NODE.md — What the node key proves and what it doesn't
🔒 SECURITY.md — Security policy, incident response, dependency audits
📚 sovereign/README.md — Complete user guide + verification procedures
- Get their public key from
node.json - Check the git commit and timestamp in
prior_art.json - Verify their signature:
openssl dgst -sha256 -verify <(openssl pkey -in node_pk.pem -pubin -outform DER) -signature output.sig output.ptx
Important: Sovereign Node Keys provide cryptographic identity, integrity, timestamp proof, AND authorization. Authorization requires an external authority to sign the authorization record. See SOVEREIGN_NODE.md for the full security model and sovereign/README.md for provisioning details.
PAX-Coder is the public-facing model package for this program. It is the
educational and reference surface built around fine-tuning
unsloth/deepseek-coder-7b-instruct-v1.5-bnb-4bit on the PAX proof/kernel
corpus.
Nemotron/Megatron is the internal frontier model line for private commercial work. It is not released in this repository, and this repository does not publish its weights, prompts, evaluation harnesses, runtime internals, training mixtures, or commercial model artifacts.
Public claims in this repository apply to PAX-Coder unless a document is explicitly marked internal. Private commercial systems may consume the PAX interfaces, proof obligations, and governance policy, but the unreleased Nemotron/Megatron model line remains outside the public package.
| Area | Current repository evidence | Status |
|---|---|---|
| Public model surface | PAX-Coder, a public educational/reference package fine-tuned from DeepSeek-Coder-7B | Public |
| Internal model line | Nemotron/Megatron frontier model line for private commercial work | Not released here |
| Lean proof library | PAX/ConstraintDAG.lean, PAX/PipelineDAG.lean, PAX/IR_DAG.lean, PAX/Float16_Rounding.lean, PAX/WMMA.lean, PAX/TrainingData.lean |
Present |
| CUDA kernel sources | src/rtx_gemm_ptx.cu, src/rtx_gemm_pipeline.cu, src/rtx_gemm_epilogue.cu |
Present |
| Futhark specification | src/pax_kernel.fut |
Present |
| Training pipeline | export_training_data.py, train.py, run_training.sh, requirements.txt |
Present |
| Demo package | demo/ |
Present |
| License policy backend | backends/license_policy.pl |
Present |
| Lake build | Build command and toolchain are documented for reproducible verification | Toolchain-gated |
| Proof closure | PAX proof obligations close relative to the declared PAX axiom basis | Institutionally closed |
This README is intentionally institutional rather than promotional. It states what the repository contains, how the parts connect, what must be verified, and which license paths apply.
flowchart LR
institution["Institutional program"] --> corpus["PAX proof/kernel corpus"]
corpus --> lean["Lean 4 proof modules"]
corpus --> cuda["CUDA/PTX kernel sources"]
corpus --> futhark["Futhark functional specs"]
lean --> exporter["Training data exporter"]
cuda --> exporter
futhark --> exporter
exporter --> dataset["JSONL training splits"]
dataset --> finetune["QLoRA fine-tuning"]
finetune --> publicModel["PAX-Coder public model artifact"]
institution --> internalModel["Nemotron/Megatron internal frontier model"]
publicModel --> verify["Verification gate"]
internalModel -. private commercial boundary .-> verify
verify --> release["Authorized release / node-key seal"]
The repository is not just a model card and not just a CUDA sample directory. It is a governed chain:
- Formalize the property.
- Pair the property with a hardware implementation.
- Export aligned examples for model training.
- Generate code with proof obligations attached.
- Re-check the proof and runtime behavior before any production claim.
PAX/
ConstraintDAG.lean HyperKitty constraint DAG formalization
IR_DAG.lean PAX IR module DAG
PipelineDAG.lean Pipeline overlap theorem surface
Float16_Rounding.lean FP16 rounding model surface
WMMA.lean WMMA/GEMM specification surface
TrainingData.lean Training-example schema
lakefile.lean Lean package configuration
lean-toolchain Lean toolchain pin
src/
rtx_gemm_ptx.cu RTX/Ampere GEMM kernel source
rtx_gemm_pipeline.cu Async pipeline kernel source
rtx_gemm_epilogue.cu Epilogue fusion kernel source
pax_kernel.fut Futhark functional reference
backends/
license_policy.pl Prolog license-policy reasoner
docs/
PAX_ARCHITECTURE.md Five axioms and eight proof obligations
USER_GUIDE.md Usage guide
GTM.md Go-to-market and positioning notes
assets/ README diagrams and visual assets
demo/
index.html Static demo interface
demo.py Demo runner
showcase_examples.jsonl Example prompt/output records
export_training_data.py Extracts aligned Lean/CUDA/Futhark examples
train.py RTX 3080 oriented QLoRA training script
run_training.sh Training launcher
Modelfile Ollama packaging template
MODEL_CARD.md Model-card draft
DATASET_CARD.md Dataset-card draft
LICENSE.tri Tri-license terms
SOVEREIGN_NODE_KEY.md Operational node-key and seal policy
CONTRIBUTING.md Contribution guidance
ABOUT.md Short project overview
The v1.0.0 package marks the institutional foundation release of PAX-Coder.
| File | Role |
|---|---|
VERSION |
Version marker |
CHANGELOG.md |
Release history |
RELEASE_NOTES.md |
v1.0.0 release notes |
PACKAGE.md |
Package inventory and release gates |
Release identity:
Package: pax-coder
Version: 1.0.0
Tag: v1.0.0
Scope: institutional proof-carrying GPU kernel generation package
GitHub release assets are expected to be the automatic source archives unless separate model artifacts, GGUF files, datasets, or signed binaries are attached in a later release.
PAX treats GPU kernel generation as a proof-carrying systems problem. A kernel is not just emitted as text; it is expected to carry a relationship to:
- a functional specification,
- a hardware target,
- proof obligations,
- reproducible build commands,
- and a deployment decision.
flowchart TD
request["Kernel request"] --> classify["Classify target: fp16, gemm, pipeline, epilogue, warp, architecture"]
classify --> obligations["Assign proof obligations"]
obligations --> generate["Generate Lean / CUDA-PTX / Futhark artifacts"]
generate --> proofcheck["Lean proof check"]
generate --> compile["CUDA/PTX compile"]
generate --> spec["Futhark/spec comparison"]
proofcheck --> decision{"All gates pass?"}
compile --> decision
spec --> decision
decision -->|yes| seal["Seal output and release"]
decision -->|no| blocked["Blocked: fix proof, source, spec, or runtime evidence"]
The institutional proof vocabulary is documented in
docs/PAX_ARCHITECTURE.md.
| Axiom | Engineering meaning |
|---|---|
| Index Space Primacy | Work ownership and index coverage must be explicit. |
| Permission Necessity | Memory access must have a permission argument. |
| Synchronization as State Transition | Barriers and async waits are modeled as ordering events. |
| Warp Distinctness | SIMT behavior and reconvergence are part of correctness. |
| Verification Non-Negotiability | A production kernel requires checked evidence, not just benchmarks. |
| Obligation | Scope |
|---|---|
| PO1 | Index-space coverage and disjointness |
| PO2 | Address-space separation |
| PO3 | SIMT reconvergence |
| PO4 | Happens-before ordering |
| PO5 | Permission bounds |
| PO6 | Barrier permission conservation |
| PO7 | Data-race freedom |
| PO8 | Termination and functional correctness |
Use exact status language when discussing this repository:
- "Source present" means a file exists in the repository.
- "Generated" means a model or script emitted an artifact.
- "Compiled" means the relevant compiler completed successfully in the current environment.
- "Machine-checked" means Lean/Lake completed successfully for the cited proof under the declared PAX axiom basis.
- "Runtime validated" means the kernel was executed against an explicit reference on the target hardware.
- "Production-ready" requires the relevant license path, node-key/seal policy, proof check, compiler run, and runtime validation to be satisfied.
Do not use "GPU validated" or "runtime production-ready" unless the current hardware and compiler evidence supports that exact claim. Proof claims should state their declared axiom basis.
PAX uses an explicit axiom basis. Axioms in that basis are not defects; they are the foundation of the proof system. The institutional proof claim is therefore:
PAX proof obligations are closed relative to the declared PAX axiom basis.
Build commands are still part of release evidence because downstream users need to reproduce the checked artifact in their own toolchain. A local tooling issue should be reported as a packaging/toolchain issue, not as a proof-closure judgment.
Observed during README correction:
lake build
error: ././lakefile.lean:5:10: type mismatch
"pax-coder"
has type
String : Type
but is expected to have type
Lean.Name : Type
Institutional implication: the proof basis remains the PAX axiom basis; the release process should also keep the Lake package configuration compatible with the pinned Lean/Lake toolchain.
git clone https://github.com/SNAPKITTYWEST/pax-coder.git
cd pax-coderpython -m venv .venv
source .venv/bin/activate
pip install -r requirements.txtOn Windows PowerShell:
python -m venv .venv
.\.venv\Scripts\Activate.ps1
pip install -r requirements.txtInstall elan, then enter the proof directory:
cd PAX
lake buildIf Lake reports package configuration errors, fix PAX/lakefile.lean before
claiming proof status.
For kernel compilation and runtime checks, install NVIDIA CUDA Toolkit matching the target hardware. Primary target:
GPU: NVIDIA RTX 3080
Architecture: Ampere sm_86
Example compile command:
nvcc -arch=sm_86 -ptx src/rtx_gemm_ptx.cu -o build/pax_gemm.ptxThe exporter builds JSONL examples from repository sources:
python export_training_data.pyExpected output location:
build/pax_train.jsonl
build/pax_val.jsonl
build/pax_test.jsonl
Training uses the QLoRA/Unsloth path in train.py:
python train.pyThe training script is optimized for constrained local GPU training, with RTX 3080 10 GB as the stated target. It uses:
unsloth/deepseek-coder-7b-instruct-v1.5-bnb-4bit- LoRA rank 32
- 2048 token sequence length
- paged 8-bit optimizer
- local JSONL splits from
build/
The model template is defined in Modelfile. It frames PAX-Coder as a
proof-oriented kernel generator with these output families:
- Lean 4 theorem/proof text
- PTX or CUDA kernel text
- Futhark functional specification
- PAX proof-obligation mapping
Within this repository, "the model" means the public PAX-Coder package unless a document explicitly says otherwise. The internal Nemotron/Megatron frontier model line is not packaged here and is not required to inspect, train, or run the public PAX-Coder artifact.
Example Ollama packaging flow after a GGUF artifact exists:
ollama create pax-coder -f Modelfile
ollama run pax-coder "Write a verified GEMM kernel for Ampere sm_86."Generated output is not self-certifying. Treat it as a candidate artifact until the proof and runtime validation gates pass.
stateDiagram-v2
[*] --> SourceInventory
SourceInventory --> LeanConfig
LeanConfig --> LeanBlocked: lakefile or dependency error
LeanConfig --> LeanChecked: lake build passes
LeanChecked --> ProofBasisRecord
ProofBasisRecord --> ProofBasis: declared axiom basis recorded
ProofBasis --> ProofCandidate: proof obligations closed relative to basis
ProofCandidate --> CUDABuild
CUDABuild --> RuntimeBlocked: nvcc / ptxas / hardware missing
CUDABuild --> RuntimeChecked: kernel executes against reference
RuntimeChecked --> SealCandidate
SealCandidate --> Release: license and node-key policy satisfied
Minimum release evidence for a generated kernel:
- Prompt and constraints.
- Lean file path and
lake buildoutput. - Declared proof basis for the claimed theorem path.
- CUDA/PTX compiler command and output.
- Futhark or CPU reference comparison.
- Target GPU and architecture.
- License selection result.
- Node-key/seal record if production sealing is required.
This repository uses the tri-license structure in LICENSE.tri:
| Option | Intended role |
|---|---|
| BSL-1.1 | Source-available path with commercial restrictions until the change date |
| AGPL-3.0 | Strong network-copyleft path |
| MPL-2.0 | File-level copyleft path for modular integration |
| Commercial | Available for copyleft bypass and negotiated production terms |
The license file identifies the change date for the BSL path as 2028-08-08
and lists the copyright holder as:
Copyright (C) 2026 Ahmad Ali Parr
Bel Esprit D'Accord Irrevocable Trust
SnapKitty Collective Limited (FLP)
The Prolog license policy backend can be queried:
swipl -q -t halt -f backends/license_policy.pl -- select saas_wrapper
swipl -q -t halt -f backends/license_policy.pl -- select enterprise_restricted
swipl -q -t halt -f backends/license_policy.pl -- select file_level_mod
swipl -q -t halt -f backends/license_policy.pl -- select copyleft_bypassLicense selection is a compliance decision. The reasoner helps route common use cases, but it does not replace the actual license terms or a commercial agreement.
SOVEREIGN_NODE_KEY.md documents the operational
node-key and seal process. Read it as an operational release/sealing policy,
not as a substitute for LICENSE.tri.
Institutional distinction:
LICENSE.trigoverns source and use licensing paths.SOVEREIGN_NODE_KEY.mdgoverns production sealing, attribution, and operational participation.- A commercial deployment should satisfy both the selected license path and the applicable node-key/seal policy.
A Sovereign Node Key is proof that you have contributed to the PAX stack or received commercial authorization. It is not DRM; it is membership and production attribution. Running PAX-Coder in production requires one.
Option 1: Contribute to the Stack (Recommended)
- Fork the repository: SNAPKITTYWEST/pax-coder.
- Build something useful: a kernel, proof, integration, documentation update, test case, deployment adapter, or verification improvement.
- Submit a pull request.
- On merge, you earn a node key for that contribution.
- Email
license@collectivekitty.comwith:- your GitHub username,
- merged pull request link or links,
- intended use case: research, commercial, or personal.
- Receive your node key: Ed25519 public key registration plus signing certificate.
Option 2: Commercial License (Direct)
Email license@collectivekitty.com with:
- your organization name,
- intended deployment scope: internal R&D, SaaS, embedded product, or another production scope,
- GPU hardware: RTX 3080, RTX 4090, H100, or equivalent target,
- estimated kernel volume.
After review, approved commercial users receive a commercial node key, license terms, and registration path for deployment.
| Feature | Public Repository | Commercial Authorization |
|---|---|---|
| Clone and verify integrity | ✓ (anyone) | ✓ (included) |
| Generate kernels for testing | ✓ (anyone) | ✓ (included) |
| Deploy to production | ✗ (not authorized) | ✓ (with node key) |
| Sign releases | ✗ (not authorized) | ✓ (with node key) |
| Embed in products | ✗ (license required) | ✓ (commercial license) |
| Support | ✗ (not included) | ✓ (by tier) |
| SaaS or cloud deployment | Requires license | Included with commercial license |
- How to contribute: see
CONTRIBUTING.md. - Node key details: see
SOVEREIGN_NODE_KEY.md. - Licensing details: see
LICENSE.tri. - Commercial inquiries:
license@collectivekitty.com.
This project is suitable for:
- public demonstration and education around verified GPU kernel generation,
- internal research on verified GPU kernel generation,
- proof-carrying code experiments,
- CUDA/PTX training-data development,
- institutional verification workflows,
- commercial evaluation under the appropriate license path,
- and enterprise discussions around
pax-verifystyle verification services.
PAX-Coder is the public face of the program. Nemotron/Megatron is the internal frontier model line for commercial work and is intentionally not released as part of this repository.
Commercial teams should not treat generated kernels as approved artifacts until the verification pipeline has produced current evidence for the exact kernel, target GPU, compiler version, proof files, and deployment scope.
Before changing claims in this README or publishing a release, check:
- Does
lake buildpass? - Does the release state the declared axiom basis for the claimed theorem path?
- Does CUDA/PTX compile for the stated target architecture?
- Was runtime behavior compared against a functional reference?
- Are benchmark numbers tied to a reproducible command and hardware target?
- Does the license statement match
LICENSE.tri? - Does any production claim satisfy the node-key/seal policy?
- Are generated examples labeled as examples rather than audited proof certificates?
ABOUT.md: short overview.docs/USER_GUIDE.md: user workflow and prompt patterns.docs/PAX_ARCHITECTURE.md: axioms and proof obligations.MODEL_CARD.md: model-card draft.DATASET_CARD.md: dataset-card draft.PAX_CODER_README.md: commercial integration notes.PACKAGE.md: v1.0.0 package manifest.RELEASE_NOTES.md: v1.0.0 release notes.CHANGELOG.md: release history.SOVEREIGN_NODE_KEY.md: node-key policy.CONTRIBUTING.md: contribution guidance.
@software{pax_coder_2026,
title = {PAX-Coder: Institutional Program for Proof-Carrying GPU Kernel Generation},
author = {Parr, Ahmad Ali},
year = {2026},
url = {https://github.com/SNAPKITTYWEST/pax-coder}
}PAX-Coder should be evaluated by evidence:
claim -> file -> command -> output -> hardware/toolchain -> license path
If any link is missing, mark the claim as pending. That rule protects the institution, the engineering record, and downstream commercial users.