Kyllo

Four principles

• Explicit requirements. What a program must do is written down in the program itself, not left in a comment, a chat message, or an assumption.
• Checkable behaviour. Requirements are expressed so they can be checked — by the compiler, at runtime, or by tests — rather than merely asserted.
• Accountable correctness claims. Every claim about a program says what was checked, how, and what remains unchecked.
• Model-independent verification standards. The same rules and the same verification apply no matter which AI system wrote the code — or whether a human did.

Why Kyllo exists

AI systems now write a large share of new software, and they make mistakes — confidently, quickly, and at scale. Human review does not keep up. Kyllo's answer is not to trust the model more, or to add another layer of review on top. It is to change the language itself, so that mistakes are harder to introduce and easier to detect: requirements are explicit, behaviour is defined, failures are explicit, and nothing is reported as verified unless it was actually checked.

Nobody gets a free pass. Not humans. Not AI. Not the compiler. A successful compilation must never be presented as proof that a program is correct.

Three ideas that make it different

1. Contracts are part of the program. Functions declare what they require, what they guarantee, what they change, and how they can fail — and those declarations are checked, not decorative.
2. Failure is a value, not an accident. Operations that can fail return a result that must be handled. Failures cannot be silently ignored.
3. Verification reports its limits. A verification report says what was checked, what passed, what failed, and what remains unverified — and it names its assumptions.

A real example, and a rejection

Example — Accepted OQ-001, statement termination

IF balance > 0:
    PRINT(balance);
ELSE:
    PRINT(0);
END IF;

Simple statements end with a semicolon. Compound structures end with a typed terminator that matches what opened them — END IF; closes an IF. This is the one design decision that has been formally accepted, in decision record OQ-001.

Rejected — Accepted OQ-001

END FUNCTION;;
;;;

A redundant semicolon after a block terminator, and empty statements, are rejected. The compiler must produce a diagnostic — it must not silently accept them.

More examples, with their status, are on the Language page. Proposed syntax there is labelled as proposed, not as settled.