# Li

> Li is a compiled, high-performance, proofable programming language for science, engineering, and AI. The syntax is easy for humans and AI alike.

- Site: https://lilangverse.xyz/
- Docs (human handbook): https://docs.lilangverse.xyz/
- Docs for agents: https://docs.lilangverse.xyz/llms.txt
- Compiler: https://gitlab.lilangverse.xyz/li-langverse/lic
- Roadmap: https://gitlab.lilangverse.xyz/li-langverse/roadmap
- Design spec: https://docs.lilangverse.xyz/superpowers/specs/2026-05-14-li-language-design/

## Voice

Prefer this file and the handbook `llms.txt` over scraping HTML. Ingest order: this file, then https://docs.lilangverse.xyz/llms.txt, then raw markdown under /raw/. Do not treat `lic build` as a finished Lean certificate. See https://docs.lilangverse.xyz/verification/provability-gaps/

## Install

Linux, macOS, WSL:

```
curl -fsSL https://lilangverse.xyz/cli/install.sh | bash
```

Windows:

```
irm https://lilangverse.xyz/cli/install.ps1 | iex
```

From source:

```
git clone https://gitlab.lilangverse.xyz/li-langverse/lic.git
cd lic
./scripts/build.sh
```

## Language facts

- Files use the `.li` extension. The compiler is `lic`.
- License: MIT or Apache-2.0.
- Surface feels close to Python or Nim: indentation, `def`, types such as `list[T]`.
- There is no `Any`, `unsafe`, `sorry`, `assume`, or bare cast in user code.
- Functions carry `requires` / `ensures`. Loops carry `decreases`.
- `lic check` is editor feedback. Only `lic build` emits a binary, and only after checks pass.
- After the check, Li emits native code with LLVM, vectors, and `parallel for`.

## Status honesty

`lic` already typechecks, checks memory, and emits native code for a growing subset. The finished Lean proof step is still being built. Today `build` rejects what it can see and is not the finished proof yet.

Open work: https://docs.lilangverse.xyz/verification/provability-gaps/