# Li

> A compiled language for science and simulation. You write ordinary code,
> then you write what has to stay true. If that does not hold, Li will not
> give you a program. HTML: https://docs.lilangverse.xyz/ — fetch Markdown from /raw/.

Full text: https://docs.lilangverse.xyz/llms-full.txt
This index: https://docs.lilangverse.xyz/llms.txt
Source: https://gitlab.lilangverse.xyz/li-langverse/lic-docs

## Start here

- [For agents and chats](https://docs.lilangverse.xyz/raw/for-agents.md): How agents and chats should fetch this handbook.
- [Getting started](https://docs.lilangverse.xyz/raw/getting-started.md): What Li is, and the first commands.
- [Hello world](https://docs.lilangverse.xyz/raw/guide/hello-world.md): A first program with requires / ensures / decreases.
- [Getting started — tools](https://docs.lilangverse.xyz/raw/guide/getting-started-tools.md): Install lic and the toolchain.
- [Provability gaps (current compiler)](https://docs.lilangverse.xyz/raw/verification/provability-gaps.md): Honest today-vs-target register. Read before claiming proofs.

## Language

- [Language handbook — overview](https://docs.lilangverse.xyz/raw/language/overview.md): Handbook map: types, numbers, SIMD, contracts.
- [Li language philosophy — simplicity and readable code](https://docs.lilangverse.xyz/raw/language/philosophy.md): Why Li is written the way it is.
- [Types and data](https://docs.lilangverse.xyz/raw/language/types-and-data.md): Types and data. No Any.
- [Contracts and proofs](https://docs.lilangverse.xyz/raw/language/contracts-and-proofs.md): requires, ensures, decreases.
- [Numerics](https://docs.lilangverse.xyz/raw/language/numerics.md): Numbers and numeric policy.
- [SIMD and parallel execution](https://docs.lilangverse.xyz/raw/language/simd-parallel.md): Vectors and parallel for.
- [`li.toml` manifest](https://docs.lilangverse.xyz/raw/language/li-toml.md): The package manifest.
- [Math-first HPC examples](https://docs.lilangverse.xyz/raw/guide/math-hpc-examples.md): Math-first examples for HPC.
- [Examples gallery](https://docs.lilangverse.xyz/raw/guide/examples-gallery.md): Copy-paste examples.

## Compiler and proof

- [Why Li is mathematically provable](https://docs.lilangverse.xyz/raw/compiler/why-provable.md): Why the compiler refuses unproved programs.
- [How `lic build` works](https://docs.lilangverse.xyz/raw/compiler/build-pipeline.md): How a file becomes a binary.
- [Formal verification in Li](https://docs.lilangverse.xyz/raw/verification/overview.md): Verification surface.
- [Tests and quality gates](https://docs.lilangverse.xyz/raw/testing/overview.md): Test suites and CI.

## Agents

- [Agent handover formats](https://docs.lilangverse.xyz/raw/ecosystem/agent-handover-formats.md): How agents should discover tools and errors.
- [Agent-kit adoption (lip / lit / lis)](https://docs.lilangverse.xyz/raw/ecosystem/ADOPTION.md): Agent-kit adoption.
- [Overview](https://docs.lilangverse.xyz/raw/ecosystem/overview.md): Packages, lip, governance.

## Optional

- [Documentation style guide](https://docs.lilangverse.xyz/raw/contributing/documentation.md): How to write handbook pages.
- [Li Language Design Spec](https://docs.lilangverse.xyz/raw/superpowers/specs/2026-05-14-li-language-design.md): Normative language design.
- [Li Master Implementation Plan (rev. 5)](https://docs.lilangverse.xyz/raw/superpowers/plans/2026-05-14-li-master-plan.md): Phase tracker.
- [Benchmarks](https://docs.lilangverse.xyz/raw/benchmarks.md): Benchmark notes.

## Also

- [Agent manifest (TOML)](https://docs.lilangverse.xyz/raw/ecosystem/li-agent-manifest.toml): commands agents should run.
- [Diagnostic schema](https://docs.lilangverse.xyz/schemas/diagnostic-v1.json): `lic check --format=json` / `lic diagnose`.