Llmll: A goto-fail body, rejected before the edit lands

Burc Sahinoglu · 29 October 2026. A self-contained demonstration. The five-post series tells the longer story, up to 163 functions.

LLMLL is a programming language built for AI agents to write. A function starts as a contract, a precondition and a postcondition, with a typed hole where the body goes. An agent checks the hole out, proposes a body, and the compiler hands the body and the contract to an SMT solver. A body the solver cannot prove is rejected before it lands, and the program is left as it was.

This page runs that loop once, on the invariant behind a real bug, and shows every diagnostic it produces.

The two fills in the recording are scripted stand-ins for agents: fixed patch files committed to the repository, so the rejection is reproducible. Script: examples/gotofail/demo.sh.

In 2014, Apple’s goto-fail bug (CVE-2014-1266) reported a TLS handshake as successful on a path where the signature check never ran. The mistake was about whether a check executes. Written as a contract, the invariant is: return Verified only if the check passed.

(type Step (| Continue) (| Abort int)) (type Verdict (| Verified) (| Rejected int))

(def-shell finalize [sig: Step payload: int] -> Verdict (post (=> (= result Verified) (= sig Continue))) ;; return Verified => sig was Continue ?body)

?body is the hole. An agent asks for it with llmll checkout, which locks the hole and returns a brief: the postcondition, the return type, the names in scope and a lock token. The brief has no reference body and no hint.

{ "postcondition_goal": "(=> (= result Verified) (= sig Continue))", "expected_return_type": "Verdict" }

A wrong fill is rejected

Say the agent makes the goto-fail mistake and returns Verified on every path:

(match sig ((Continue) Verified) ((Abort c) Verified))

It submits the body as a JSON-Patch against the program’s JSON-AST, with --require-proof:

$ llmll patch finalize-hole.ast.json wrong.json --require-proof { "diagnostics": [ { "kind": "lh-unsafe", "message": "body verification of 'finalize' failed (else-branch does not satisfy postcondition) (constraint #1)", "pointer": "patch-op/1", "severity": "error" } ], "result": "PatchVerifyError" }

The patch is refused and the file is byte-for-byte unchanged. The diagnostic names the branch that fails: the else branch, the one that returns Verified when sig is Abort. That is the input the real bug shipped on.

(match sig ((Continue) Verified) ((Abort c) (Rejected c)))

$ llmll patch finalize-hole.ast.json right.json --require-proof {"result":"PatchSuccess","reuse_suggestions":[],"statements":3,"verification":[{"body_faithful":true,"fn":"finalize"}]}

$ llmll verify finalize-hole.ast.json body-faithful: finalize Running liquid-fixpoint ... ✅ finalize-hole.ast.json — SAFE (liquid-fixpoint)

body_faithful means the solver proved the postcondition from the body itself. It did not assume the contract.

This contract is a safety property. It forbids returning Verified when the check failed, and it does not require returning Verified when the check passed, so a body that always returns (Rejected 0) also verifies. Ruling that out takes a stronger contract, with <=> in place of =>. Post 2 runs both versions.

The rejection comes from the verifier, not from the type checker. llmll build checks types and emits Haskell, and it compiles the wrong body without complaint. The proof runs in llmll verify, and in llmll patch, which re-verifies the patched function before writing anything. With --require-proof, a patch is also refused when its function passes only because the solver fell back to assuming the postcondition.

Why a language for this, and not a verifier behind an agent tool. The verifier is not the new part: Dafny, Liquid Haskell or F* would reject the same body, and LLMLL’s proofs run on liquid-fixpoint and Z3. What LLMLL adds is the loop around the proof, built into the toolchain:

None of this needs a stronger solver. It lets you hand one function at a time to an agent and take back only bodies that verify, with the rest of the program untouched. How contracts compose across calls is Post 3.

With Docker and nothing else, see the rejection:

docker run --rm ghcr.io/machunter/llmll verify /opt/llmll/examples/gotofail/finalize-bad.llmll

It prints error: body verification of 'finalize' failed (else-branch does not satisfy postcondition). Swap finalize-bad for finalize to see the guarded body verify.

To run the whole checkout-and-patch loop from the recording, build llmll from the repository and run bash examples/gotofail/demo.sh. It needs liquid-fixpoint, z3 and jq on your PATH.

Two kinds of report are useful, and they show different things:

The series goes from this one function to 163: