About this page: this page is editorial guidance written for this documentation site. It summarises and links to source material; it defines no language rules. The normative rules are in the Technical Specification.
Verification Statuses¶
The status vocabulary is defined in Program Validation and Verification and Section 55. Statuses are always shown as text, never by colour alone.
Overall program status¶
| Status | Meaning |
|---|---|
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. |
Individual property status¶
| Status | Meaning |
|---|---|
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. |
Rules¶
- Failed mandatory checks prevent a valid build; required but unverified properties 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.
- The compiler must never report an unverified property as verified.
Open decision
The exact meaning and release requirements for VERIFIED are themselves an
open decision — OQ-023 in
Section 57.