Source status: no status is stated in the source document, so none is assigned here. Do not treat this page as a finalized specification. The normative rules are in the Technical Specification.

Program Validation and Verification¶

1. Compilation Status¶

A program can have one of three overall verification statuses:

• VALID: All mandatory language and compiler checks have passed.
• INVALID: One or more mandatory checks have failed.
• UNVERIFIED: The program passes mandatory structural checks, but one or more required behavioral properties cannot be established.

2. Individual Property Status¶

Every declared requirement must receive an individual status:

• PROVEN: Mechanically established through formal verification.
• TESTED: Passed specified tests, but not mathematically proven.
• CHECKED: Passed a static or runtime check.
• FAILED: A violation was detected.
• UNKNOWN: Available verification methods could not establish the result.

3. Verification Evidence¶

The compiler must record:

• The property being evaluated.
• The verification method used.
• The result.
• Any assumptions required.
• Any limitations or unresolved conditions.

4. Build Restrictions¶

• Failed mandatory checks prevent a valid build.
• Required but unverified properties must prevent a verified build.
• Tests must never be represented as formal proofs.
• AI-generated explanations must never substitute for actual verification evidence.
• Verification results must correspond to the exact source code being compiled.

Design Goal¶

The language must provide an honest, traceable account of what has been checked, what has been proven, and what remains uncertain.

Source and authority¶

This page migrates VALIDATION.md in full. It is an explanatory / implementation document, not the normative specification. Where it simplifies a rule, the Technical Specification governs. The original file is preserved in source-original/LANG/.