Section 55: Verification Report Format and Evidence Records¶

TECHSPEC-55 — Section 55 · Version 0.1 · Status: Initial Draft

Status: draft. This section is an Initial Draft (Section 57 is a Working Register). It describes intended or proposed behavior, not a finalized, implemented language rule. Do not treat examples here as normative.

1. Purpose¶

Verification reports communicate what the compiler, runtime, tests, and other verification tools actually established.

The report is a first-class build artifact. It must be machine-readable, stable, and understandable by both humans and AI agents.

2. Overall Build Status¶

The report uses the established status model:

DEVELOPMENT: Work in progress; no acceptance claim.
COMPILED: Parsing and required compilation stages completed.
VALIDATED: Required configured checks completed successfully.
VERIFIED: All explicitly required verification conditions have sufficient recorded evidence.
RELEASED: An identified artifact has been approved and released.

A build must not be labeled VERIFIED merely because it compiled or passed tests.

3. Property Statuses¶

Each property receives one of these statuses: - PROVEN: Established by a specified proof process under recorded assumptions. - TESTED: Passed one or more recorded tests. - CHECKED: Passed a specified static or runtime check. - FAILED: Evidence shows the property was violated. - UNKNOWN: No sufficient evidence is available.

These statuses must not be treated as interchangeable.

4. Evidence Record¶

Each evidence record should include: - Stable evidence identifier. - Property or requirement identifier. - Subject declaration or artifact. - Evidence status. - Method used. - Tool and version. - Inputs and assumptions. - Result. - Source and artifact hashes. - Timestamp where relevant. - Limitations and scope. - Links to diagnostics, tests, or proof artifacts.

5. Requirements Traceability¶

Requirements should have stable identifiers.

The report should map each requirement to: - Relevant declarations and code locations. - Applicable contracts. - Tests. - Static checks. - Proof obligations. - Current status. - Known gaps.

An unimplemented or unverified requirement must remain visible.

6. Failure Reporting¶

Failures must include: - Stable diagnostic identifier. - Severity and category. - Source location or artifact reference. - Expected property. - Observed result. - Reproduction information where available. - Whether execution or external effects may already have occurred.

7. Evidence Freshness¶

Evidence is tied to exact source, dependency, compiler, verifier, configuration, and artifact identities as applicable.

Changes to relevant inputs invalidate or require re-evaluation of affected evidence.

The compiler must not reuse stale evidence as if it applied to changed code.

8. Machine-Readable Format¶

The initial report format should be versioned JSON with a formal schema.

The schema must define required fields, optional fields, enumerations, compatibility behavior, and how unknown fields are handled.

A human-readable summary may be generated from the same underlying report.

9. Report Integrity¶

Reports should be associated with the exact build artifact and protected against accidental or unauthorized modification.

A report signature can establish report origin and integrity. It does not make the reported claims true unless the evidence itself is sound.

10. Design Goal¶

The report must answer a precise question: what was checked, by which method, against which exact artifact, with what result, under which assumptions, and what remains unknown?

Source file: TECHSPEC-55.md (preserved in source-original/LANG/). See the specification index, the glossary, and the cross-reference index.