Part of the Lex project — Agents · Manifesto · All packages
A Lex-native coding assistant — think Claude Code or Cursor, built entirely in the Lex ecosystem.
Trust Without Comprehension — live demo
Effect-typed parallel orchestration (§VI) + tamper-evident audit (§VIII) — verified live by the type checker:
# run it yourself
bash examples/manifesto_full_chain/demo.shUse bin/lex-code rather than calling lex run by hand: it supplies
the capability grant every session needs, the main -- separator that
stops your first flag being read as a function name, and a raised
--max-steps — the VM's 10,000,000-step default is a DoS guard for
untrusted sandboxed snippets, not for a long agentic session, and a
verbose provider's ordinary output can hit it outright partway through
a real task. Calling lex run directly (as the rest of this README
does, for entry points other than the TUI) needs the same flag added
by hand; see bin/lex-code's own comment for the full story.
# set provider keyexport ANTHROPIC_API_KEY=sk-...
# build mode (default), interactive REPL
./bin/lex-code
# one-shot CLI mode (exits after the task)
./bin/lex-code "implement list.zip"# plan mode
./bin/lex-code --plan
# mistral provider
./bin/lex-code --mistral
# bootstrap demo: impl → spec → test → review
lex run src/bootstrap/run.lex
# web UI + HTTP API on :7700 (see Web Frontend)
lex run --max-steps 20000000000 --allow-effects approval,concurrent,crypto,env,fs_read,fs_walk,fs_write,io,llm,net,proc,random,sql,stream,time \
src/server/web.lex serve_web# installs to /usr/local/bin/lex-code and /usr/local/lib/lex-code/
make install
# custom prefix
make install PREFIX=~/.local
# uninstall
make uninstallAfter install, lex must still be on your PATH (it’s the interpreter).
lex-code "implement list.zip"
lex-code --plan --ollama "how should we structure the session module?"| Flag | Mode | Role |
|---|---|---|
| (default) | Build | Write and edit Lex source files |
--plan | Plan | Produce implementation plans, no writes |
--explore | Explore | Read + grep, understand the codebase |
--refactor | Refactor | Restructure code, rename, inline |
--spec | Spec | Generate lex-spec Spec values |
--test | Test | Write unit and property tests |
--review | Review | Code-review: correctness, style, effects |
--verify | Verify | Independently re-derive expected output from the task's own spec and check the implementation against it — never trusts the implementation's existing test file (below) |
--bar | Bar | Walk a project against the minimum bar, read-only (below) |
--multi | Multi | Run Build + Test in parallel via std.conc |
| Flag | Provider | Model | Key required |
|---|---|---|---|
| (default) | Anthropic | claude-sonnet-4-6 | ANTHROPIC_API_KEY |
--openai | OpenAI | gpt-5.5 | OPENAI_API_KEY |
--google | gemini-3.5-flash | GOOGLE_API_KEY | |
--mistral | Mistral | mistral-large-latest | MISTRAL_API_KEY |
--litellm | LiteLLM proxy | $LITELLM_MODEL | none (proxy handles keys) |
--ollama | Ollama (local, native API) | $OLLAMA_MODEL | none |
--vllm | vLLM (local/remote) | $VLLM_MODEL | none |
--opencode | OpenCode Go plan (cloud, direct) | $OPENCODE_MODEL | OPENCODE_API_KEY |
ollama pull codellama # or llama3, deepseek-coder, qwen2.5-coder, …
lex run src/tui/main.lex --ollama# start vLLM server
python -m vllm.entrypoints.openai.api_server \
--model mistralai/Mistral-7B-Instruct-v0.3
# run lex-code against it
VLLM_MODEL=mistralai/Mistral-7B-Instruct-v0.3 \
lex run src/tui/main.lex --vllm "implement list.zip"# remote GPU box
VLLM_BASE_URL=http://gpu-box:8000/v1/chat/completions \
VLLM_MODEL=deepseek-ai/DeepSeek-Coder-V2-Lite-Instruct \
lex run src/tui/main.lex --vllmVLLM_MODEL defaults to mistralai/Mistral-7B-Instruct-v0.3.
VLLM_BASE_URL defaults to http://localhost:8000/v1/chat/completions.
OpenCode Go bundles cloud access to several open-weight coding models (DeepSeek, Qwen3, Kimi, GLM, MiniMax, MiMo) behind one subscription key. Two ways to reach it — same key either way:
# native (direct to the Go endpoint, no proxy)export OPENCODE_API_KEY=$(cat ~/.credentials/opencode/key | tr -d '\n')
lex run --max-steps 20000000000 --allow-effects approval,concurrent,crypto,env,fs_read,fs_walk,fs_write,io,llm,net,proc,random,sql,stream,time \
src/tui/main.lex main -- --opencode "implement list.zip"# override the default model (kimi-k2.7-code)
OPENCODE_MODEL=qwen3.7-max \
lex run --max-steps 20000000000 --allow-effects approval,concurrent,crypto,env,fs_read,fs_walk,fs_write,io,llm,net,proc,random,sql,stream,time \
src/tui/main.lex main -- --opencode "implement list.zip"# via the LiteLLM proxy instead (shares one proxy + model list with lex-loom — see below)
LITELLM_MODEL=deepseek-v4-flash \
lex run --max-steps 20000000000 --allow-effects approval,concurrent,crypto,env,fs_read,fs_walk,fs_write,io,llm,net,proc,random,sql,stream,time \
src/tui/main.lex main -- --litellm "implement list.zip"OPENCODE_MODEL accepts any Go-plan model id (see litellm/config.yaml's "OpenCode Go plan" section for the full list). OPENCODE_BASE_URL overrides the endpoint if you're routing through a local reasoning proxy instead of hitting opencode.ai directly.
LiteLLM is the recommended path for running local models, and the only path that gives OpenCode Go's thinking-mode models correct merge_reasoning_content_in_choices handling. It provides an OpenAI-compatible endpoint over any backend (Ollama, vLLM, OpenCode Go, MLX, …), which gives cleaner tool calling than the native Ollama wire format.
This repo ships a ready-to-run proxy config at litellm/config.yaml + litellm/docker-compose.yml — kept in sync with lex-loom's own litellm/ directory (same model list, same OpenCode Go entries) so both repos can point at one shared proxy instance.
# start the bundled proxycd litellm
ANTHROPIC_API_KEY=... OPENAI_API_KEY=... OPENCODE_API_KEY=... docker compose up -d
cd ..
# run lex-code against qwen3-coder:30b (recommended local model)
LITELLM_MODEL=qwen3-coder:30b \
lex run --max-steps 20000000000 --allow-effects approval,concurrent,crypto,env,fs_read,fs_walk,fs_write,io,llm,net,proc,random,sql,stream,time \
src/tui/main.lex main
# one-shot via the --litellm flag
LITELLM_MODEL=qwen3-coder:30b \
lex run --max-steps 20000000000 --allow-effects approval,concurrent,crypto,env,fs_read,fs_walk,fs_write,io,llm,net,proc,random,sql,stream,time \
src/tui/main.lex main -- --litellm "implement list.zip"# OpenCode Go through the proxy instead of native --opencode
LITELLM_MODEL=kimi-k2.7-code \
lex run --max-steps 20000000000 --allow-effects approval,concurrent,crypto,env,fs_read,fs_walk,fs_write,io,llm,net,proc,random,sql,stream,time \
src/tui/main.lex main -- --litellm "implement list.zip"# override the proxy URL (default: http://localhost:4000)
LITELLM_BASE_URL=http://gpu-box:4000 \
LITELLM_MODEL=qwen3-coder:30b \
lex run --max-steps 20000000000 --allow-effects approval,concurrent,crypto,env,fs_read,fs_walk,fs_write,io,llm,net,proc,random,sql,stream,time \
src/tui/main.lex main -- --litellmLITELLM_MODEL is the model name as it appears in litellm/config.yaml's model_name field.
LITELLM_BASE_URL defaults to http://localhost:4000.
Running against a standalone LiteLLM install instead of the bundled compose file works the same way — point litellm --config <your-config.yaml> --port 4000 at any config with the model names you use.
Tested on lex-code fizzbuzz bootstrap — task: write fizzbuzz.lex with fn fizzbuzz(n :: Int) -> List[Str] + 4 unit tests, lex check clean, run_all returns 0.
| Model | VRAM | Steps | Result | Notes |
|---|---|---|---|---|
qwen3-coder:30b (Q4_K_M) | 45 GB | ~14 LLM rounds | ✅ passes | Best local choice. Correct tool use, proper Lex idioms after linter feedback. |
gemma4:26b (Q4) | 19 GB | — | ❌ fails | Thinking model: consumes 500–700 tokens on chain-of-thought before any output. Tool calls appear as embedded JSON in content instead of tool_calls. Generates Python instead of Lex under large context. |
gemma4:latest (9 B) | 10 GB | — | not tested | Lighter variant; same thinking-model caveats apply. |
Reliable patterns with qwen3-coder:30b:
# Warm the model before a run (first call loads weights, subsequent calls are faster)
curl -s http://localhost:4000/v1/chat/completions \
-H "Content-Type: application/json" \
-d '{"model":"qwen3-coder:30b","messages":[{"role":"user","content":"hi"}],"max_tokens":10,"stream":false}' \
> /dev/null
LITELLM_MODEL=qwen3-coder:30b \
lex run --allow-effects env,io,net,llm,proc,sql,fs_write,time,approval \
src/bootstrap/fizzbuzz_lex.lex main
# [fizzbuzz_lex] starting build via litellm# [fizzbuzz_lex] done — steps: 71$ lex check fizzbuzz.lex && lex run fizzbuzz.lex run_all
ok
0The browser client sends session_id and the server honours it. A session is
whatever its trail derives — resume_session reads
.lex/sessions/<id>.db and rebuilds the conversation per request, so it
survives a page reload and a server restart.
This is not the registry pattern the ACP path uses, and could not be:
net.serve_fn hands the handler a Request and nothing else, so there is no
value to thread between requests and nowhere to keep an in-memory map. That
constraint points at #54's contract rather than away from it — the
conversation is a projection of the trail, so deriving it per request is the
design, not a substitute for a cache.
A client-supplied id becomes a file path, so it is checked: lowercase hex, 4–64 characters, anything else replaced with a fresh id. An id the server has never seen is a working empty session rather than an error, because a log with no events derives the empty conversation.
Session logs are swept at server start — older than
persist.max_session_age_days() (30) by mtime, which moves on every turn.
Age rather than count, so an eviction cannot take a conversation someone is
still in.
Facts that outlive a session — a convention, a version pin, a gotcha. Three stages, and the boundary between them is enforced by the effect system rather than by policy.
The agent proposes.remember(kind, content, key?, why?) appends a
candidate. It cannot do more than that: lex-llm fixes the tool row at
[net, io, proc], with no sql and no time, and record-field rows unify by
equality — so no tool can widen it to what a durable write needs. An agent
cannot install a belief.
Consolidation disposes. At session start, src/memory/consolidate.lex
reconciles each candidate against what the project already knows:
| unknown kind, empty content | rejected |
| nothing known yet | accepted |
| identical to what is known | skipped |
| contradicts what is known | superseded — the trail keeps the previous value |
recent_change | accepted; it accumulates by design |
Rules are mechanical, not model-judged: a model adjudicating between two contradictory beliefs is the failure this mechanism exists to contain.
The trail records why. Every outcome, including a rejection, becomes a
memory.recorded event with a chained memory.reconciled attestation in
.lex/memory_trail.db — deliberately not the session log, which is in-memory
and gone at exit. So attest.chain answers "why does it believe this" with
something better than "it said so once".
A session opens with a summary, not the store. At most five entries per kind, newest first, and the header says how many were left out — a model that can see its excerpt is partial can ask for the rest; one shown a silently truncated list cannot.
Everything the prompt sees was attested by consolidation. A candidate that
was refused never leaves .lex/memory-candidates.jsonl.
Turns arrive as they happen. Text appears token by token, tool calls announce themselves as they are dispatched, and the reply lands when the model is done — rather than the whole turn appearing at once when it finishes.
This reaches every surface that shows steps: the TUI (repl and one-shot),
the ACP server's session/update notifications, and the web backend.
It depends on the provider offering a streaming half. anthropic, ollama, and
everything routed through the OpenAI adapter (LiteLLM, vLLM, lex-moe, MLX,
opencode-go, Mistral) do. google and vertex do not — Gemini answers with a
JSON array rather than SSE — so a turn on those still arrives in one burst.
Nothing else changes: the same steps reach the same renderer either way, so
there is no separate code path to fall out of date.
The pull loop lives in lex-llm's run_steps_streamed; run_turn_streaming_with_provider
in src/server/session.lex is the seam. Consuming a live socket carries the
[stream] effect, so every entry point's --allow-effects list includes it.
Step count explained:steps counts all d.Step records emitted by the agent loop — StepDelta (per LLM token event), StepToolExec, StepToolResult, and StepDone. One LLM round + one tool call ≈ 5 step records. 71 steps ≈ 14 LLM rounds (max_steps: 20 counts rounds, not records).
Avoiding the 0-delta stall: If Ollama receives many large-context requests in rapid succession it can enter a state where it returns {"done": false, "response": ""}. The agent loop sees 0 deltas, emits a silent empty StepDone, and the run appears to complete in 1 step with no output. Fix: restart Ollama (pkill -f "ollama serve" && open -a Ollama) and avoid batching many large-context calls without pauses.
Models with a chain-of-thought "thinking" phase need two things to work through LiteLLM:
max_tokens ≥ 2000— thinking tokens count against the budget before any visible output is produced. Withmax_tokens: 256the model exhausts its budget mid-thought and returns empty content.merge_reasoning_content_in_choices: trueinlitellm_config.yaml— without this, LiteLLM drops thecontentfield whenthinkingis present in the Ollama response.
# litellm_config.yaml
- model_name: gemma4:26blitellm_params:
model: ollama/gemma4:26bapi_base: http://localhost:11434merge_reasoning_content_in_choices: trueEven with these fixes, thinking models tend to emit tool calls as embedded JSON in content (rather than in the tool_calls field) when given 10+ function schemas. The openai.lex adapter has a content_tool_call fallback parser, but the generated code quality degrades significantly under large context. Use qwen3-coder:30b for coding tasks.
lex-code has been an MCP server for a while — src/server/mcp_main.lex
exposes its agents to Claude Desktop. It is now also a client, so an issue
tracker, a CI system or a package registry can be a tool the agent calls.
.lex/mcp.toml (an example ships at docs/mcp.toml.example):
[[servers]]
url = "http://localhost:3000"allow = ["search_issues", "create_pr"]
modes = ["build", "refactor"] # optional; defaults to build onlyTools arrive named mcp__<tool> — mcp__search_issues. The prefix is not
cosmetic: without it a server offering a tool called write or bash would
shadow a local one in the dispatcher's name lookup.
allow is the operator's gate — which of a server's tools this project
loads at all. An empty or missing allow list loads nothing. The opposite
reading ("no filter configured, so no filtering") is how a server that adds a
tool next week gets it into the prompt without anyone deciding.
modes is the agent's gate — which agent modes get them, defaulting to
build alone. Build's permission spec already permits everything, so that is
the one mode where adding a tool grants no new authority to a restricted
agent. An explore-mode agent that must not write does not reach an MCP tool
that writes unless you say so.
The issue asked for an mcp_tool(name) predicate in permissions/rules.lex.
There deliberately isn't one: lex-spec has no string-prefix operator so it
cannot be written, and permission enforcement is still tool-list based rather
than spec-based, so modes is the gate that actually runs. rules.lex
records what Phase 2 will need.
A server that is down, a config that will not parse, a name in allow the
server does not offer — each yields no tools and a printed note. The session
still starts: an unrelated outage should not become a total outage. But a tool
that quietly vanishes is the failure this codebase keeps finding (#32, #74),
so the absence is always said out loud.
Tools are loaded once per turn rather than cached. A cached list goes stale silently — a server that changes what it offers, or goes away, would keep being advertised to the model until the process restarted.
grep and glob match names. semantic_search matches intent — "validate an
A2A envelope", "retry a failed HTTP call" — by ranking every function's
signature, effects and examples against the query.
It needs an index, and the index needs an embeddings endpoint. LiteLLM is the
one lex-code speaks to, which is how Ollama is reached: the proxy presents
OpenAI's /v1/embeddings over ollama/nomic-embed-text, so lex-code never
learns Ollama's native embeddings shape. litellm/config.yaml ships the entry.
ollama pull nomic-embed-text # 768-dim, ~270MB, CPU is finecd litellm && docker compose up -d &&cd ..
lex run --max-steps 20000000000 --allow-effects env,io,net,proc \
src/index_build.lex main| Variable | Default | Meaning |
|---|---|---|
LITELLM_BASE_URL | http://localhost:4000 | proxy (shared with the chat path) |
LEX_EMBED_MODEL | nomic-embed-text | must be in the proxy's model list |
LEX_EMBED_DIMS | 128 | components kept per vector — see below |
LEX_INDEX_PATH | src/ | what to index |
--max-steps is not optional. The default VM budget is 10M opcode
dispatches and a whole-repo build blows straight through it.
Reading .lex/index.jsonl dominates query latency, and the reason is upstream:
jv.parse_into_errors is quadratic in document size, because
json_value.char_at walks the input with str.slice(src, p, p + 1) and slicing
is O(p). Doubling a JSON document roughly quadruples parse time — 16K/0.2s,
33K/0.9s, 66K/3.2s, 132K/13.7s, 264K/55.7s. So the index has to stay small, and
on this repo's 674 functions it measures:
| dims | index | read |
|---|---|---|
| 512 | 932K | 34s |
| 128 | ~500K | ~6s |
| 64 | 336K | 3s |
A 34-second search tool is not a search tool, so only the first
LEX_EMBED_DIMS components are kept. The same parser cost bounds indexing:
lex docs output for the whole tree is 310K and takes ~55s to parse before a
single embedding is requested, which is why LEX_INDEX_PATH defaults to a
subtree-sized scope rather than the repo. That is sound rather than merely cheap
for a Matryoshka-trained model like nomic-embed-text, which is trained so a
leading slice of the vector is itself a usable embedding; the prefix is
renormalised, since truncating changes the norm. Raise it for better ranking on
a small tree, lower it on a large one.
The reuse key is sig_id, not mtime: it hashes the function's own content, so
it answers "did this function change" rather than "was this file touched",
which is true after a comment edit and false after a git checkout that
rewinds content. Changing the model, endpoint or dims invalidates the whole
index — vectors are only comparable within one model, and mixing two vector
spaces in one ranking produces plausible nonsense rather than an error.
semantic_search is available to the explore, plan and review agents. It never
builds the index itself: a build makes one HTTP call per function, and
Tool.execute's [net, io, proc] row cannot read the env it would need.
Off by default. Point it at a collector and every turn arrives as a trace:
LEX_OTLP_ENDPOINT=http://localhost:4318 lex-code| Variable | Effect |
|---|---|
LEX_OTLP_ENDPOINT | POST OTLP/JSON to /v1/traces and /v1/metrics |
LEX_OTEL_STDOUT=1 | print the same envelopes to stdout instead |
An endpoint wins over the stdout flag, and with neither set nothing is
emitted — io.print is the TUI's own output stream, so a default-on stdout
exporter would dump OTel envelopes into your session on every turn.
The trace is projected from the trail, not instrumented separately.
lex-llm already writes cap.invoked before every tool call and
cap.completed / cap.failed after it, parented to the invoke, and every
trail event carries ts_ms. A start, an end, a parent link and a name is a
span — the trail was already a trace, just never spoken in OTel's wire
format. src/observability.lex reads the turn's slice of the log and
translates. Running a second span stream inside the same dispatch loop would
put two recorders on one set of facts, which is precisely how the
attestation chain broke (#32): the loop wrote one place, the reader read
another.
You get an agent.turn root span per turn, one tool.<name> child per
completed tool call, a tool.calls counter tagged by tool and success, and a
turn.duration_ms histogram. An invoke with no outcome — a turn cut short
mid-tool — is dropped rather than exported with a fabricated end time.
Span ids are derived, not drawn. Trail event ids are sha256 hashes of the
event's own content, so a span id taken from one is stable: re-exporting a
session reproduces the same trace instead of forging a rival. That also keeps
random out of the turn's effect row entirely. An unreachable collector
costs telemetry, never the turn.
src/server/mcp_main.lex exposes lex-code as a single code tool over
MCP, so any MCP-speaking host — Claude Code, Cursor, Zed — can hand it
a task. mode selects the agent strategy; the provider is a
server-launch choice, not a per-call argument.
LEX_CODE_PROVIDER=anthropic ANTHROPIC_API_KEY=… \
lex run --max-steps 20000000000 --allow-effects approval,concurrent,crypto,env,fs_read,fs_walk,fs_write,io,llm,net,proc,random,sql,stream,time \
src/server/mcp_main.lex main &
curl -s http://localhost:7778/.well-known/agent.json
curl -s -X POST http://localhost:7778/mcp \
-d '{"jsonrpc":"2.0","id":1,"method":"tools/list"}'
curl -s -X POST http://localhost:7778/mcp \
-d '{"jsonrpc":"2.0","id":2,"method":"tools/call","params":{"name":"code", "arguments":{"task":"add retries to fetch()","mode":"refactor"}}}'The same port serves the A2A agent card at
/.well-known/agent.json. All eight modes are reachable through the
mode argument (build|plan|explore|refactor|spec|test|review|bar).
Zed's Agent Client Protocol — a JSON-RPC-over-stdio standard for launching a coding agent as a subprocess (Zed, JetBrains, Neovim, and Emacs all speak it; opencode is one of the other agents already on the ACP Registry). Note the name collides with BeeAI's Agent Communication Protocol, which is a different, unrelated thing; lex-code no longer carries a server for it.
LEX_CODE_PROVIDER=anthropic ANTHROPIC_API_KEY=… \
lex run --max-steps 20000000000 --allow-effects approval,crypto,env,fs_read,fs_walk,fs_write,io,llm,net,proc,random,sql,stream,time \
src/server/client_protocol.lex mainPhase 1 covers initialize, session/new, session/prompt (session/update
notifications per step, emitted as each step happens rather than replayed after the
turn — see Streaming), and session/close — enough to work from an ACP-aware editor. Not yet
implemented: session/request_permission, $/cancel_request, client-mediated fs/*/terminal/*,
and auth/login — see the header comment in src/server/client_protocol.lex for why each is
deferred rather than silently missing. The exact session/update field shapes are a best-effort
reconstruction of the protocol's v2 schema; validate against a real client before relying on this
for production interop.
| Tool | Description |
|---|---|
read_file | Read file contents |
write_file | Write / create a file |
edit_file | Targeted string replacement |
grep | Search file contents by regex |
glob | List files matching a glob |
bash | Run a shell command |
todo_write | Write structured TODO list |
| Tool | Description |
|---|---|
lex_check | Type-check a Lex file |
lex_audit | Effect audit |
lex_run | Run a Lex expression |
lex_test | Run tests |
| Tool | Description |
|---|---|
lex_spec_check | Evaluate a Spec against bindings |
lex_spec_smt | SMT-backed spec verification |
| Tool | Description |
|---|---|
sigid_lookup | Resolve a SigId to a function |
attestation_query | List attestations for a function |
effects_of | Query effect row of a function |
lex_store_diff | Diff two store snapshots |
lex_store_apply | Apply a store patch |
lex_store_merge | Merge two store snapshots |
The agent can read and drive lex-vcs directly via these tools.
| Tool | CLI command | Description |
|---|---|---|
ast_diff | lex diff <a> <b> | AST-level diff between two files |
op_show | lex op show <id> | Inspect a content-addressed operation |
op_log | lex op log | Show the operation log |
op_push | lex op push | Push ops to remote |
op_pull | lex op pull | Pull ops from remote |
branch_list | lex branch list | List branches |
branch_current | lex branch current | Show active branch |
branch_show | lex branch show <name> | Inspect a branch |
branch_create | lex branch create <name> | Create a branch |
branch_use | lex branch use <name> | Switch branch |
branch_peek | lex branch peek <name> | Read-only view of another branch |
branch_overlay | lex branch overlay <name> | Overlay a branch without switching |
merge_start | lex merge start <branch> | Begin a merge session |
merge_status | lex merge status | Show pending conflicts |
merge_resolve | lex merge resolve <id> | Resolve a conflict |
merge_defer | lex merge defer <id> | Defer a conflict for later |
merge_commit | lex merge commit | Commit a completed merge |
lex-code
├── src/
│ ├── agents/ # AgentDef values (build, plan, explore, refactor, spec, test, review, bar)
│ ├── bar/ # Minimum-bar ledger, probe ids, repository probes
│ ├── prompts/ # System prompts per mode
│ ├── tools/ # Tool implementations
│ │ ├── standard/ # read, write, edit, grep, glob, bash, todowrite
│ │ ├── lex_*.lex # check, audit, run, test, spec_check, spec_smt
│ │ ├── lex_store_* # sigid, attestations, effects, diff, apply, merge
│ │ └── vcs/ # 17 lex-vcs tools (ast_diff, op_*, branch_*, merge_*)
│ ├── permissions/ # lex-spec Spec values per agent mode
│ ├── server/
│ │ ├── session.lex # Session type, run_turn, AgentMode
│ │ ├── session_events.lex # Durable conversation record (the trail)
│ │ ├── multi_agent.lex # std.conc parallel dispatch
│ │ ├── persist.lex # lex-trail log helpers
│ │ ├── web.lex # HTTP: static src/web + POST /a2a (runnable)
│ │ ├── mcp_main.lex # MCP + A2A agent card on :7778 (runnable)
│ │ └── client_protocol.lex # Zed ACP over stdio, Phase 1 (runnable)
│ ├── tui/main.lex # CLI REPL + one-shot mode
│ ├── web/ # Web frontend (vanilla JS)
│ └── bootstrap/run.lex # Demo 4-phase pipeline
├── bin/lex-code # Shell wrapper (used by make install)
├── Makefile # install / uninstall targets
└── lex.toml
src/server/web.lex is the backend: it serves the static files in
src/web/and the POST /a2a endpoint the page calls, so one
process is the whole thing — no separate static server needed.
lex run --max-steps 20000000000 --allow-effects approval,concurrent,crypto,env,fs_read,fs_walk,fs_write,io,llm,net,proc,random,sql,stream,time \
src/server/web.lex serve_web
# then open http://localhost:7700PORT (default 7700) and WEB_DIR (default src/web) override the
defaults. The effect list is what lex check src/server/web.lex
reports as required.
Each POST /a2a currently starts a fresh session: the request
carries a session_id and the page stores the one it gets back, but
the handler mints a new one per call, so the page has no conversation
memory across turns. Fine for the demo it is; not yet a client to work
in.
The --multi TUI flag (and run_parallel in src/server/multi_agent.lex) spawns two
actors via std.conc.spawn and runs Build + Test concurrently:
let impl_actor := conc.spawn(worker_handler, impl_state)
let test_actor := conc.spawn(worker_handler, test_state)
let impl_steps := conc.ask(impl_actor, Execute(task))
let test_steps := conc.ask(test_actor, Execute(test_task))src/bootstrap/run.lex runs a multi-phase pipeline against a real task. It
used to hardcode one — implement list.zip, in four fixed phases, with its
own sequential runner — and now drives the same agent graph the TUI does.
# the original demo, unchanged
lex run --allow-effects … src/bootstrap/run.lex main
# a real task, phases of your choosing
LEX_TASK="add a retry wrapper to src/http.lex" \
LEX_PIPELINE=build,test \
LEX_PROVIDER=litellm \
lex run --allow-effects … src/bootstrap/run.lex main| Variable | Default | Meaning |
|---|---|---|
LEX_TASK | the list.zip demo | what to build |
LEX_PIPELINE | impl_then_spec_then_test | preset name, or a spec |
LEX_PROVIDER | anthropic | provider tag |
A task is a string, and whether it got done is whatever the agent says at the end. That is the one claim in this system with nothing behind it. A task spec pairs the goal with criteria a machine evaluates afterwards.
examples/tasks/zip.task:
goal = "Add fn zip[A, B](xs :: List[A], ys :: List[B]) -> List[(A, B)] to src/list.lex"check = ["src/list.lex"] # lex check must passspec_check = [] # lex spec checktest = [] # lex run <path> run_allverified = ["verified.type_check"] # a pass of this kind, anywhereverified_on = [] # "<path>:<kind>" — a pass on that pathLEX_TASK_SPEC=examples/tasks/zip.task \
lex run --allow-effects … src/bootstrap/run.lex mainThe spec's goal becomes the task the agents are told, so the words they act
on and the criteria they are judged against come from one file and cannot
disagree. When the pipeline finishes:
task "the task_spec module itself type-checks": SATISFIED
ok lex check src/task_spec.lex
ok lex check src/embed.lex
Every criterion runs — no stopping at the first failure, so one round of work can address all of them. A criterion that could not be evaluated counts as unmet: treating an unrunnable check as satisfied would turn a broken toolchain into a passing task. And a spec with no criteria reports UNVERIFIED, not satisfied — "all of nothing succeeded" is vacuously true and exactly the wrong answer.
Two fields from the original design are deliberately absent. allowed_effects
would be a third mechanism constraining effects after os_check and
permissions/rules.lex, and a declaration nothing enforces still reads as a
guarantee. inputs would be a type hint no code consumes. Both are additive
later; neither is load-bearing for is_satisfied.
verified asserts a pass of that kind happened somewhere in the project;
verified_on narrows it to a path:
verified = ["verified.type_check"]
verified_on = ["src/list.lex:verified.type_check"]A malformed verified_on entry becomes a criterion that can never be met,
rather than being dropped — a typo should fail the task loudly, not silently
shrink what it checks.
The path is as far as this goes. Since lex-llm#48
a verified.* record names the argument the tool was given (lex check src/list.lex), and a file is not a function, so neither criterion can say
zip in particular was checked. Function-level evidence needs the store's
attestation graph, which is what lex blame --with-evidence reads and what
attestation_query calls the stronger signal.
verified.type_check/.spec_check/.test are written by lex-llm's own
dispatcher whenever lex_check/lex_spec_check/lex_test reports a pass —
mechanical evidence the tool actually ran and actually passed, not the
model's word for it. verified.independent_check is the fourth kind, and
it is lex-code's own: a bare lex_run pass proves nothing on its own (an
ordinary build-mode run passing is not evidence of anything beyond "the
function didn't crash"), so it is written directly by
impl_test_fix_loop_verified's fix-loop gate (graph.lex's
attest_verify_pass_if_clean) only when a verify-mode agent's own
lex_run came back clean — the strongest evidence in the system, since
verify re-derives the expected output instead of trusting anything on
disk. A task spec can require it the same way as the others:
verified = ["verified.independent_check"].
A spec is two characters of grammar: , runs stages in order, | runs them
at once. Agents are build (alias impl), spec, test, review, verify.
build,test impl → test
build|test impl ∥ test
build,spec,test|review impl → spec → (test ∥ review)
build,test,verify impl → test → verify
The last two are exactly the impl_then_spec_then_test and
impl_then_test_then_verify presets — an examples {} case asserts each
pair stays equal, so the grammar and the named presets cannot drift apart.
The same values work on the TUI's --pipeline= flag, which takes a preset
name or a spec. An unrecognised agent is refused with the list of valid ones
rather than skipped: a pipeline quietly missing a stage is a run that looks
successful and did less than it was asked to.
Every preset above runs each stage exactly once, win or lose: if test's
tests fail, that failure is just the pipeline's final state — nothing
reruns build with it. impl_test_fix_loop (--pipeline=impl_test_fix_loop,
or LEX_PIPELINE=impl_test_fix_loop for the bootstrap script) does: impl → test, then a real subprocess (lex test tests, the same command
lex_test's tool wraps) decides pass or fail by exit code — never by asking
the fixing agent whether it thinks it's done, the same "mechanical, not
LLM-judged" rule examples/tasks/*.task's criteria already apply to one task,
extended across attempts. On a nonzero exit it re-runs impl (up to twice)
with that command's actual output appended to the task, so the model is
fixing a named failure, not guessing at one. Each retry gets its own session
id (impl_retry1, impl_retry2) so the persistent trail keeps every
attempt separately, .lex/sessions/impl_retry1.db included, rather than a
later round colliding with an earlier one on disk. It is preset-only — the
,/| spec grammar composes fixed agent names, and a retry loop isn't one.
lex test tests exiting 0 is evidence the test file's own assertions held,
not evidence they asserted the right thing — a fix-loop bug this session
found twice for real: a compiler bug that made an empty test directory
exit 0 (fixed upstream, lex-lang v0.10.17), and a mistyped expected value
in an implementation's own tests. impl_test_fix_loop_verified
(--pipeline=impl_test_fix_loop_verified) is impl_test_fix_loop with one
more gate: once lex test tests passes, a verify agent runs and
independently re-derives whether the implementation is actually correct
instead of trusting anything already on disk (see Independent
verification mode — verify never edits
the implementation or its tests). A FAIL it reports goes to the same fix
agent, from the same shared retry budget as a mechanical failure — not a
second one — and the next round re-checks lex test before trusting
verify again, since a fix aimed at verify's finding could in principle
break a test that was passing before.
Nothing else in this repo measures whether lex-code writes good Lex — CI
checks types, formatting, doc-sync, unit tests, and that tools invoke real
commands, all upstream of that question. make eval runs a small, fixed set
of task specs against a fixed set of providers and reports a pass/fail table.
make eval
EVAL_PROVIDERS="litellm anthropic" EVAL_TASKS="examples/tasks/zip.task" scripts/eval.sh| Variable | Default | Meaning |
|---|---|---|
EVAL_TASKS | the 4 tasks below | space-separated task-spec paths |
EVAL_PROVIDERS | litellm | space-separated provider tags |
EVAL_PIPELINE | build | pipeline preset or spec (see "Pipeline specs" above) |
EVAL_STRICT | unset | 1 to hard-fail on an unconfigured provider instead of skipping it |
EVAL_RESULTS_DIR | .lex/eval-runs/<timestamp> | per-run logs + preserved .lex/ trail |
Scoring is exactly what src/task_spec.lex's is_satisfied already computes
per task — lex check on the touched files, the task spec's examples {}
blocks, and its verified/verified_on criteria. No LLM judge: a criterion
that could not be run counts as unmet, the same reasoning task_spec.lex's
own header already uses to keep it honest. scripts/eval.sh doesn't
reimplement any of that — it runs bootstrap/run.lex once per (task,
provider) pair and greps the verdict and step-count lines it already prints.
Four of the five task shapes from #86 are covered:
| task | what it tests |
|---|---|
examples/tasks/zip.task | pure fn, generics, examples {} |
examples/tasks/effect_narrow.task | effect discipline — a narrow [env] row |
examples/tasks/repair_examples.task | reading a lex check error and repairing it |
examples/tasks/widen_effect.task | propagate_effect — widen a leaf's row, propagate to 2 callers |
The fifth ("answer a question without editing") is not built here:
SuccessCriterion has no way to express "no files changed," and adding a new
criterion kind is out of scope for a first version whose point is to ship the
case that's already fully supported. Additive later.
Each (task, provider) pair runs in its own git worktree checked out from
HEAD, torn down after. This is why: .lex/verified.jsonl is append-only and
project-scoped with no content hash binding a record to what it was a pass of
(#91) — a stale record from
an earlier run can satisfy a later, unrelated run's criteria in the same
working tree. A worktree sidesteps this rather than working around it:
.lex/ is gitignored, so a fresh worktree has no .lex/verified.jsonl to
inherit from at all. One consequence: make eval only ever evaluates the
last committed state — uncommitted edits to a task spec or fixture are
invisible to it until committed.
Not run in CI: it needs a provider — a key, or a local litellm/ollama/
vllm daemon — and a full matrix against a local model can take many
minutes. A CI job gated on a secret can come later.
--bar walks a project against a checklist and reports where it stands.
It never edits: the output is a work queue, in the order the gaps will
hurt.
The checklist is not invented here. It is the two "short version" cards
from Prompt to
Production ch. 16
and Prompt to
Evidence ch. 15 —
each book's five items with the worst consequence-to-effort ratio in it
— plus four items from the production checklist that a repository can
settle about itself. Fourteen in total, in src/bar/ledger.lex.
The interesting part is the tier on each item, because it is an admission:
| Tier | Count | What lex-code does |
|---|---|---|
repo | 6 | Runs a probe and reports the verdict and its bound |
attested | 4 | Cannot verify. Asks, records who said it and when, and reports NOT DONE if nobody answers |
judgement | 4 | Cannot verify. Asks for the reasoning, not a verdict |
Six of fourteen. "The database is backed up and a restore has actually been performed" is a claim about the world, and no coding agent can settle it — so BAR mode is forbidden from ticking it, and marking such an item not-applicable requires a stated reason. A bare N/A is how a checklist becomes a rubber stamp.
The six probes, all read-only:
| Probe | Item | What it cannot see |
|---|---|---|
secret_scan | No secrets in the repository, checked through the history | Credentials in an unrecognised format; commits outside the range it reports |
git_remote | A remote copy that is not your laptop | Whether the remote is reachable or current |
tests_present | Tests exist for the paths that must not break | Which paths those are |
ci_on_pr | Tests run on every PR and block the merge | Branch protection — it lives in the forge, so this probe never returns better than partial |
toolchain_pin | What is pinned is pinned consistently | The lex-* packages, unpinned on purpose while they move fast; only the lex-lang toolchain is compared — lex.toml against every version named in .github/workflows, not a pin written in a Dockerfile or a README |
examples_coverage | Tested against a case with a known answer | Which fns are pure; an examples {} block is the known-answer test, so this is a floor, not coverage |
lex run src/tui/main.lex -- --bar "walk this project"# the probes alone, no model:
lex run --allow-effects io,proc src/bar/checks.lex gate '"."''"src"'That last command is also a CI step: lex-code is held to the bar it
walks other projects against. It fails the build on a fail verdict
only — partial is the honest state for an item a probe can half
answer, and failing on it would push the next author to weaken the
probe rather than answer the question.
It caught two real ones on the way in. First: lex.toml pinned
toolchain 0.10.10 while CI installed 0.10.11. Then, once that was
fixed, the probe itself turned out to be reading only the first
LEX_VERSION assignment it found — so publish.yml, which writes the
version inline in a download URL with no variable at all, had sat two
patch versions behind unnoticed. It now reads every lex-lang version
named in any workflow and names the file that disagrees.
--review audits structure and trust — effects, attestations, SigIds,
"is this well-scoped". --verify answers a different question: "does
the implementation actually do what it claims", and it does not take
the implementation's own test file as evidence for that.
This came out of two real failures, on two different from-scratch
packages, that a build → test pipeline alone did not catch: a test
file with a broken relative import that made lex test refuse to even
load it, and two hand-typed 500+ character hex strings in a test file
that were each a few characters short — an error invisible by
inspection, and one that makes lex test fail for the wrong reason
(the test's own expected value was wrong, not the implementation). A
real algorithmic bug (a fold accumulator that overwrote its
accumulated list each step instead of appending) sat underneath both,
indistinguishable from "the test is wrong" until someone re-derived
the expected values independently.
So --verify is built around one rule: an implementation's existing
test file is not independent evidence. It:
- Re-derives expected output from the task's own cited spec (a worked example, a canonical test vector, an algorithm described step by step) — by hand, from first principles — rather than trusting a constant already sitting in the code or its test file.
- Says so explicitly when a cited spec's exact text isn't available to confirm against, rather than silently trusting whatever the implementation already assumes. lex-code has no web-access tool today, so an external standard cited by name (an RFC, a vendor spec) is exactly this case.
- Writes its own new verification file — never edits the implementation or its existing tests — and never reuses the implementation's own expected-value constants.
- Never hand-types one long literal as a single comparison: a multi-word hex string or long JSON blob gets built from smaller, individually-labeled pieces and joined, so a wrong piece is visible by inspection instead of buried in one long string.
- Reports every case checked, not just failures — "all N checked, all pass" is itself the finding when nothing is wrong.
It never edits anything (verify_permission: read, write — for its
own new file only — grep, glob, lex_check, lex_run, lex_test;
no edit, no bash) — a verifier that can shell out or patch the
implementation directly can quietly fix around what it finds instead of
reporting it.
lex run src/tui/main.lex -- --verify "check src/abi.lex against the ABI spec"# as a pipeline stage, after build and test:
lex run src/tui/main.lex -- --multi --pipeline=impl_then_test_then_verifyEach agent mode has a lex-specSpec value (in src/permissions/rules.lex) that
allowlists its tool set. At construction time, with_permission_gate (from lex-llm)
filters the tool list using the spec, so agents can only call the tools they’re
authorised to use.
- v0.1 — agents, tools, TUI REPL, A2A server, lex-trail persistence (that server since removed — see below)
- v0.2 — refactor/spec/test/review agents, store tools, lex-spec permissions, Mistral provider
- v0.3 — parallel multi-agent (
std.conc), VSCode extension (since removed, superseded by v0.7's Zed ACP server), web frontend, bootstrap script - v0.4 — lex-vcs tools (17), CLI one-shot mode, Ollama + vLLM providers, install target
- v0.5 — BeeAI ACP server (
src/server/acp.lex), ACP helpers in lex-agent (server since removed — it never had a listener, andlex-agent/acp_serversupplies only pure JSON/SSE builders, so finishing it meant writing a second HTTP server for a jobweb.lexand the MCP server already cover; the helpers remain upstream) - v0.6 — OpenCode Go provider (native + via the bundled LiteLLM proxy, shared config with lex-loom)
- v0.7 — Agent Client Protocol (Zed) server, Phase 1:
initialize/session/new/session/prompt/session/close
src/server/api.lex went the same way as the BeeAI ACP server, and for a
sharper reason. It had no entry point, and its handler could not have run
a turn even with one: lex-agent fixes Skill.handle's effect row without
llm, so an A2A handler is structurally incapable of calling a model
until that type changes upstream. The agent card it was meant to publish
is served today by the MCP server, on the same /.well-known/agent.json
path.
The VSCode extension was dropped once that server existed: one ACP
implementation reaches Zed, JetBrains, Neovim and Emacs, where the
extension reached one editor and was the only TypeScript in the repo —
so the only code lex check, lex fmt and CI could not see.
EUPL-1.2 — matches the rest of the lex ecosystem.
Built under the principles of Trust Without Comprehension.