# LLMLL: a language for agent-written code, with a Haskell compiler that emits liquid-fixpoint constraints directly

**URL:** <https://discourse.haskell.org/t/llmll-a-language-for-agent-written-code-with-a-haskell-compiler-that-emits-liquid-fixpoint-constraints-directly/14915>\
**Category:** Show and Tell\
**Tags:** llm-use\
**Created:** [October 30, 2026, 8:12pm UTC](https://discourse.haskell.org/t/llmll-a-language-for-agent-written-code-with-a-haskell-compiler-that-emits-liquid-fixpoint-constraints-directly/14915 "2026-10-30T20:12:14Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![machunter](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/machunter/32/5845_2.png) [@machunter](https://discourse.haskell.org/u/machunter)\
**Post date:** [October 30, 2026, 8:12pm UTC](https://discourse.haskell.org/t/llmll-a-language-for-agent-written-code-with-a-haskell-compiler-that-emits-liquid-fixpoint-constraints-directly/14915/1 "2026-10-30T20:12:14Z")

</div>

LLMLL is a language I’ve been building to experiment with AI (LLMs) writing code. A function starts as a contract with a typed hole for the body. The contract is a typed signature, optionally refined with predicates (`(where [x: int] (\> x 0))`), plus a precondition and a postcondition. When an agent attempts to fill the hole, the fill must type-check, and then the compiler checks it against the predicates and conditions with Z3 before the patch is integrated into the AST. A body the solver can’t prove is rejected, and the program is left as it was.

The idea is that multiple, potentially specialized, agents work in parallel to fill all the holes at once.

All of the code, the Haskell compiler included, was written by LLM agents. My role was that of a technical director.

The parts this forum might find interesting:

- **The compiler is Haskell** (GHC 9.6.6, Stackage lts-22.43), and so is its output: a checked program is emitted as Haskell and compiled by GHC.
- **It goes to liquid-fixpoint directly, not through Liquid Haskell.** The compiler walks its own typed AST and writes `.fq` constraint files for liquid-fixpoint 0.9.6.3.1, which hands them to Z3. Calls are checked assume-guarantee: a caller proves the callee’s precondition and assumes its postcondition.
- **The semantics are call-by-value, and the generated Haskell has to honour that.** Before v0.27.0 the generated code was lazy, and that could make a `verify` verdict describe a program that evaluated differently. Now the spec states the evaluation order, and generated Haskell that evaluates differently is treated as a codegen bug.

Scope, so nobody has to ask: the solver covers linear integer arithmetic, booleans, non-recursive sums, pairs, fixed-size bytes, maps and string literals. Outside that, a postcondition is assumed and the tool says so by name. A proof shows the body matches the contract, not that the contract is right.

A two-minute demo, using Apple’s goto-fail bug as the invariant (a scripted wrong body rejected, then a guarded one accepted): [LLMLL: a goto-fail body, rejected before the edit lands | LLMLL](https://machunter.github.io/llmll/demo.html)

You can try the rejection yourself: the demo page has a one-line Docker command.

Repo: [GitHub - machunter/llmll: A programming language and verification pipeline for experiments in which AI agents write code under formal contracts: agents fill typed holes, and an SMT solver proves each body before it merges. · GitHub](https://github.com/machunter/llmll)

Two questions I’d value opinions on from people who know this stack:

1. Emitting `.fq` directly rather than generating Liquid Haskell annotations gave me control over the constraint shape, but it means maintaining my own VC generator. Is there a reason I’ll regret not going through LH?

2. I’m pinned to liquid-fixpoint 0.9.6.3.1 on GHC 9.6. What’s the least painful way to keep up as Liquid Haskell and liquid-fixpoint move to newer GHCs?

---

<div class="post-metadata">

**Author:** ![Execute](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/execute/32/5828_2.png) [@Execute](https://discourse.haskell.org/u/Execute)\
**Post date:** [October 30, 2026, 8:22pm UTC](https://discourse.haskell.org/t/llmll-a-language-for-agent-written-code-with-a-haskell-compiler-that-emits-liquid-fixpoint-constraints-directly/14915/2 "2026-10-30T20:22:47Z")

</div>

LLMLL.. el-el-m-el-el.. this is so hard to say fast 😭

---

<div class="post-metadata">

**Author:** ![machunter](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/machunter/32/5845_2.png) [@machunter](https://discourse.haskell.org/u/machunter)\
**Post date:** [October 30, 2026, 8:32pm UTC](https://discourse.haskell.org/t/llmll-a-language-for-agent-written-code-with-a-haskell-compiler-that-emits-liquid-fixpoint-constraints-directly/14915/3 "2026-10-30T20:32:04Z")

</div>

lack of imagination 🙂