Skip to content

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

KYLLO's central idea: a program is checked against its intended behaviour, and anything that cannot be verified is identified as unverified.

  • Verification Model — four levels: static checks, contract checks, runtime checks, formal verification.
  • Validation — program statuses (VALID / INVALID / UNVERIFIED) and per-property statuses (PROVEN / TESTED / CHECKED / FAILED / UNKNOWN).
  • Verification Statuses — the status vocabulary in one place, with the rule that tests are never proofs.
  • Testing — unit, integration, property-based, boundary, and regression testing.
  • Evidence Reports — what a verification report must record.

Normative detail: Section 11: Testing, Section 55: Verification Report Format, Section 56: Conformance.