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.

Verification System¶

The language will use multiple levels of verification.

Level 1: Static Checks¶

Checks performed without running the program.

Examples: - Type mismatches - Missing required values - Invalid function arguments - Unhandled return types - Unused or invalid declarations

Level 2: Contract Checks¶

Checks that code satisfies explicitly declared requirements.

Examples: - A balance cannot become negative. - A transfer must deduct and deposit equal amounts. - A function must preserve specified conditions. - An operation must satisfy its declared postconditions.

Level 3: Runtime Checks¶

Checks performed while the program is running.

Examples: - Input validation - Array bounds - Resource availability - Runtime invariants - Unexpected external responses

Level 4: Formal Verification¶

Mathematical reasoning used to prove specific properties of a program.

Examples: - Proving that an operation cannot violate a defined invariant. - Proving that certain execution paths cannot occur. - Proving that a function satisfies its postconditions under its stated assumptions.

Verification Reporting¶

Every verification result must distinguish between:

VERIFIED: The specified property was successfully checked or proven.
FAILED: The property was checked and violated.
UNVERIFIED: The property could not be established.

The compiler must never report an unverified property as verified.

Source and authority¶

This page migrates VERIFICATION.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/.