Showcase  /  Formal proof

A proof that a part of the prompt never goes over its token limit

A model can read only so many tokens at once. If a prompt is one token too long, the request fails. So when you tell Affordance that some part of the prompt may use at most 1,500 tokens, it matters that 1,501 can never come out. We proved that it cannot.

What a limit is

In Affordance you can put any part of the prompt in a box and give the box a limit, for example the output of a command or the history of a conversation. A token is a piece of text about three quarters of a word long.

Output {
  max-tokens: 1500tok;
  overflow: clip-middle;
}

When the content is longer than the limit, the box has to cut. It can keep the start, the end or both ends, drop whole items, or scroll, and it can add a marker that says how much is hidden. There are eight ways of cutting, and each has its own arithmetic. An off-by-one mistake in any of them would put a prompt over its limit.

Tested, and also proved

A test tries some inputs and checks the result. It cannot try every input. A proof checker reads the code and shows that a statement holds for all inputs, or it fails and says where.

We used Verus, a proof checker for Rust, the language Affordance is written in. The statement it checks is short: if a box has a limit, the number of tokens it produces is at most that limit. It holds for any content, any limit, any marker, and all eight ways of cutting.

Verus checks the same file that Affordance runs, src/fit.rs. There is no separate copy written for the proof that could drift away from the real code.

Checking the checker

A proof that passes could be passing because it says nothing. So we broke the code on purpose, five times, one mistake at a time. One version kept one token too many when cutting. Another forgot to leave room for the marker. Verus rejected all five.

The verification page in the docs has the exact statements and what each one assumes.