RPOS Formal Assurance Evidence Flow

RPOS Formal Assurance Evidence Flow A data-flow diagram generated by Archify. 01 / Exact source 02 / Independent checks 03 / Source-bound evidence 04 / Public assurance 05 / Operational authority RPOS Source Commit · exact Git SHA · 01 / Exact source · source of truth RPOS Source Commit exact Git SHA source of truth Lean 4 Model · structural invariants · 02 / Independent checks · formal Lean 4 Model structural invariants formal Runtime Tests · implementation evidence · 02 / Independent checks · runtime Runtime Tests implementation evidence runtime Pinned lake build · checked theorems · 03 / Source-bound evidence · Lean Pinned lake build checked theorems Lean Assurance Manifest · theorem + tests + hashes · 03 / Source-bound evidence · exact-head manifest Assurance Manifest theorem + tests + hashes exact-head manifest Assurance Viewer · user-visible crosswalk · 04 / Public assurance · public assurance Assurance Viewer user-visible crosswalk public assurance Human Authority · decision owner · 05 / Operational authority · separate authority Human Authority decision owner separate authority formal model sources exact commit runtime implementation + tests exact commit lake build machine check machine_checked=true bounded theorem evidence test crosswalk + source hashes runtime evidence source_commit + catalog hashes provenance public assurance data read-only review context only no authority effect Legend primary data async batch data store data flow

Two Evidence Streams

  • • Lean machine checking and Python runtime tests are related but distinct
  • • The manifest cross-links them without claiming implementation-wide formal equivalence
  • • Every release binds the evidence to an exact source commit

Proof Ceiling

  • • Formal claims are limited to the modeled structural invariants
  • • The manifest states what each theorem does not prove
  • • External-effect truth still requires operational evidence

No Authority Transfer

  • • The viewer is public assurance, not a runtime control plane
  • • Passing Lean theorems cannot approve a Human Gate
  • • Human Authority remains the operational decision owner