# 22. Alice for AI agents

> Chapter 22: how AI coding agents learn Alice with alice guide, what alice agents --write puts in AGENTS.md and why, the edit-check-prove loop, and a change by an agent that alice prove --check stops with a counterexample.

Canonical: https://alice-lang.org/documentation/learn/agents/

[Documentation index](https://alice-lang.org/documentation/llms.txt) · [Complete book](https://alice-lang.org/llms-full.txt)

More and more code is written with AI coding agents: tools that read a repository, edit files and run commands. They are fast, and they make a particular kind of mistake. They write code that *looks* right, often in the style of a more common language, and they can "simplify" something whose purpose they did not understand.

Alice was designed with this in mind. Its compiler rejects much of what looks plausible but is wrong, and its rules and proofs catch changes that compile but break a requirement. This chapter shows how to set up a project so that an agent works within those guard rails, and what the guard rails catch.

Everything here applies to human contributors too.

## 22.1 Teaching an agent Alice: `alice guide`

An agent knows Ruby and C# from its training data, but not Alice. The compiler prints a compact guide written for this purpose:

```sh
alice guide              # the language in one page
alice guide performance  # how to write code the compiler can optimize
alice guide proofs       # rules, alice prove, PROOF.al
alice guide interop      # .NET, C libraries, @[Native], safe
```

Every example in the guide compiles, and every rule in it says what the compiler enforces. It is short enough to read before each task. The guide ships with the compiler, so it always matches the installed version.

## 22.2 AGENTS.md: what `alice agents --write` adds

Many agents read a file named `AGENTS.md` at the root of a repository before they start. `alice new` creates one for every project, plus a `CLAUDE.md` that imports it. For an existing repository, run:

```sh
alice agents --write
```

```text
AGENTS.md: Alice block written (between the alice:start / alice:end markers); CLAUDE.md imports it
```

The command writes a block between two markers, `<!-- alice:start ... -->` and `<!-- alice:end -->`. Running it again replaces only that block, so your own notes outside the markers survive. `alice agents` without `--write` prints the block. Here it is in full, as Alice 0.14 prints it, followed by what each part is for.

```text
## Alice

This project is written in Alice (`.al` files), a .NET language with Ruby/Crystal-like syntax. It is not Ruby
and not Crystal: code that looks right in those languages often does not compile or behaves differently here.

Before writing Alice:

- Run `alice guide` and read it. Topics: `alice guide performance`, `alice guide proofs`, `alice guide interop`.
- Check your work with `alice check` (types only) and `alice run file.al`.
- Run `alice prove --check` before committing when the project has a `RULES.al`. If a rule fails, fix the code;
  change the rule only if the rule itself is wrong, and say so. Commit the regenerated `PROOF.al`.
- Run `alice explain file.al` after changing hot code: it lists the optimizations each method got.
```

**The opening paragraph** names the trap directly. An agent that sees `def`, `end` and blocks will assume Ruby. Saying "not Ruby" up front changes what it reaches for.

**"Before writing Alice"** is the loop: learn from the guide, check types with `alice check`, run, and prove before committing. The proof line also states the policy for failures: fix the code, change a rule only when the requirement changed, and say so. That sentence matters, because the easiest way for an agent to make a failing check pass is to weaken the check.

```text
### Not Ruby, not Crystal

| You may write (Ruby/Crystal habit) | In Alice |
|---|---|
| `xs << 1` / `xs.push(1)` on an array | `Array(T)` is a fixed-size .NET array. Use `List(T)` (`xs = List(Int32).new`, then `xs << 1`) |
| `h["missing"]` returns `nil` | raises `KeyNotFoundException`. Use `h.fetch(k, default)` or check `h.has_key?(k)` |
| `h[k] += 1` on a new key | raises. Initialise first: `h[k] = h.fetch(k, 0) + 1` |
| `s << "x"` on a String | strings are immutable .NET strings. Use `s += "x"`, interpolation, or `System.Text.StringBuilder` |
| big integers grow forever | `Int32`/`Int64` raise `OverflowException`. Use `Int64` or `&+ &- &*` (wrapping) on purpose |
| `Array<Int32>`, `Hash<K, V>` | generics use parentheses: `Array(Int32)`, `Hash(String, Int32)` |
| `require "json"` (a gem) | `require` loads `.al` files. Libraries are NuGet packages: `alice add <Package>`, then use the .NET API |
| `x.size` on a value that may be `nil` | compile error AL0310. Check `if x`, `x.nil?`, use `x || default`, or `x.not_nil!` |
| `x = risky rescue fallback` | no `rescue` modifier. Write `x = begin ... rescue e : Exception ... end` |
| `"a" < "b"` on strings | `<`/`>` are not defined on strings. Use `"a" <=> "b"` (returns -1, 0, 1) |
| `-7 / 2 == -3` (C#/Java habit) | integer `/` and `%` are floored, as in Ruby: `-7 / 2 == -4`, `-7 % 3 == 2` |
| monkey-patching hot paths, `method_missing`, `send` | they work but run through reflection. Prefer plain methods in performance-sensitive code |
| untyped `Any`/`Object` containers | they box and disable optimizations. Use typed arrays and collections |
```

**The table** lists the habits that compile in Ruby or Crystal but fail or behave differently in Alice. You met each of them in this book: fixed-size arrays and missing hash keys in [chapter 4](https://alice-lang.org/documentation/learn/collections.md), immutable strings in [chapter 5](https://alice-lang.org/documentation/learn/strings.md), overflow and floored division in [chapter 3](https://alice-lang.org/documentation/learn/common-concepts.md), nil checks in [chapter 2](https://alice-lang.org/documentation/learn/guessing-game.md). A table is the right shape for an agent: it matches on the left column and applies the right one.

Two rows are behind the 0.14 compiler. `Hash(String, Int32).new(0)` now gives a hash whose missing keys read as 0, so `h[k] += 1` works on such a hash (chapter 4); on a plain hash the row is still right. And the `rescue` modifier exists since 0.14: `x = (Int32.Parse(s) rescue 0)` compiles (chapter 8). The advice in those rows still produces correct code, only longer.

```text
### Writing Alice the compiler can optimize

- Hot data: arrays of numbers (`Array(Float64)`), allocated in the method that uses them. They become owned:
  pooled, no GC.
- Use `own`, `borrow`, `scope`, `pure`, `par` and `par for` to make the compiler prove what you intend. A
  failed proof is a compile error that explains why. Do not delete the keyword to silence the error.
- Divide and conquer as two independent calls to pure functions runs in parallel. So do loops whose
  iterations write only their own index.
- Do not hand-write threads, locks or `Parallel.For` for work the compiler can parallelize.
```

**The optimization section** steers toward code that [chapters 9 to 12](https://alice-lang.org/documentation/learn/ownership.md) showed the compiler can prove things about. The key line is "Do not delete the keyword to silence the error". An `own`, `pure` or `par for` is a contract; removing it makes an error go away and the guarantee with it.

```text
### Error codes you will meet

AL0201 non-exhaustive `case`, AL0202 data race, AL0203 `val` reassigned, AL0207 owned value escapes,
AL0208 use after move, AL0209 `par for` not independent, AL0210 not pure, AL0211 `par` cannot fork,
AL0212 `safe` reaches ambient authority, AL0213 borrow escapes, AL0214 rule domain too large, AL0310 maybe nil.
```

**The error codes** let an agent connect a compiler message to its meaning without searching. [Appendix B](https://alice-lang.org/documentation/learn/error-codes.md) has the full list.

## 22.3 Compiler errors as feedback

An agent works in a loop: edit, run a command, read the output, edit again. The quality of that output decides how fast the loop converges. Alice's errors are designed for it: a code, the exact place, and a `help:` line with the fix.

Suppose an agent is asked to speed up a sum and reaches for parallelism with a shared counter:

```alice fail="AL0202"
def total_cups(orders : Array(Int32)) : Int32
  total = 0
  Par.For(orders.size) { |i| total += orders[i] }
  total
end
```

```text title="Error"
error[AL0202]: data race: spawned task writes captured variable 'total'
help: send the value through a Channel(T), use an Actor, or return it from the task
```

In most languages this compiles and returns a wrong total now and then, the hardest kind of bug to notice in review. Here the agent gets an error and a fix. The idiomatic fix is even simpler: `orders.sum`, which the compiler already runs in parallel on large arrays.

## 22.4 A change that compiles and is still wrong

The compiler cannot know your business rules. That is what `RULES.al` is for. Here is a complete example of an agent's change that passes the type checker and the existing tests, and is caught by `alice prove --check`.

The tea shop gives 10 percent off from 10 cups:

```alice file="src/bulk.al"
def bulk_price(cups : Int32) : Int64
  base = cups.to_i64 * 250
  return base if cups < 10
  base - base / 10
end
```

The shop's requirements, as rules: a price is never negative, and buying one more cup never costs less than before. Customers would notice, and game the system:

```alice cmd="prove" target="." ignore="last-column"
rule price_never_negative(cups in 0..1000)
  bulk_price(cups) >= 0
end

rule one_more_cup_never_costs_less(cups in 0..1000)
  bulk_price(cups + 1) >= bulk_price(cups)
end
```

```text title="Output"
╭───────────────────────────────┬───────┬────────┬────╮
│ rule                          │ cases │ result │ ms │
├───────────────────────────────┼───────┼────────┼────┤
│ one_more_cup_never_costs_less │ 1,001 │ proven │  0 │
│ price_never_negative          │ 1,001 │ proven │  0 │
╰───────────────────────────────┴───────┴────────┴────╯
```

Both hold: 9 cups cost 22.50, and 10 cups cost 25.00 minus 2.50, also 22.50. `PROOF.al` is committed.

Now the task for the agent: "Make bulk orders more attractive: 20 percent off from 10 cups." The agent makes the obvious edit:

```alice file="src/bulk.al"
def bulk_price(cups : Int32) : Int64
  base = cups.to_i64 * 250
  return base if cups < 10
  base - base / 5
end
```

It compiles. The unit test for 12 cups is updated to the new price and passes. Then the agent runs the check its `AGENTS.md` asks for:

```alice cmd="prove --check" target="." exit="1" ignore="last-column"
rule price_never_negative(cups in 0..1000)
  bulk_price(cups) >= 0
end

rule one_more_cup_never_costs_less(cups in 0..1000)
  bulk_price(cups + 1) >= bulk_price(cups)
end
```

```text title="Output"
╭───────────────────────────────┬───────┬───────────────────┬────╮
│ rule                          │ cases │ result            │ ms │
├───────────────────────────────┼───────┼───────────────────┼────┤
│ one_more_cup_never_costs_less │ 1,001 │ fails at cups = 9 │  0 │
│ price_never_negative          │ 1,001 │ proven            │  0 │
╰───────────────────────────────┴───────┴───────────────────┴────╯
error: PROOF.al is missing or stale: the code or RULES.al changed since it was 
written; run `alice prove` and commit PROOF.al
```

The counterexample is exact: at 9 cups the price is 22.50, and at 10 cups it would be 25.00 minus 5.00, which is 20.00. A customer who wants 9 cups should order 10 and leave one. The agent's instructions say to fix the code, not the rule, so the agent goes back to the requirement. One fix that keeps both rules: never charge more for 10 or more cups than for 9 cups at full price, by phasing in the discount:

```alice file="src/bulk.al"
def bulk_price(cups : Int32) : Int64
  base = cups.to_i64 * 250
  return base if cups < 10
  Math.Max(base - base / 5, 9_i64 * 250)
end
```

```alice cmd="prove" target="." ignore="last-column"
rule price_never_negative(cups in 0..1000)
  bulk_price(cups) >= 0
end

rule one_more_cup_never_costs_less(cups in 0..1000)
  bulk_price(cups + 1) >= bulk_price(cups)
end
```

```text title="Output"
╭───────────────────────────────┬───────┬────────┬────╮
│ rule                          │ cases │ result │ ms │
├───────────────────────────────┼───────┼────────┼────┤
│ one_more_cup_never_costs_less │ 1,001 │ proven │  0 │
│ price_never_negative          │ 1,001 │ proven │  0 │
╰───────────────────────────────┴───────┴────────┴────╯
```

From 10 cups to 11, the price stays at 22.50, and from 12 cups on the 20 percent discount applies in full. The agent commits the code with the new `PROOF.al`, and the reviewer sees in the diff both what changed and that the rules still hold.

Notice what did the work. The tests checked the examples someone thought of. The rule checked all 1,001 cup counts, and the one that broke was at the edge nobody tested.

## 22.5 Wiring it in

Make the checks impossible to skip:

- **A pre-commit hook** in `.git/hooks/pre-commit`:

  ```sh
  #!/bin/sh
  set -e
  alice fmt --check
  alice check
  alice test
  alice prove --check
  ```

- **CI** runs the same commands, as in [chapter 21](https://alice-lang.org/documentation/learn/tooling.md#project-ci-for-the-tea-shop), so a change that skipped the hook is still stopped.

- **Review** looks at diffs of `RULES.al` with extra care. A changed rule is a changed requirement and should say why.

## 22.6 What this does not do

The guard rails are specific. Be clear about their reach:

- The compiler checks types, nil, races, purity, ownership and exhaustiveness. It does not know whether your program does what the customer wanted.
- Rules prove what they state, over the domains they state. A missing rule protects nothing, and a wrong rule proves the wrong thing.
- An agent can still write a correct but slow solution, or a confusing one. `alice explain` and human review remain part of the loop.

:::caution\[Common mistakes]

- **Letting an agent edit `RULES.al` to make a check pass.** That changes the requirement. Require a reason in the commit message, and review it.
- **Deleting `own`, `pure`, `par for` or `safe` to silence an error.** The error disappears and the guarantee with it.
- **Forgetting to commit `PROOF.al`.** `alice prove --check` then fails as stale on the next run.
- **Editing inside the `alice:start` / `alice:end` markers.** `alice agents --write` replaces that block. Put project notes outside it.
  :::

## Exercises

1. Add a rule to the bulk pricing example that the price for any number of cups is at most `cups * 250`. Does the final `bulk_price` keep it?
2. An agent removes `pure` from a function to fix `AL0210`. What should a reviewer ask?
3. Why is "fails at cups = 9" more useful to an agent than "a rule failed"?

<details>
<summary>Answers</summary>

1. Yes: the discount only ever lowers the price below the full price, and `Math.Max` with the 9-cup price is still below `cups * 250` from 10 cups on.

   ```alice cmd="prove" target="." ignore="last-column"
   rule never_more_than_full_price(cups in 0..1000)
     bulk_price(cups) <= cups.to_i64 * 250
   end
   ```

   ```text title="Output"
   ╭────────────────────────────┬───────┬────────┬────╮
   │ rule                       │ cases │ result │ ms │
   ├────────────────────────────┼───────┼────────┼────┤
   │ never_more_than_full_price │ 1,001 │ proven │  0 │
   ╰────────────────────────────┴───────┴────────┴────╯
   ```

2. What effect made it impure, and whether that effect belongs there. `pure` was a promise that the function can run in parallel and be tested in isolation. Removing it hides the new side effect instead of explaining it.

3. It is a concrete input to reproduce, test and reason about. The agent can compute `bulk_price(9)` and `bulk_price(10)`, see the jump, and fix the cause instead of guessing.

</details>

## Summary

- `alice guide` teaches the language in one compact page per topic, matched to the installed compiler.
- `alice agents --write` writes an Alice block into `AGENTS.md`: the workflow, the Ruby and Crystal habits to avoid, how to write optimizable code, and the error codes.
- Compiler errors carry a code, a location and a fix, which makes the agent's edit loop converge.
- `RULES.al` states requirements; `alice prove --check` stops a change that breaks one with an exact counterexample.
- Hooks and CI make the checks unavoidable; reviewers watch changes to rules.

That is the end of the main text. The appendices follow, starting with [keywords and operators](https://alice-lang.org/documentation/learn/keywords.md).

## Continue reading

- Previous: [21. Tooling](https://alice-lang.org/documentation/learn/tooling.md)
- Next: [Appendix A: Keywords and operators](https://alice-lang.org/documentation/learn/keywords.md)