Lean 4 formal contract layer for Structural Explainability.
This repository contains the machine-checked formal substrate that authorizes the operational contracts consumed by SE constitution, kernel, mapspec, and regime repositories.
It separates formal proof obligations from operational contribution workflows. Contributors to operational SE repositories consume exported contract artifacts; they do not need to edit Lean files or discharge proof obligations.
- Lean 4 definitions for core SE formal constraints
- Machine-checked theorem status for selected invariants
- Exported contract artifacts used by operational repositories
- Versioned proof-to-contract traceability
- Operational validators
- Domain mappings
- Applied datasets
- Regime execution pipelines
- Interpretation-specific semantics
SEFormalContract/
- Basic.lean foundational types and shared predicates only
- Regime.lean identity regime declarations and regime-level constraints
- Neutrality.lean neutrality assumptions, claims, and theorem stubs/results
- Relation.lean allowed relation primitives for operational mappings
- Export.lean contract-facing declarations intended to be exported
Use VS Code Menu:
View / Command Palette / Developer: Reload Window to refresh.
elan self update
lake update
lake build
lake exe export_contractShow command reference
Open a machine terminal where you want the project:
git clone https://github.com/structural-explainability/se-formal-contract
cd se-formal-contract
code .uv self update
uv python pin 3.15
uv sync --extra dev --extra docs --upgrade
uvx pre-commit install
git add -A
uvx pre-commit run --all-files
# repeat if changes were made
git add -A
uvx pre-commit run --all-files
# After running: lake exe export_contract, run:
uv run se-formal-contract validate
# do chores
uv run python -m pyright
uv run python -m pytest
uv run python -m zensical build
# save progress
git add -A
git commit -m "update"
git push -u origin main