For agents

Using Brine with coding agents

Brine is designed to be written by coding agents as well as people. The loop is short: edit, run brine check --json, fix what it reports, run brine test. Every error has a stable code, an exact location, the reason, and how to fix it, and the compiler catches the mistakes that are hardest to find by reading code: data races, deadlocks, and broken contracts.

Why Brine suits agents

The design doc lists these principles for agent usability:

Stable error codes. Every error has a code (E0501), a primary span, a “why” and a “how to fix”. Codes are stable, so an agent can look them up and learn them.
Machine-applicable fixes. In --json output, many errors carry a fixes array of exact text replacements. See Machine-readable output.
Deterministic output. The same input gives the same diagnostics in the same order, so runs can be compared and cached.
No configuration for anything common. brine guide and an AGENTS.md in every project give an agent what it needs to start.
Syntax models already know. Brine looks like Python, minus the parts that cause bugs. When an agent writes Python or C habits (def, else if, &&, x++), the compiler names the Brine spelling, often with a fix.

The language’s rules help too. A mistake that would be a silent bug elsewhere is a compile error in Brine: a data race in a parallel loop (E0501), a collective call that could deadlock (E0510), a precondition a caller can’t guarantee (E0601). Runtime checks for bounds, overflow and division by zero can’t be turned off, so a wrong index stops the program with a location instead of corrupting memory.

The loop

Edit the code.
Run brine check --json. It type-checks and runs the prover without building, so it’s fast. Each problem is one JSON object on its own line.
Fix each error. Apply its fixes if it has any; otherwise read help, or run brine explain <code>.
Repeat until brine check prints {"ok":true,...}.
Run brine test --json: one object per test, with its output if it failed.
Run brine fmt before committing.

brine check --json        # after every edit
brine test --json         # when it compiles
brine fmt                 # before committing

brine check exits with status 0 when the code compiles and 1 when it doesn’t, so a script can loop on the exit code alone. See Machine-readable output for every object shape and exit code.

brine guide

brine guide prints the whole language on one page: syntax, types, built-ins, par, world, contracts and the CLI, with examples. It’s about 500 lines, small enough to read into context once at the start of a task.

brine guide

# brine quick reference

brine is a compiled, verified, natively parallel language with Python-like syntax.
Blocks use `:` plus 4-space indentation. Comments start with `#`.
...

It’s the same text as the quick reference, and it always matches the installed compiler.

brine explain

Every error ends with run brine explain <code> for more about this error. The explanation says why the rule exists and shows the usual fixes:

brine explain E0501

E0501: writing shared state in `par`

Iterations of `par` code run at the same time. To rule out data races, a
`par` body may not assign variables from outside it, call functions that
mutate them, or push/pop them. The one exception: in `par for i in ...`,
arrays from outside may be written at index `i`:

    var out = [0.0] * n
    par for i in 0..n:
        out[i] = f(i)        # OK: each iteration writes its own slot

To combine results, use a reduction instead: `par sum(f(i) for i in 0..n)`.

brine explain with no code lists every code and its title. Both forms take --json. The same explanations are on the error codes page.

AGENTS.md in every project

brine new and brine init write an AGENTS.md into the project. It lists the commands and the rules that most often trip up a model that knows Python: let and var, explicit conversions, ref, proofs, par for writes, map keys, negative indexes, string bytes. Many agents read AGENTS.md automatically. See AGENTS.md and common mistakes for the full text and an example of each rule.

These docs, for agents

Every page of this site is also plain Markdown:

Add .md to any URL. https://docs.brinelang.org/proofs/contracts/ is also https://docs.brinelang.org/proofs/contracts.md. Code blocks, tabs and notes come through as Markdown.
Copy page. The button under each page title copies that page’s Markdown. “View as Markdown” opens it, and “Ask Claude” and “Ask ChatGPT” start a chat that reads it.
/llms.txt is an index of the site for language models, following the llms.txt convention, with the key facts for writing brine at the top.
/llms-full.txt is the whole site in one file.
/llms-small.txt is the same with non-essential content removed, for smaller context windows.
One topic at a time: /_llms-txt/language.txt, /_llms-txt/parallelism.txt and /_llms-txt/proofs.txt hold one section of the docs each.

Add brine to your agent’s instructions

Paste this into your agent’s instructions (AGENTS.md, CLAUDE.md, a Cursor rule, or a system prompt) when it works on brine code outside a project made by brine new:

## brine

This project uses brine, a compiled language with Python-like syntax,
compile-time proofs and race-free `par` parallelism. It is not Python.

- Read `brine guide` once before writing brine. Docs: https://docs.brinelang.org
  (add `.md` to any page URL for Markdown; https://docs.brinelang.org/llms.txt
  is an index).
- After every edit run `brine check --json` and fix every diagnostic. Apply the
  `fixes` array when present. `brine explain <CODE>` explains any error code.
- Run `brine test --json` before finishing, and `brine fmt` before committing.
- Common mistakes: `let` is immutable and `var` is mutable, with no shadowing;
  no implicit numeric conversions (`float(i)`); integer `/` rounds down;
  arguments are copies, so a function that changes the caller's variable takes
  `ref x: T` and is called as `f(ref x)`; no negative indexes; strings index by
  bytes; `m[k]` panics on a missing key (use `k in m` or `m.get(k)`); `match`
  must cover every case; failures are `Result`/`Option` with `?`, not
  exceptions; `elif`, not `else if`.
- `requires`, `ensures` and `invariant` must be proven at compile time. If the
  prover can't, add a `requires`, an `invariant`, or an `assert`.
- Inside `par for i in ...:` only `out[i]` of outer arrays may be written; use
  `par sum(...)` or `par [...]` to combine results.