An experiment in letting AI write the code: the compiler proves each function against its contract, and refutes a type-correct but wrong body before it merges.
LLMLL (Large Language Model Logical Language) is a programming language and verification pipeline built for experiments in which AI agents write code under formal contracts. Its primary author is an LLM agent, not a human: contracts state what a function must do, agents fill typed holes, and the compiler proves each body against its contract with Z3 before the patch is applied. Agents coordinate through those contracts, not through conversation. An agent can hallucinate an implementation and that's fine, as long as it satisfies the contract: verification turns hallucination from a failure mode into a search strategy (generate a candidate, check it against the spec, accept or reject).
Current version: see
CHANGELOG.md § Latest. Full release notes per version live in CHANGELOG; this README does not duplicate them.
Learn more:
docs/README.mdis the reading guide to the documentation ·ROADMAP.mdsays what has shipped and what is next ·experiments/README.mdindexes the experiments and their results.
conserve(from, to, amount) returns both post-transfer balances, and its contract ties them together: (first result) + (second result) = from + to: the total is conserved, full stop. A deliberately wrong body that credits the destination one unit extra is type-correct and looks harmless on inspection, but it breaks conservation, and the SMT solver refutes it:
# body: (pair (- from amount) (+ to (+ amount 1))) ← type-correct, creates money
$ llmll verify conserve-bad.llmll
error: body verification of 'conserve-bad' failed —
implementation does not satisfy postcondition (constraint #0)
# body: (pair (- from amount) (+ to amount)) ← correct, conserves the sum
$ llmll verify conserve.llmll
✅ conserve.llmll — SAFE (liquid-fixpoint)
The proof is over both return values at once: a relational invariant, not a bound on one number. The wrong body above is scripted to show the check firing; no agent produced it. Dafny, Liquid Haskell or F* would refute it too; what LLMLL adds is the loop around the proof, below.
The wrong body in this recording is scripted to show the check firing; no agent produced it. Regenerate with make demo-gifs. If an animation on this page shows a still frame, your browser or GitHub's Accessibility setting for animated images may be pausing it; click the image to open the GIF directly.
Full copy-pasteable walkthrough: payments-core/DEMO-RUNBOOK.md — the composed transfer/debit call-chain beat and the single-constructor settle beat live there too. For the interactive repair-loop protocol — an agent checks out a typed ?hole, submits a patch, and the compiler rejects or accepts it before anything merges — see withdraw-demo/DEMO-RUNBOOK.md (narrated: DemoPost.md).
Those tools prove the same kind of property, and LLMLL's proof path (liquid-fixpoint over Z3) is the one Liquid Haskell uses. LLMLL does not claim a stronger verifier. It builds the loop around the verifier for the case where an agent writes the code:
- A hole is a contract. llmll checkoutgives an agent a typed?holewith its precondition, the postcondition it must meet and the names in scope, and not the answer.llmll patchapplies the fill only if the program still type-checks and the solver does not refute it.
- Weak contracts are flagged. --weakness-checkreports a contract so weak that a trivial body satisfies it;--cdpscores how sharply a contract rules out wrong bodies.
- Every function carries a trust level. The trust report marks each function verified,assertedand so on, and averifiedclaim never silently rests on an unproven callee.
- Agents edit structure, not text. Every program also has a JSON-AST form, and patches are RFC 6902 JSON-Patch against it, so there are no text merge conflicts.
- Decomposition is checked. llmll refinefills a hole and spawns contracted sub-holes in one step, and rejects a sub-contract that no body can meet or that says nothing.
What the experiments show. In experiments/minimal-agent/, three frontier models wrote verified-correct bodies 30 of 30 times on fixtures built to trip them, with 0 wrong fills in 54 attempts. The evidence is for assurance: agent-written code, proved against a contract the agent did not write. The refutation demos in this README and on the blog use scripted wrong versions to show that the check works; the agents in these experiments did not produce them. Every experiment, with its result: experiments/README.md.
Not every property is decidable by SMT. square(n) = n*n claims result ≥ 0 — but n*n is nonlinear, outside the linear-arithmetic fragment LLMLL sends to the solver, so the SMT verifier can only mark the postcondition asserted (an explicit "not proven"). With --leanstral, LLMLL states the obligation as a Lean theorem, has Leanstral prove it, and checks that proof with the Lean kernel + Mathlib — recording a verified-lean tier with an independently re-checkable .lean certificate.
Experimental. Recorded live on v0.26.3 against the Leanstral API; regenerate with examples/leanstral-demo/demo.sh (needs an API key and a Lean 4 + Mathlib project).
$ llmll verify examples/leanstral-demo/square.llmll --trust-report
square: post: asserted # nonlinear: outside the SMT fragment, not proven
$ LLMLL_LEANSTRAL_API_KEY=… llmll verify examples/leanstral-demo/square.llmll \
--leanstral --leanstral-lean-project ~/proofcheck --trust-report
square: Leanstral proof found, Lean kernel + Mathlib CHECKED
square: post: verified-lean (certificate: square.verified.lean)
The certificate is a Lean proof term the kernel accepted, checkable by anyone with Lean without trusting Leanstral. What you still trust is LLMLL's translation of the contract into the Lean theorem statement. An AI proved what the SMT solver couldn't, and you don't have to take its word for it.
Experimental. Opt-in demo; needs a Leanstral API key (
LLMLL_LEANSTRAL_API_KEY) and a local Lean 4 + Mathlib project. Production Lean verification across all obligation classes is the deferredLEAN-GArebuild. Reproduce:examples/leanstral-demo/(demo.sh) · design:docs/archive/shipped-design-specs/leanstral-demo-spec.md.
The full repair loop (hole → rejected bad fills → accepted fix → verified) is the copy-pasteable DEMO-RUNBOOK.md.
The two fills are scripted stand-ins for agents: fixed patch files committed to the repo, not produced by an agent run. Script: examples/withdraw-demo/demo.sh.
Zero-install (Docker). No Haskell toolchain — the image bundles llmll, z3, and liquid-fixpoint:
# see the SMT refutation of a conservation-breaking fill (no local files needed):
docker run --rm ghcr.io/machunter/llmll verify /opt/llmll/examples/payments-core/conserve-bad.llmll
# verify your own file (mounts the current directory at /work):
docker run --rm -v "$PWD":/work ghcr.io/machunter/llmll verify myfile.llmllFrom source. Build first:
cd compiler && stack build
stack exec llmll -- --helpRequires GHC ≥ 9.4 + Stack ≥ 2.9. The proof step also needs z3 + liquid-fixpoint.
Nothing passes without the solver. On the from-source path, with
z3/liquid-fixpointabsent,verifyprints aSOLVER NOT FOUND -- NOTHING WAS PROVENbanner and exits3, andpatch/refinerefuse to apply a contracted patch (PatchVerifyUnavailable, exit3). Install both to see the refutation. (The Docker image bundles both, so it never hits this.) Seedocs/getting-started.md.
LLMLL treats verification as the coordination protocol. A lead agent defines types and contracts (the what); specialist agents fill typed holes with the how; the compiler verifies each fill against its contract before merging. Agents trust each other's contracts, not each other's code. Merges are structured JSON-AST patches, not text diffs — so there are no structural merge conflicts, and every patch is re-verified before it lands.
It does not claim program correctness. It guarantees that all code is consistent with its declared specifications, and it tracks how strong each guarantee is: a verified contract was proven by the SMT solver; an asserted one was not. Trust propagates — no verified claim silently rests on an unproven dependency. The weakness checker (--weakness-check) even flags a contract so weak that a trivial implementation satisfies it. Its discriminative-power sibling (--cdp) scores how sharply a contract rules out wrong bodies. Both checks measure non-vacuity, not spec fidelity: a contract that is discriminative yet captures the wrong behavior still passes, and the code still verifies against it.
The shipped proof path is SMT (Z3 via liquid-fixpoint) over a non-recursive QF-LIA core — integer linear arithmetic, let-bindings, conditionals, calls to contracted functions (assume-guarantee), and n-arm matches on admissible (non-recursive) sums (Result and user ADTs, nested and sequential) — extended with three decidable theories: the array class (bytes[n] memory safety, and map[{int,string},{int,bool,string}] get-after-put / key-presence / construction / read-modify-write), admissible datatype construction, and string literals (equality, distinctness, and code-point length). That covers numeric bounds, conservation invariants, length preservation, array/map bounds-and-presence safety, and string-tag discrimination. Everything else — string structure (concatenation, substring, regex), recursive-payload ADTs, non-linear arithmetic (* / mod), IO — falls back to contract-only checking, property tests, or runtime assertions, each carrying an explicit trust label (full matrix in LLMLL.md §5.3.5). Recursion is inside the fragment: with a (decreases e) measure the solver discharges, the proof is total; without one, it holds only if the recursion terminates, and the verify headline drops the ✅ and names the function.
Nonlinear obligations have an experimental Lean 4 path: the opt-in --leanstral flag shown above, which needs a Leanstral API key and a local Lean 4 + Mathlib project. Production Lean verification across all obligation classes is deferred. --leanstral-mock runs the same pipeline against a mock prover, for testing.
docs/one-pager.md carries the full Claim-to-Evidence map — every claim mapped to a shipped command or an explicit "Planned"/"Not shipped" label. The "Planned"/"Not shipped" labels are deliberate; read it before sharing.
Six of this repository's CI gates are LLMLL programs, in tools/: version-gate (version banners and schema versions agree), doc-archive (each archived design document sits where its status says), doc-claims (what the docs say the compiler rejects, checked against the compiler), doc-path-lint (path citations in prose; advisory), refute-crux (96 frozen verify verdicts, so a lost refutation fails CI) and build-smoke (builds and runs the other five gates end to end). The CI workflow builds and runs them on every push to main and every pull request against it. In the same run, each gate's decision core (adjudicate.llmll) must pass llmll verify, and a deliberately broken copy of that core (crux-*.llmll) must be refuted, or the run fails. Only the decision core is proved; the file and process handling around it is built and run, not proved.
The largest LLMLL program in the tree is not a CI gate. tools/llmll-driver/ is the RFC-SWARM pipeline driver: 8522 lines across 39 modules, with 55 proved functions and 581 effectful def-shell functions that carry no proof by construction (docs/design/driver-ll-campaign-close.md). Its README separates what is proved from what is only asserted.
The active compiler is a Haskell stack project in compiler/. It is the only supported backend.
Both source formats compile to identical AST nodes:
The JSON-AST schema is at docs/llmll-ast.schema.json.
Requires GHC ≥ 9.4 + Stack ≥ 2.9.
cd compiler
stack build
stack exec llmll -- --help→ Full build guide and known-good patterns: docs/getting-started.md
cd compiler
# Check the example
stack exec llmll -- check ../examples/hangman_sexp/hangman.llmll
# Build a Haskell package in generated/hangman_sexp
stack exec llmll -- build ../examples/hangman_sexp/hangman.llmll -o ../generated/hangman_sexp
# Build from JSON-AST
stack exec llmll -- build ../examples/hangman_json/hangman.ast.json -o ../generated/hangman_json
# Run the generated game
cd ../generated/hangman_json && stack build && stack exec hangmanLLMLL provides body-faithful SMT verification for a non-recursive QF-LIA core with compositional call-chain reasoning: integer and bool values, linear arithmetic and comparisons, let-bindings, conditionals, calls to contracted functions (assume-guarantee, same-file or imported), n-arm matches on non-recursive sums, pairs, non-recursive datatype construction, the array class (bytes[n] and map operations) and string literals. Programs outside that fragment fall back to contract-only verification, property-based testing, or runtime assertions, each with an explicit trust label.
Full verification matrix: LLMLL.md §5.3.5.
Start here: examples/README.md is the tiered index to every example.
LLMLL.md ← canonical language specification
CHANGELOG.md ← release notes
compiler/ ← Haskell compiler (stack project)
src/LLMLL/
Parser.hs ← S-expression parser (Megaparsec)
Lexer.hs ← Megaparsec lexer (tokens, whitespace, layout)
ParserJSON.hs ← JSON-AST parser
Syntax.hs ← AST types (incl. ModulePath, ModuleEnv, ModuleCache, TPair)
TypeCheck.hs ← Bidirectional type checker
HoleAnalysis.hs ← Hole collector (?hole expressions)
CodegenHs.hs ← Haskell code emitter
AstEmit.hs ← JSON-AST emitter (--emit round-trip)
Contracts.hs ← Runtime contract assertion generator
PBT.hs ← QuickCheck property runner
Diagnostic.hs ← Structured error/warning types
Module.hs ← Multi-file module resolver, cycle detection, ModuleCache
Hub.hs ← llmll-hub local package cache (tarball install) and scaffold
Sketch.hs ← Partial-program type inference (--sketch)
Serve.hs ← HTTP endpoint for agent swarms (llmll serve)
FixpointIR.hs ← .fq constraint IR + text emitter
FixpointEmit.hs ← typed AST → .fq + ConstraintTable builder
DiagnosticFQ.hs ← liquid-fixpoint output → [Diagnostic] with JSON Pointers
Replay.hs ← JSONL event log parser + replay execution
LeanTranslate.hs ← LLMLL contracts → Lean 4 theorem obligations
MCPClient.hs ← Leanstral client (Mistral API over HTTPS; mock-first)
ProofCache.hs ← per-file .proof-cache.json sidecar (SHA-256)
TrustReport.hs ← transitive trust closure analysis (--trust-report)
VerifiedCache.hs ← .verified.json sidecar read/write
WeaknessCheck.hs ← trivial-body spec weakness detection
InvariantRegistry.hs ← pattern-based invariant suggestion database
ObligationMining.hs ← downstream postcondition strengthening suggestions
ObligationAssembly.hs ← structured obligation report assembly + JSON encoding
GuardClassifier.hs ← shared guard classification (verifier + obligations)
SpecCoverage.hs ← specification coverage metric + governance guardrails
JsonPointer.hs ← RFC 6901 pointer resolution + descendant hole search
Checkout.hs ← Hole checkout with per-file lock management (llmll checkout)
PatchApply.hs ← RFC 6902 JSON-Patch application with scope validation + re-verification (llmll patch)
AgentSpec.hs ← Compiler-emitted agent spec for LLM system prompts (llmll spec)
HubQuery.hs ← Query-by-signature: find hub modules matching a type signature (llmll hub query)
CDP.hs ← contract discriminative power evidence axis (--cdp)
ProofArtifact.hs ← unified, replayable verification record (--proof-artifact / replay-artifact)
package.yaml / stack.yaml
examples/
hangman_sexp/ ← Full Hangman (S-expression)
hangman_json/ ← Full Hangman (JSON-AST); getting-started.md's worked example
tictactoe_sexp/ ← Tic-Tac-Toe (S-expression)
life_sexp/ ← Conway's Life (S-expression, multi-module)
life_json/ ← Conway's Life (JSON-AST, multi-module)
withdraw.llmll ← Contract demo
hangman_json_verifier/ ← Hangman with contracts (asserted, not solver-proven)
tictactoe_json_verifier/ ← Tic-Tac-Toe with contracts (asserted, not solver-proven)
conways_life_json_verifier/ ← Life with contracts (see its VERIFICATION_SCOPE.md)
erc20_token/ ← ERC-20 benchmark (frozen ground truth)
totp_rfc6238/ ← TOTP RFC 6238 benchmark
benchmarks/ ← agent-fill benchmark seeds (B1/B3/B5)
secure-channel-emergent/ ← emergent flagship: 25 fns / 7 modules, agents invented the decomposition
token-revocation-emergent/ ← emergent data flagship: RFC 7662/7009, agent-invented bodies, 5 refute twins
heartbleed/ ← Heartbleed (CVE-2014-0160) + TLS record layer; scales to a 163-fn channel
gotofail/ ← Apple "goto fail" (CVE-2014-1266) with real sum types
payments-core/ ← flagship verified-payments demo: two-account conservation, transfer/debit call chain, settle (see "See it")
withdraw-demo/ ← repair-loop demo: holes → checkout/patch → two-axis trust + composition + CDP + proof-artifact
refine-demo/ ← cascading refine: one hole → contracted sub-hole tree, each state verified
tcp_rfc793/ ← RFC 793 connection state machine, legal-successor safety
session-pay/ ← Connected demo: protocol state-safety + verified payment + bounded amount in one verified function
nested-result/ ← Nested Result-variable match under let
refined-payload/ ← Matched Result payload refinement + weaker-forward refusal
outcome-totality/ ← Payload-carrying outcome sum, verified legal/illegal totality
banking_ledger/ ← Three-level assume-guarantee chain (transfer → withdraw → safe-subtract) + refuting twin
orchestrator_walkthrough/ ← Auth module orchestration exercise
docs/
UPDATE-PROTOCOL.md ← Doc canonical-sources + per-change update matrix
getting-started.md ← Build guide, known-good patterns, schema versioning
compiler-team-roadmap.md ← Engineering backlog and shipped-releases history
llmll-ast.schema.json ← JSON-AST schema (use with AI agents)
orchestrator-walkthrough.md ← End-to-end orchestration walkthrough
one-pager.md ← Project overview / pitch document
design/ ← Active design proposals (status in design/INDEX.md)
INDEX.md ← Reading guide for active design documents
archive/ ← Superseded design specs, shipped proposals, professor reviews, wasm investigations
tools/
llmll-orchestra/ ← Python orchestrator (pip package)
llmll_orchestra/
orchestrator.py ← Fill-mode orchestrator
lead_agent.py ← Lead Agent skeleton generation (plan/lead/auto modes)
quality.py ← Skeleton quality heuristics
agent.py ← LLM agent interface
compiler.py ← Compiler CLI wrapper
GPLv3 with LLMLL Runtime Library Exception — see LICENSE.