prometeu-studio/docs/general/specs/19. Verification and Safety Checks Specification.md

PBS Verification and Safety Checks Specification

Status: Draft v0 (Quality-Gate Baseline)
Applies to: test-backed safety gates for compiler stages and integration regression safety checks

1. Purpose

This document defines the minimum safety/verification quality gates that can be enforced now.

The intent is to keep safety measurable without over-specifying future verifier internals before backend and runtime integration stabilize.

2. Scope

This document defines:

• compiler-stage safety checks that must be covered by tests now,
• conditional integration safety regression checks for executable backends,
• and evidence requirements for safety-related support claims.

This document does not define:

• full verifier algorithm internals,
• full bytecode/runtime proof obligations,
• or one mandatory verifier implementation architecture.

3. Authority and Precedence

Normative precedence:

1. 2. Governance and Versioning.md
2. 12. Diagnostics Specification.md
3. 13. Lowering IRBackend Specification.md
4. 13. Conformance Test Specification.md
5. 15. Bytecode and PBX Mapping Specification.md
6. This document

If a rule here conflicts with higher-precedence authorities, it is invalid.

4. Normative Inputs

This document depends on:

• 12. Diagnostics Specification.md
• 13. Lowering IRBackend Specification.md
• 13. Conformance Test Specification.md
• 15. Bytecode and PBX Mapping Specification.md

5. Safety Gate Model

PBS currently uses two safety gate families.

5.1 Gate S-U: Compiler-Stage Safety Unit Tests (Required)

At minimum, test coverage must exist for:

1. deterministic rejection of malformed source input at lexer/parser level,
2. deterministic rejection of in-scope frontend semantic failures,
3. deterministic dependency/manifest validation failures,
4. stable diagnostics identity for required rejection surfaces (code, severity, primary attribution).

This gate is mandatory regardless of backend maturity.

5.2 Gate S-I: Integration Safety Regression With Runtime (Conditional)

For languages/backends that emit executable artifacts, integration safety regression tests must be introduced.

At minimum, these tests must cover:

1. deterministic rejection behavior for known malformed/unsupported integration scenarios in supported scope,
2. preservation of fixed safety regressions,
3. and repeatability across the declared runtime line for that backend.

When executable artifact emission is not yet present, Gate S-I is explicitly deferred.

6. Evidence Requirements

Safety claims must map to gate evidence:

• S-U evidence is required for baseline safety posture,
• S-I evidence is additionally required for integration-ready safety claims,
• and no published safety-related support claim should exist without current gate evidence.

7. Explicit Deferrals

The following are intentionally deferred:

• full verifier obligation catalog,
• formal proof of runtime safety properties,
• richer source-map/debug attribution standards beyond current minimum diagnostics needs.

8. Non-Goals

• Replacing runtime/bytecode authority.
• Freezing verifier architecture before implementation maturity.
• Defining performance tooling in a safety spec.

9. Exit Criteria

This document is in a healthy state when:

1. required compiler-stage safety checks are test-backed,
2. executable backends have explicit S-I status (pass/fail/deferred),
3. safety regressions are preserved in tests,
4. and safety-related support claims remain evidence-backed.