Verification

Verification is the point of Kyllo. The language is designed so that a program's requirements can be checked — and so that the checking is honest about what it did and did not establish. A successful compilation must never be presented as proof that a program is correct.

The four levels

L1 — Static Checks

Checks performed without running the program: syntax, types, and the checks below that can be decided from the source alone.

L2 — Contract Checks

Checking REQUIRES, ENSURES, and INVARIANT declarations against the code that must satisfy them.

L3 — Runtime Checks

Checks performed while the program runs, where a property cannot be established statically.

L4 — Formal Verification

Proof that a program satisfies its specification. This is the highest level — and the least settled. The proof language and proof engine are open (OQ-018), the supported proof obligations are open (OQ-019), and advanced formal verification is deferred in the MVP scope.

Eight kinds of check — and what each one establishes

Syntax checking

Parsing only: does the program match the grammar? A program that matches the grammar is not automatically valid. Syntax checking establishes nothing about meaning.

Semantic analysis

Does the program mean something coherent — are names declared, are declarations used consistently, do the pieces fit together? This is where a well-formed but meaningless program is caught.

Type checking

Strict and static, with no implicit conversions. A value of one type is never silently treated as another. Type checking establishes that the program's types line up — not that its logic is right.

Contract checking

Checking preconditions, postconditions, and invariants against implementations. Results are reported with a status: Proven, Checked, Unverified, or Failed. One honest caveat: the status vocabularies are not fully reconciled across the documentation — different sections use slightly different status words for the same ideas. The docs use PROVEN, TESTED, CHECKED, FAILED, and UNKNOWN in their verification-status system; this site uses the same words and always shows them as text, never by colour alone.

Static analysis

Analysis of the program without running it: effect and permission analysis, safety analysis, and checks for patterns the type system alone does not catch.

Runtime enforcement

Where a property cannot be proved statically, it is checked while the program runs — and a violation is a failure, reported as such, not silently tolerated.

Testing

Unit, integration, property, boundary, and regression tests are built into the language's workflow. But the docs are explicit: tests must never be represented as formal proofs, and passing tests must never be presented as proof of universal correctness. Tests show that tested inputs behaved as expected. Nothing more.

Formal proof

Proof that a program satisfies its specification, with respect to that specification — never proof in the abstract. Formal proof is level L4, and it is the least settled part of the design: the proof language, the proof engine, and which proof obligations are supported are all open questions.

The compiler workflow — a specified plan, not a built system

The documentation specifies a nine-stage compiler workflow. It has not been built. The stages, in order, are:

1. Lexical analysis
2. Parsing
3. Semantic analysis
4. Contract verification
5. Effect / permission analysis
6. Safety analysis
7. Intermediate representation (IR)
8. Code generation
9. Verification report

Three rules govern the workflow, and they are part of the design, not slogans:

• A failed mandatory check must prevent the program being accepted as a valid build.
• Unverified properties must remain explicitly identified and must never be reported as proven.
• A build must not be labelled VERIFIED merely because it compiled or passed its tests. What “verified” means is itself an open question (OQ-023).

What a verification report must record

Every verification report must record, for each property it speaks about:

• Property — what was supposed to hold.
• Method — how it was checked (static check, contract check, runtime check, test, proof).
• Result — passed, failed, or unverified.
• Assumptions — what the check had to assume.
• Limitations and unresolved conditions — what the check could not establish.

A report that omits any of these is not a verification report. It is a claim without evidence.

Illustrative verification report

Illustrative This is an example constructed for this website from the documentation. It is not compiler output — no compiler exists. It shows the shape a report must have, using the Bank Account deposit example from the Language page.

Property	Method	Result
Balance never goes negative	Contract invariant, static check	Passed
Deposit amount > 0	Contract precondition, checked	Passed for tested inputs
Withdrawal of 150 from a balance of 100 is rejected	Test	Passed
Decimal rounding behaviour	—	Unverified (OQ-002 open)
Formal proof of the deposit postcondition	—	Unverified (no proof engine; OQ-018 / OQ-019 open)

Assumptions: the deposit example is taken as written; the postcondition subject contradiction in the docs (see the Language page) is not resolved. Evidence source: illustrative example constructed for this website from the docs; not compiler output.

Failures, shown as failures

Verification that only ever passes is not verification. The checks below must fail — and the failure must be reported, not hidden:

• Withdraw 150 from a balance of 100 → Failure. The withdrawal is rejected; the balance is unchanged.
• Deposit −50 → Failure. The amount violates the precondition amount > 0; the deposit is rejected.

A language that cannot say “no” clearly cannot be trusted when it says “yes”.