Metadata-Version: 2.4
Name: responsibility-pathway-os
Version: 0.1.0a2
Summary: Executable Responsibility Pathway OS in Python with Lean 4 machine-checked responsibility invariants
Author: Akihisa Ono
License-Expression: MIT
Project-URL: Homepage, https://github.com/YutoriKomeiji/responsibility-pathway-os
Project-URL: Repository, https://github.com/YutoriKomeiji/responsibility-pathway-os
Project-URL: Issues, https://github.com/YutoriKomeiji/responsibility-pathway-os/issues
Classifier: Development Status :: 3 - Alpha
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Requires-Python: >=3.11
Description-Content-Type: text/markdown
License-File: LICENSE
Dynamic: license-file

<!-- RPOS-DOC-ID: RPOS-PUBLIC-README-001 -->
<!-- RPOS-DOC-LANG: en -->
<!-- RPOS-DOC-VERSION: 0.1.0a2 -->
<!-- RPOS-DOC-STATUS: public-alpha-release-candidate -->
<!-- RPOS-DOC-COUNTERPART: README.ja.md -->

# RPOS — Responsibility Pathway Operating System

**Executable responsibility pathways in Python, with critical responsibility invariants machine-checked in Lean 4.**

RPOS is an independently engineered, open-source Responsibility Pathway OS for consequential AI and automation workflows. It combines a Python/SQLite executable runtime with a Lean 4 Formal Assurance Surface for selected invariants covering Human Gate, operational authority, dispatch, external-effect verification, uncertainty, recovery, resumption, and completion.

RPOS is not a model wrapper, a policy document, or a logging layer. It keeps responsibility-bearing state executable across:

`proposal -> Human Gate -> authorization -> dispatch -> effect verification -> uncertainty -> repair -> explicit resumption -> completion`

Its core rule is simple: **authorization is not execution, an execution receipt is not proof of external effect, and failure or uncertainty must not erase responsibility.**

## What is implemented now

The public alpha includes:

- a Python/SQLite operational state machine with durable responsibility state;
- explicit Human Gate and operational-authority boundaries;
- bounded dispatch attempts, restart/reconciliation, repair/resume, and Human Return;
- external-effect separation so a successful transport receipt does not silently become completion;
- CLI and executable evaluation scenarios;
- Responsibility State Envelope templates with `authority_effect: "none"`;
- reproducible public-export, SBOM, and release-evidence generation;
- Windows/Python field-portability checks; and
- a reproducible Lean 4 project machine-checking selected responsibility invariants.

## Python × Lean 4 — executable responsibility with machine-checked invariants

RPOS exposes a public theorem-to-runtime-test crosswalk in `formal/assurance-catalog.json`:

`operational risk -> Lean theorem -> Python runtime test -> model scope -> proof ceiling`

Current machine-checked assertions include:

1. `RPOS.human_gate_cannot_dispatch_directly` — a Human Gate is not direct dispatch authority;
2. `RPOS.only_verified_enters_completed` — only `VERIFIED` may directly enter `COMPLETED`;
3. `RPOS.effect_unknown_is_not_completed` — unresolved external-effect uncertainty is not completion;
4. `RPOS.ready_to_resume_is_not_authorized` — repair readiness is not execution authority;
5. `RPOS.receipt_is_not_effect_verification` — a transport/API receipt is not external-effect verification;
6. `RPOS.model_proposal_is_not_authority` — a model proposal is not operational authority.

These are real Lean 4 theorems over declared bounded models. They do **not** imply that the entire Python runtime, deployment environment, legal responsibility, organizational authority, or arbitrary external system is formally proven.

That boundary is deliberate: formal proof, executable implementation evidence, and real external-effect evidence are different evidence classes and must not impersonate one another.

## Independent Responsibility Pathway lineage

RPOS is independently engineered within the Responsibility Pathway lineage:

```text
Responsibility Pathway Model / Paper
  -> Responsibility Pathway Design
  -> Responsibility Pathway Engineering
  -> Responsibility Pathway Runtime
  -> RPOS — Responsibility Pathway Operating System
  -> formal + executable + operational evidence
  -> upstream revision
```

The lineage centers on responsibility continuity across judgment, authorization, execution, uncertainty, repair, return, resumption, and residual ownership. RPOS is the operating layer: **RPOS owns operation, not intelligence.** Models remain replaceable proposal sources; they do not become authority merely by proposing an action.

## Public Alpha status

Version: **0.1.0a2 — Early Public Alpha / Executable Preview**

`responsibility-pathway-os==0.1.0a2` is the current release candidate. The previous `0.1.0a1` alpha is publicly available on PyPI; `0.1.0a2` will be published only after its exact source commit passes the declared release route.

Python 3.11+ is required.

```bash
python -m pip install responsibility-pathway-os==0.1.0a2
rpos --db rpos.db boot
```

The installation command above becomes valid when `0.1.0a2` is published to PyPI. Until then, use a source checkout for evaluation.

```bash
python -m pip install -e .
python examples/quick_start_end_to_end.py
```

This alpha is intended for engineering evaluation and bounded pilots, not unattended production operation.

## Why RPOS exists

Agent systems can receive a successful tool/API receipt while the real-world effect is absent, partial, duplicated, ambiguous, or unverifiable. They can also lose the human decision boundary during retry or recovery.

RPOS keeps those cases explicit:

- `AUTHORIZED` does not mean execution has started or succeeded.
- `DISPATCHING` preserves an issued but unresolved attempt.
- `EFFECT_UNKNOWN` preserves uncertainty instead of reporting false success.
- `REPAIR_REQUIRED` makes recovery responsibility explicit.
- `READY_TO_RESUME` means repair readiness, not permission to execute.
- explicit resumption restores authority before a fresh dispatch attempt.
- `COMPLETED` follows bounded verification, not merely a transport receipt.

## Core responsibility states

`PROPOSED`, `HUMAN_GATE`, `AUTHORIZED`, `DISPATCHING`, `EFFECT_UNKNOWN`, `VERIFIED`, `REPAIR_REQUIRED`, `READY_TO_RESUME`, `COMPLETED`, `DENIED`, `ABORTED`.

## Executable examples

The repository includes eight executable scenarios:

```bash
python examples/happy_path_verified.py
python examples/human_gate_denied.py
python examples/effect_unknown_restart_reconcile.py
python examples/quick_start_end_to_end.py
python examples/idempotency_replay_guard.py
python examples/human_return_reauthorization.py
python examples/adapter_exception_containment.py
python examples/reconciliation_unresolved_human_return.py
```

They exercise bounded paths for approval/denial, `EFFECT_UNKNOWN`, restart, reconciliation, repair, explicit resume authority, replay protection, adapter exceptions, and Human Return. They are executable evidence for those scenarios only.

## Lean 4 Formal Assurance Surface

The formal project is pinned to **Lean 4.32.2**.

```bash
cd formal/lean
lake build
```

Current modules include:

- `RPOSState.lean` — state transitions, Human Gate, completion, uncertainty, resume authority;
- `RPOSReachability.lean` — bounded multi-step reachability and no-direct-shortcut properties;
- `RPOSEvidenceBoundary.lean` — separation among authorization, receipt, verification, evaluation, and dependency evidence;
- `RPOSPacketBoundary.lean` — no-authority-effect properties for responsibility envelopes;
- `RPOSOperationalBoundary.lean` — model proposal, human authorization, receipt, external observation, and operational responsibility;
- `RPOSTransparencyBoundary.lean` — transparency/evidence distinctions.

The public Formal Assurance Viewer is generated from the exact site commit after the Lean project is machine-checked and maps operational risks to theorem names, Python runtime tests, source identity, model scope, and proof ceiling.

## Responsibility State Envelope

`templates/catalog.json` contains reusable neutral-role templates for operation proposal, Human Gate decision, verification contract, repair plan, resume authorization, dependency evidence, external evaluation evidence, and Human Return.

Every envelope has `authority_effect: "none"`: **creating or validating an envelope never authorizes, dispatches, verifies, completes, or resumes an operation.**

## Verification route

The release route includes:

- the complete Python test suite;
- all eight source examples;
- wheel and sdist build and clean-install checks;
- installed CLI/API checks outside the repository working directory;
- exact-HEAD public-export reconstruction;
- source-bound CycloneDX SBOM and SHA-256 release evidence;
- public-source likely-secret scanning;
- Windows and Ubuntu checks on Python 3.11 and 3.12;
- pinned Lean 4 `lake build`;
- exact-head Formal Assurance manifest generation; and
- GitHub Pages validation and deployment with machine-checked assurance and verified architecture visuals.

Passing those checks establishes the named engineering evidence within their declared scope. It does not automatically establish production readiness, legal compliance, universal safety, organizational authority, arbitrary external-system correctness, or implementation-wide formal correctness.

## Claim boundary and promotion

RPOS separates two different things:

- **Current Evidence Boundaries** — claims that may advance when declared evidence is obtained and reviewed;
- **Permanent Responsibility Boundaries** — authority or responsibility that software should not create by itself.

Evidence-limited claims currently include production readiness, broader platform support, implementation-wide formal conformance, stronger software-supply-chain trust, and domain effectiveness beyond the published scenarios.

Permanent boundaries include legal/regulatory authority, correctness of arbitrary external systems, receipt-as-effect proof without a verification contract, transfer of final organizational responsibility to software, and universal exactly-once guarantees for arbitrary systems lacking the required contract.

See `docs/en/claim-boundary-promotion.md`.

## Direction

The long-term goal is larger than the current alpha: make responsibility-bearing operational state easier to execute, inspect, test, formally reason about, recover, and return to accountable humans or institutions across real AI-enabled workflows.

That is a goal, not a claim of completion. Each stronger public claim must earn its promotion through implementation, evidence, and review.

## Project surfaces

- GitHub Pages product site and architecture maps
- `site/assurance.html` — Formal Assurance Viewer
- `formal/assurance-catalog.json` — canonical theorem/runtime-test crosswalk
- `product-status.json` — machine-readable release and claim state
- `docs/en/public-alpha-evaluation-guide.md` — third-party evaluation route
- `CHANGELOG.md` — release history
- `SECURITY.md`, `SUPPORT.md`, `CONTRIBUTING.md`

## License

MIT License.
