Public assurance / source-bound evidence

See what RPOS machine-checks — and what it does not.

This view connects concrete operational risks to bounded Lean 4 theorems and executable Python tests. Lean evidence is an assurance layer, never runtime authority.

Lean buildLoading…

Assurance assertions—

Toolchain—

Source commit—

Evidence crosswalk

Risk → theorem → runtime evidence

Every row is validated against the source tree when the manifest is built.

Proof ceiling

Machine-checked does not mean universally proven.

Loading proof boundary…