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

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.md is the reading guide to the documentation · ROADMAP.md says what has shipped and what is next · 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:

$ llmll verify conserve-bad.llmll
error: body verification of 'conserve-bad' failed —
       implementation does not satisfy postcondition (constraint #0)

$ 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 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 functionverified ,asserted and so on, and averified 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/, 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 deferred LEAN-GA rebuild. 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:

docker run --rm ghcr.io/machunter/llmll verify /opt/llmll/examples/payments-core/conserve-bad.llmll
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.

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.

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 withstack build , orghc --make when Stack is absent. Accepts both.llmll S-expression and.ast.json JSON-AST sources. With neitherstack norghc 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, andllmll 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 runliquid-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, andweakness-ok suppressions (note:--trust-report reloads persisted evidenceinstead of running fixpoint , so a solver-refutable function renders asasserted , notrefuted ; use the defaultverify or--strict-verified-core to surfacerefuted ). 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 paireddiscriminative_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 orunknown /timeout.
llmll typecheck --sketch <file>	Partial-program type inference. Returns inferred type for every ?hole plusholeSensitive -annotated errors andinvariant_suggestions from the pattern registry.
llmll serve [--host H] [--port P] [--token T]	Expose --sketch asPOST /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 bycheckout --multi . A fill the solver could not grade (no solver, or no verdict) is listed understatus_partition.unavailable , the record carriessolver_available , and the command exits 3. A fill whose body is outside the decidable fragment is listed understatus_partition.outside_fragment , notrefuted , 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 advisoryreuse_suggestions (non-blockingW-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 asllmll --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

stack exec llmll -- check ../examples/hangman_sexp/hangman.llmll

stack exec llmll -- build ../examples/hangman_sexp/hangman.llmll -o ../generated/hangman_sexp

stack exec llmll -- build ../examples/hangman_json/hangman.ast.json -o ../generated/hangman_json

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] andmap 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.

Start here: examples/README.md is the tiered index to every example.

Example	What it proves
examples/secure-channel-emergent/	Emergent flagship. A Heartbleed-domain secure channel, 25 functions across 7 import-linked modules, where agentsinvented the entire decomposition via cascadingrefine 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/	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/	Heartbleed (CVE-2014-0160) + a full TLS record layer: the buggy heartbeat that echoes an unbounded claimed length isrefuted atcopy-bytes ' bound; scales to a 163-function channel
examples/gotofail/	Apple "goto fail" (CVE-2014-1266) modeled with real sum types: Verified only if the signature stage returnedContinue ; the bug (returningVerified on theAbort arm) isrefuted

Demo	What it proves
examples/payments-core/	Flagship. Two-account conservation over a pair return (conserve ) — "money can't be created";transfer verified over adebit call edge (no-overdraw);settle is aResult -match return
examples/tcp_rfc793/	RFC 793 connection state machine reaches verified on legal-successor safety;step-bad isrefuted
examples/session-pay/	Connected demo: protocol state-safety + verified payment + bounded amount in one verified function
examples/nested-result/	A nested Result -variable match (underlet ) reachesverified
examples/refined-payload/	A matched Result[Pos,string] arm uses its payload's> 0 (verified ); a caller forwarding a weakerResult[int] is refused
examples/outcome-totality/	A payload-carrying Accepted(n) /Rejected(n) outcome with a verified legal→Accepted / illegal→Rejected totality
examples/banking_ledger/	Three-level assume-guarantee chain ( transfer → withdraw → safe-subtract ), all verified; the twin that drops one guard isrefuted at the call site
examples/withdraw-demo/	The repair loop (hole → rejected bad fills → accepted fix → verified) + the return-refine beat
examples/refine-demo/	Cascading refine : one hole decomposed top-down into a contracted sub-hole tree, every intermediate stateverified via assume-guarantee; two guardrails reject a vacuous or orphan decomposition
examples/bytes-bounds/	bytes[n] memory safety: a correct bounds check verifies; the off-by-one (<= for< ) and an out-of-range write arerefuted at the call site
examples/total-recursion/	A recursive function with (decreases n) verifiestotal (termination discharged); a bad measure fails on the distinctmeasure-not-decreasing channel
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 itsVERIFICATION_SCOPE.md )
examples/replay-demo/	S-expression	The llmll replay demo: codegen + deterministic event-log replay (used bydocs/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	Full language specification — types, syntax, FFI, grammar, builtins
docs/README.md	Reading guide to docs/ : what to read first, and what is working material
ROADMAP.md	Public roadmap: what has shipped, what is next, deliberate boundaries
experiments/README.md	Index of the experiments and their headline results
docs/getting-started.md	Build guide + known-good patterns + schema versioning (single reference for agents)
docs/compiler-team-roadmap.md	Engineering backlog and shipped-releases history (current version in CHANGELOG § Latest )
docs/llmll-ast.schema.json	Machine-readable JSON-AST schema
docs/UPDATE-PROTOCOL.md	Doc canonical-sources table and per-change update matrix
docs/orchestrator-walkthrough.md	End-to-end multi-agent orchestration walkthrough with auth module exercise
docs/one-pager.md	Project overview — problem, approach, status, related work
docs/design/INDEX.md	Reading guide for all active design documents
CHANGELOG.md	Release notes by version

GPLv3 with LLMLL Runtime Library Exception — see LICENSE.

source & further reading

github.com — original article Show HN: Porch – a Mac menu bar work log for Claude Code and Codex sessions Show HN: Tallyhook – price Claude Code and Codex logs per client you bill Sub-1-Bit LLM Compression via Latent Factorization