Show HN: Llmll – AI agents fill typed holes, an SMT solver rejects wrong fills

LLMLL (Large Language Model Logical Language), a programming language and verification pipeline whose primary author is an LLM agent, uses the Z3 SMT solver to prove each AI-written function body against its formal contract before a patch is applied, refuting type-correct but incorrect implementations. In the project's `conserve(from, to, amount)` example, a body that credits the destination one extra unit passes type-checking but fails verification with "implementation does not satisfy postcondition (constraint #0)," while the conserving body verifies as SAFE via liquid-fixpoint. The project's stated goal is to turn hallucination from a failure mode into a search strategy by having agents fill typed `?hole` contracts that `llmll patch` accepts only if the program still type-checks and the solver does not refute it.

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 https://github.com/machunter/llmll/blob/main/CHANGELOG.md Latest . Full release notes per version live in CHANGELOG; this README does not duplicate them. Learn more: docs/README.md https://github.com/machunter/llmll/blob/main/docs/README.md is the reading guide to the documentation · ROADMAP.md https://github.com/machunter/llmll/blob/main/ROADMAP.md says what has shipped and what is next · experiments/README.md https://github.com/machunter/llmll/blob/main/experiments/README.md indexes 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 why-not-have-an-agent-write-dafny-liquid-haskell-or-f . <sub 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.</sub Full copy-pasteable walkthrough: payments-core/DEMO-RUNBOOK.md https://github.com/machunter/llmll/blob/main/examples/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 https://github.com/machunter/llmll/blob/main/examples/withdraw-demo/DEMO-RUNBOOK.md narrated: DemoPost.md https://github.com/machunter/llmll/blob/main/examples/withdraw-demo/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 checkout gives an agent a typed ?hole with its precondition, the postcondition it must meet and the names in scope, and not the answer. llmll patch applies the fill only if the program still type-checks and the solver does not refute it. - Weak contracts are flagged. --weakness-check reports a contract so weak that a trivial body satisfies it; --cdp scores how sharply a contract rules out wrong bodies. - Every function carries a trust level. The trust report marks each function verified , asserted and so on, and a verified claim 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 refine fills 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/ https://github.com/machunter/llmll/blob/main/experiments/minimal-agent/SUMMARY.md , 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 https://github.com/machunter/llmll/blob/main/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. <sub 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 .</sub bash $ 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 deferred LEAN-GA rebuild. Reproduce: examples/leanstral-demo/ https://github.com/machunter/llmll/blob/main/examples/leanstral-demo demo.sh · design: docs/archive/shipped-design-specs/leanstral-demo-spec.md https://github.com/machunter/llmll/blob/main/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 https://github.com/machunter/llmll/blob/main/examples/withdraw-demo/DEMO-RUNBOOK.md . <sub 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 https://github.com/machunter/llmll/blob/main/examples/withdraw-demo/demo.sh .</sub 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.llmll From source. Build first: cd compiler && stack build stack exec llmll -- --help Requires 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-fixpoint absent, verify prints a SOLVER NOT FOUND -- NOTHING WAS PROVEN banner and exits 3 , and patch / refine refuse to apply a contracted patch PatchVerifyUnavailable , exit 3 . Install both to see the refutation. The Docker image bundles both, so it never hits this. See docs/getting-started.md https://github.com/machunter/llmll/blob/main/docs/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 https://github.com/machunter/llmll/blob/main/LLMLL.md . 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 https://github.com/machunter/llmll/blob/main/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 https://github.com/machunter/llmll/blob/main/.github/workflows/version-gate.yml 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/ https://github.com/machunter/llmll/blob/main/tools/llmll-driver/README.md 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 https://github.com/machunter/llmll/blob/main/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. | Command | What it does | |---|---| | llmll check <file --strict | Parse + type-check; emit structured diagnostics. With --strict : unbound variables, unknown functions, unknown operators, and branch type mismatches are hard errors instead of warnings. Without --strict : text mode renders accumulated warnings on success. | | llmll holes <file --deps --deps-out FILE | List all ?hole expressions. With --deps : include dependency graph in --json output. With --deps-out : persist graph to file. | | llmll test <file | Run property-based tests check / for-all blocks via QuickCheck | | llmll build <file -o <dir | Generate a Haskell package src/Lib.hs + package.yaml + stack.yaml and compile it with stack build , or ghc --make when Stack is absent. Accepts both .llmll S-expression and .ast.json JSON-AST sources. With neither stack nor ghc on PATH it fails exit 1 ; --emit-only writes the package without compiling it. | | llmll build-json <file.ast.json -o <dir | Compile a JSON-AST source to a Haskell package: the build pipeline reading .ast.json input. --emit-only writes the Haskell sources but skips the internal stack build; --contracts MODE sets the runtime assertion mode full default, unproven , none . | | llmll run <file args... | Compile the program and run it immediately; requires a def-main . The program inherits this process's stdin, stdout and stderr, and llmll run exits with the program's own status. Trailing arguments are passed through to the running program, flags included; -- is needed only before an argument that starts with - and must not be read as a flag. | | llmll verify <file --fq-out FILE --leanstral --leanstral-lean-project DIR --leanstral-mock --trust-report --weakness-check --obligations --obligation-report --spec-coverage --strict-verified-core --cdp --strict-verify --proof-artifact FILE | Emit .fq constraint file and run liquid-fixpoint if installed . With --proof-artifact FILE , also writes a unified, replayable verification record consolidating the trust/obligation/ .fq /sidecar surfaces plus the determinism pins. With --leanstral experimental , sends nonlinear obligations to a live Leanstral prover and checks the returned proof with the Lean kernel see above ; --leanstral-mock runs the same pipeline against a mock prover. With --trust-report , prints per-function trust summary with transitive closure, epistemic drift warnings, and weakness-ok suppressions note: --trust-report reloads persisted evidence instead of running fixpoint , so a solver-refutable function renders as asserted , not refuted ; use the default verify or --strict-verified-core to surface refuted . With --weakness-check , detects specs that admit trivial implementations. With --obligations , suggests postcondition strengthening when UNSAFE at cross-function boundaries. With --obligation-report , emits structured JSON obligation report for every hole, unproven contract, and failed call-site precondition. With --spec-coverage , classifies every function and computes effective specification coverage ratio. With --strict-verified-core , hard-errors if any function falls back from body-faithful verification, carries overflow-tainted verified evidence, or is refuted body-faithful but disproved by the solver , transitively over the call graph, or reaches an imported contract that is not proved fell back, never verified, or changed since . With --cdp , computes contract discriminative power per function: emits a paired discriminative axis block in the trust-report JSON alongside the existing evidence axis. With --strict-verify , runs --trust-report --weakness-check --spec-coverage --cdp together: the recommended serious-verify path. | | llmll replay-artifact <FILE | Re-derive and check a recorded proof artifact: recompute the source hash, re-run the stored VC under the pinned solver, and fail closed on any source/solver-determinism mismatch or unknown /timeout. | | llmll typecheck --sketch <file | Partial-program type inference. Returns inferred type for every ?hole plus holeSensitive -annotated errors and invariant suggestions from the pattern registry. | | llmll serve --host H --port P --token T | Expose --sketch as POST /sketch HTTP endpoint for agent swarms. Default: 127.0.0.1:7777 . | | llmll checkout <file.ast.json <pointer --multi N | Lock a ?hole for exclusive agent editing. Returns a checkout token with the hole's contract context contract pre , postcondition goal , path condition and typing context in scope , type definitions . Use --release to abandon, --status to query TTL. With --multi N , opens or joins an R5 divergence session: N concurrent scratch-isolated tokens on one pointer. | | llmll diverge-report <file.ast.json <session | R5: collect a divergence session's fills and emit the divergence witness record. The session id is the one returned by checkout --multi . A fill the solver could not grade no solver, or no verdict is listed under status partition.unavailable , the record carries solver available , and the command exits 3. A fill whose body is outside the decidable fragment is listed under status partition.outside fragment , not refuted , and does not change the exit code. | | llmll patch <file.ast.json <patch.json | Apply an RFC 6902 JSON-Patch to a checked-out hole. Re-type-checks and re-verifies SMT the patched program before writing it. Exits 1 on a rejection, and 3 PatchVerifyUnavailable , nothing written when the solver is missing or returns no verdict. A success reports, per patched function, whether its body was proved verification .body faithful ; --require-proof refuses a fill whose postcondition passed only as an assumption PatchNotProved . | | llmll refine <file.ast.json <refine.json | Fill a checked-out hole and spawn new contracted sub-holes its body calls, atomically cascading decomposition . Spawned sub-contracts pass a feasibility no-miracle gate a sub-contract no body can discharge is rejected with a witnessing input and a CDP vacuity gate; in-scope defs whose contracts subsume a spawned sub-contract are surfaced as advisory reuse suggestions non-blocking W-REUSE on an exact contract-equivalent . | | llmll hub fetch --from-file <tarball | Install a local .tar.gz package into the hub cache ~/.llmll/modules/ . Local tarballs only; there is no registry-by-name fetch. | | llmll hub scaffold <template --output DIR | Generate a project from a llmll-hub skeleton template ~/.llmll/templates/ . | | llmll hub query --signature <sig | Search hub cache for functions matching a type signature e.g. "int - int - int" . | | llmll replay <source <log | Rebuild program, replay event log inputs, compare outputs for determinism verification. | | llmll spec --json | Emit agent prompt specification from compiler builtins. Text default or JSON output. | | llmll version | Print compiler version and exit. Supports --json for {"version":"…"} output. Also available as llmll --version . | | llmll repl | Start an interactive LLMLL REPL | Both source formats compile to identical AST nodes: | Format | Extension | Best for | |---|---|---| | S-expressions | .llmll | Human editing, concise iteration | | JSON-AST | .ast.json | AI agents — schema-constrained, structurally valid by construction | 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 hangman LLMLL 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. | Construct | SMT body-faithful | Fallback | |---|---|---| | ELit , EVar int / bool , linear ops + - = < <= = = | ✅ | n/a | | ELet PVar , EIf ≤4096 paths | ✅ path-split | n/a | | EApp contracted callee, same-file or imported | ✅ assume-guarantee | n/a | | EApp uncontracted callee | ❌ | contract-only | | EApp recursive self / cycle | ✅ partial; ✅ total with decreases e | no measure: termination unverified ; bad measure: measure-not-decreasing | | EMatch on non-recursive sums Result and user ADTs, nested and sequential | ✅ n-ary int-tag | n/a | | EPair / pair returns first , second , pair | ✅ datatype selectors | n/a | | Non-recursive datatype construction | ✅ | n/a | | bytes n and map operations bytes-get / -set / -length / -zero , map-has / -get / -put / -empty | ✅ array theory; index-in-bounds and key-presence are proof obligations | non- {int,string} keys, direct map-empty reads, whole-structure = : contract-only | | String literals in = / = , string-length of a literal | ✅ | string structure concat, substring, regex : contract-only | | EMatch recursive-sum payload , ELambda , EDo | ❌ | contract-only / runtime | | letrec own body VC | ❌ | runtime + :decreases | | Non-linear ops , / , mod | ❌ | runtime + ?proof-required experimental --leanstral | | Int overflow | ✅ no gap | int is unbounded Integer in both the verifier and the generated code | Full verification matrix: LLMLL.md §5.3.5 https://github.com/machunter/llmll/blob/main/LLMLL.md . Start here: examples/README.md https://github.com/machunter/llmll/blob/main/examples/README.md is the tiered index to every example. | Example | What it proves | |---|---| | examples/secure-channel-emergent/ https://github.com/machunter/llmll/blob/main/examples/secure-channel-emergent | Emergent flagship. A Heartbleed-domain secure channel, 25 functions across 7 import-linked modules, where agents invented the entire decomposition via cascading refine with no reference solution; the spine composes six modules through cross-module assume-guarantee and declines an unsteered goto-fail bait | | examples/token-revocation-emergent/ https://github.com/machunter/llmll/blob/main/examples/token-revocation-emergent | Emergent data flagship. An OAuth RFC 7662/7009 introspection/revocation service, 8 functions / 5 modules, where both the contracts RFC :source -tagged and the agent-invented bodies are machine-auditable; 5 famous-bug refute twins, CI-frozen | | examples/heartbleed/ https://github.com/machunter/llmll/blob/main/examples/heartbleed | Heartbleed CVE-2014-0160 + a full TLS record layer: the buggy heartbeat that echoes an unbounded claimed length is refuted at copy-bytes ' bound; scales to a 163-function channel | | examples/gotofail/ https://github.com/machunter/llmll/blob/main/examples/gotofail | Apple "goto fail" CVE-2014-1266 modeled with real sum types: Verified only if the signature stage returned Continue ; the bug returning Verified on the Abort arm is refuted | | Demo | What it proves | |---|---| | examples/payments-core/ https://github.com/machunter/llmll/blob/main/examples/payments-core | Flagship. Two-account conservation over a pair return conserve — "money can't be created"; transfer verified over a debit call edge no-overdraw ; settle is a Result -match return | | examples/tcp rfc793/ https://github.com/machunter/llmll/blob/main/examples/tcp rfc793 | RFC 793 connection state machine reaches verified on legal-successor safety; step-bad is refuted | | examples/session-pay/ https://github.com/machunter/llmll/blob/main/examples/session-pay | Connected demo: protocol state-safety + verified payment + bounded amount in one verified function | | examples/nested-result/ https://github.com/machunter/llmll/blob/main/examples/nested-result | A nested Result -variable match under let reaches verified | | examples/refined-payload/ https://github.com/machunter/llmll/blob/main/examples/refined-payload | A matched Result Pos,string arm uses its payload's 0 verified ; a caller forwarding a weaker Result int is refused | | examples/outcome-totality/ https://github.com/machunter/llmll/blob/main/examples/outcome-totality | A payload-carrying Accepted n / Rejected n outcome with a verified legal→Accepted / illegal→Rejected totality | | examples/banking ledger/ https://github.com/machunter/llmll/blob/main/examples/banking ledger | Three-level assume-guarantee chain transfer → withdraw → safe-subtract , all verified; the twin that drops one guard is refuted at the call site | | examples/withdraw-demo/ https://github.com/machunter/llmll/blob/main/examples/withdraw-demo | The repair loop hole → rejected bad fills → accepted fix → verified + the return-refine beat | | examples/refine-demo/ https://github.com/machunter/llmll/blob/main/examples/refine-demo | Cascading refine : one hole decomposed top-down into a contracted sub-hole tree, every intermediate state verified via assume-guarantee; two guardrails reject a vacuous or orphan decomposition | | examples/bytes-bounds/ https://github.com/machunter/llmll/blob/main/examples/bytes-bounds | bytes n memory safety: a correct bounds check verifies; the off-by-one <= for < and an out-of-range write are refuted at the call site | | examples/total-recursion/ https://github.com/machunter/llmll/blob/main/examples/total-recursion | A recursive function with decreases n verifies total termination discharged ; a bad measure fails on the distinct measure-not-decreasing channel | | examples/rfc1982 serial/ https://github.com/machunter/llmll/blob/main/examples/rfc1982 serial | RFC 1982 serial arithmetic via the spec-from-RFC pipeline: all three functions verified with per-clause :source ; the historical naive- < DNS bug refutes | | Example | Format | Description | |---|---|---| | examples/hangman sexp/ | S-expression | Full Hangman game with ASCII gallows art; uses def-main :mode console | | examples/hangman json/ | JSON-AST | Same program, JSON-AST schema-constrained version | | examples/tictactoe sexp/ | S-expression | Two-player Tic-Tac-Toe; demonstrates :done? + :on-done | | examples/life sexp/ | S-expression | Conway's Game of Life; multi-module core , world , main | | examples/life json/ | JSON-AST | Same Life program in JSON-AST format | | examples/withdraw.llmll | S-expression | Simple withdraw with pre / post contracts; acceptance gate | | examples/hangman json verifier/ | JSON-AST | Hangman with apply-guess contracts llmll verify ; asserted, not solver-proven | | examples/tictactoe json verifier/ | JSON-AST | Tic-Tac-Toe with set-cell contracts asserted, not solver-proven | | examples/conways life json verifier/ | JSON-AST | Conway's Life — next-cell / count-neighbors contracts see its VERIFICATION SCOPE.md | | examples/replay-demo/ | S-expression | The llmll replay demo: codegen + deterministic event-log replay used by docs/getting-started.md | | examples/proof required test/ | S-expression | Leanstral proof pipeline validation | | examples/erc20 token/ | JSON-AST | ERC-20 benchmark — frozen ground truth with verification-scope matrix | | examples/totp rfc6238/ | JSON-AST | TOTP RFC 6238 benchmark — crypto builtins, RFC :source provenance | 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 | Document | Purpose | |---|---| | LLMLL.md https://github.com/machunter/llmll/blob/main/LLMLL.md | Full language specification — types, syntax, FFI, grammar, builtins | | docs/README.md https://github.com/machunter/llmll/blob/main/docs/README.md | Reading guide to docs/ : what to read first, and what is working material | | ROADMAP.md https://github.com/machunter/llmll/blob/main/ROADMAP.md | Public roadmap: what has shipped, what is next, deliberate boundaries | | experiments/README.md https://github.com/machunter/llmll/blob/main/experiments/README.md | Index of the experiments and their headline results | | docs/getting-started.md https://github.com/machunter/llmll/blob/main/docs/getting-started.md | Build guide + known-good patterns + schema versioning single reference for agents | | docs/compiler-team-roadmap.md https://github.com/machunter/llmll/blob/main/docs/compiler-team-roadmap.md | Engineering backlog and shipped-releases history current version in CHANGELOG § Latest https://github.com/machunter/llmll/blob/main/CHANGELOG.md Latest | | docs/llmll-ast.schema.json https://github.com/machunter/llmll/blob/main/docs/llmll-ast.schema.json | Machine-readable JSON-AST schema | | docs/UPDATE-PROTOCOL.md https://github.com/machunter/llmll/blob/main/docs/UPDATE-PROTOCOL.md | Doc canonical-sources table and per-change update matrix | | docs/orchestrator-walkthrough.md https://github.com/machunter/llmll/blob/main/docs/orchestrator-walkthrough.md | End-to-end multi-agent orchestration walkthrough with auth module exercise | | docs/one-pager.md https://github.com/machunter/llmll/blob/main/docs/one-pager.md | Project overview — problem, approach, status, related work | | docs/design/INDEX.md https://github.com/machunter/llmll/blob/main/docs/design/INDEX.md | Reading guide for all active design documents | | CHANGELOG.md https://github.com/machunter/llmll/blob/main/CHANGELOG.md | Release notes by version | GPLv3 with LLMLL Runtime Library Exception — see LICENSE https://github.com/machunter/llmll/blob/main/LICENSE .