Verification

Verification is the point of Kyllo. The language is designed so that a program's requirements can be checked — by the compiler, at runtime, and by tests — and every check reports what it established.

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. The proof language and proof engine are open (OQ-018), the supported proof obligations are open (OQ-019), and advanced formal verification is outside the MVP scope.

Eight kinds of check

Syntax checking

Parsing: does the program match the grammar? Syntax checking establishes that the program is well-formed; it says 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.

Contract checking

Checking preconditions, postconditions, and invariants against implementations. Results are reported with a status: PROVEN, TESTED, CHECKED, FAILED, or UNKNOWN, always shown as text.

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. Tests show that tested inputs behaved as expected.

Formal proof

Proof that a program satisfies its specification, with respect to that specification. The proof language, the proof engine, and which proof obligations are supported are open questions (OQ-018, OQ-019). Verification checks a program against its specification; a specification that is wrong, incomplete, or silent about a behaviour is outside what verification can catch.

The compiler workflow

The compiler works in nine stages, in order:

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:

• A failed mandatory check prevents the program from being accepted as a valid build.
• Unverified properties remain identified as unverified in the report.
• A build is labelled VERIFIED only for properties that were actually verified. The exact meaning of “verified” is an open question (OQ-023).

What a verification report records

Every verification report records, 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.

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. Evidence source: illustrative example constructed for this website from the docs; not compiler output.

Failures, shown as failures

The checks below fail — and the failure is 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.