Lean-based runtime kernels engineered for reliability, auditability, and deterministic validation.
The project focuses on safety-critical runtime behavior across policy, concurrency, and shape handling, with strict documentation-to-gate alignment.
Runtime systems fail in production when guarantees are implicit, tests are brittle, or builds are environment-sensitive.
This repository hardens that path by making reliability properties explicit and mechanically checkable.
- Canonical contracts: shared runtime-critical aliases live in
src/RuntimeSafetyKernels/Contracts.lean. - Proof-hole enforcement: safety-critical modules must stay free of
sorry, enforced bypython scripts/check_proof_completeness.py. - Contract consistency: extraction paths are checked by
python scripts/check_contract_consistency.py. - Resilient execution: validation runs with diagnostics, retry/backoff, and fallback runtime checks for unstable environments.
Run the full local reliability pipeline:
python scripts/validate_local.pyThis command orchestrates diagnostics, gate checks, build, and runtime verification through a primary path plus fallback path where needed.
| Tool | Purpose | Output/Behavior |
|---|---|---|
scripts/lake_doctor.py |
Collect environment, toolchain, and network diagnostics | Writes build/lake-diagnostics.json |
scripts/lake_resilient.py |
Execute lake commands with retry/backoff and timeout |
Improves reliability under flaky fetch/toolchain states |
scripts/run_runtime_checks.py |
Run tests, fuzz, benchmarks | Uses Windows-safe fallback from lake exe to lake env lean --run when native linking fails |
scripts/validate_local.py |
Orchestrate full local validation | Runs primary sequence, then fallback sequence on failure |
- Main module:
src/RuntimeSafetyKernels.lean - Tests:
src/RuntimeSafetyKernels/Tests.lean - Fuzz checks:
src/RuntimeSafetyKernels/Fuzz.lean - Benchmarks:
src/RuntimeSafetyKernels/Benchmarks.lean - Canonical contracts:
src/RuntimeSafetyKernels/Contracts.lean
Fallback Lean runners used by runtime checks:
src/RuntimeSafetyKernels/Runner/TestsMain.leansrc/RuntimeSafetyKernels/Runner/FuzzMain.leansrc/RuntimeSafetyKernels/Runner/BenchmarksMain.lean
- API surface:
docs/api.md - Contribution standards:
CONTRIBUTING.md
All changes are expected to preserve reliability guarantees, provide verification evidence, and keep documentation aligned with implementation reality.