ADR-264: An assert Is a Contract — Proved Where the Compiler Can, Checked Where It Cannot, and a Test Is a Block

Status: Superseded by ADR-269 — restated there with the same decision numbers, together with ADR-266 Amended by: ADR-266 — D5’s precondition is found by computing a claim back to the entry rather than by its line, and its three exclusions are lifted by a ledger contract and two entries Date: October 2, 2026 Answers: #190 (assert is on the prelude’s list and is not in std; whatever it is, it is decided with the testing chapter), and the owner’s question what happens to a claim the compiler cannot prove Displaces: Part III 14.2’s rule that an assertion is removed from a release build (D4), and Part III 14.1’s assert statement form (D2) Related: ADR-154 D1 (the prelude’s list), ADR-117 and ADR-124 (a reserved word needs a construct), Part I 2.2 and Part III A.2 (an overflow is unrecoverable at every build), ADR-010 D2 (data from outside the program), ADR-255 (a jump that carries its condition — the guard the prover reads most), ADR-244 (a promise is what the source wrote), ADR-258 (the four weights this is weighed by)

1. Question

When the compiler can neither prove nor refute an assert, does the program build — with the claim checked when it runs — or is it refused?

Everything else about assert and tests follows from the answer, which is why this record holds all of it: what a test is, what an assert is, what its condition may do, which claims the compiler proves, and what it reports.

The answer cannot default, for three reasons:

• A prover is a theory at a time. The one the compiler has reads linear arithmetic over whole numbers that do not change (D9). The claims a real program makes about its data — this list is not empty here, this state was set before this call, this index is inside that table — are fields, matches and calls, and none of them is in that theory, or will be soon. If an unproved claim is refused, those claims cannot be written at all, and what is written instead is a panic() that no prover will ever look at.
• The compiler’s own sources are the first large program to want them. Self-hosting moves the compiler into Nikaia a module at a time (ADR-250); the invariants the Rust modules state with unreachable! move with them. Each has to become something, and the only thing that keeps it a claim — something a later prover can discharge — is an assert that builds.
• Formal verification is a project of its own. Refusing what is not proved ties every program that wants to state an invariant to that project’s schedule. Checking what is not proved lets it arrive a theory at a time, each one removing checks and changing nothing a correct program does.

2. How others do it

Language / tool	Its answer	What it costs there	Source
Ada / SPARK	Pre, Post and pragma Assert are contracts; GNATprove proves what it can, and what it does not prove stays a run-time check under the assertion policy. A project may require all checks proved as a goal it reaches step by step	the proof is opt-in per unit, which is how large Ada code bases adopt it gradually	from memory, not checked
Dafny	every assertion is proved, or the program is not compiled	specification effort is the price of every line; loops need invariants by hand	from memory, not checked
Eiffel	require / ensure / check are checked at run time; which levels are on is a build setting	a contract can be switched off, so it is a test and not a promise	from memory, not checked
Rust	assert! is on in every profile, debug_assert! only in debug; nothing is proved	the check is always paid; the optimiser removes what it can see through	the reference, std::assert!
Zig	assert is checked in Debug and ReleaseSafe, and is undefined behaviour in ReleaseFast	the release build trades the claim for speed	from memory, not checked

What does not transfer: Dafny’s model needs a specification language and a solver the project does not have, and makes the solver’s reach the language’s reach. Eiffel’s and Zig’s build switch is what Part I 2.2 rules out for overflow, and would make an assert the one check a build removes. SPARK’s model is the one that fits — the claim means the same thing whether or not it is proved, and the proof only removes its cost.

3. Options, weighed

Option A — proved, or the program is refused

fn first(xs: Vec[i64]) -> i64 {
    assert(xs.len() > 0)       // refused: the caller's list is not readable
    return xs[0]
}

Option B — proved where the compiler can, checked where it cannot

fn first(xs: Vec[i64]) -> i64 {
    assert(xs.len() > 0)       // checked here today; proved at each call later
    return xs[0]
}

Option C — always checked at run time, nothing proved

The same source as B; a check is emitted for every claim, and a proof would never remove one.

Option D — B, and a build option removes the unproved checks

The same source as B; --release-fast leaves out what is not proved.

Weighed

	D1 the special case pays, not the common one	D2 the compiler works, not the developer	D3 no cost for the common case	D4 consistent with itself	If it is wrong
A	the common claim pays: an invariant outside the theory cannot be written	the developer works for the prover — reshapes code until it is readable, or writes panic()	nothing at run time	consistent, and narrow: a claim exists only where a theory does	programs written around the prover; undoing it accepts more, breaks nothing
B	the unproved claim pays one comparison, where it is reached	the compiler proves what it can and says which it could not (D7)	a proved claim costs nothing; the others cost what the program would have written as a panic	one meaning for every claim; Part I 2.2’s the check does not depend on a build option	a program can stop in production on a claim nobody proved — visible in D7, and a project can refuse it (§6)
C	every claim pays	nothing proved, nothing reported	every claim costs	consistent with overflow today	fixes the meaning at today’s implementation; a prover could never remove a check
D	as B	as B	the release build pays nothing	the one check a build removes, against Part I 2.2	a release build runs a program whose claim is false, silently

B wins on D2 and D4. A wins only D3, and only by refusing the programs whose claims it cannot read — the cost moves from the run to the developer, which is what D2 says the language does not do. C is B without the proof, and D is B with Part I 2.2 broken.

4. Decision

D1 — A test is a test "name" { … } block in the package it tests.

test "a blank line is counted" {
    let (lines, blank) = count("a\n\nb\n")
    assert(lines == 3)
    assert(blank == 1; message: "an empty line is blank")
}

• A test block stands where a fn may, in any file of the package, and sees what the package sees, private names included.
• It is compiled only by nikaia test; nikaia build and nikaia run leave it out.
• Its body may pause and may fail. An error that leaves the body fails the test and is printed in its long form (error.full(): the site and the chain).
• A test fails on an error that leaves it, a false assert, or a panic. A failing test does not stop the others: each test runs in a process of its own, because a panic at user_parallelism = no ends the process (Part III A.2).

test is a reserved word, for this construct.

D2 — assert is a prelude function, and the compiler knows it.

assert(cond)
assert(cond; message: "what should have held")

It is a function in the sense of the language — the subject before the ;, an option after it — so it costs no reserved word, and it is on the prelude’s list (ADR-154 D1). The compiler recognises the call, for D3 to D11, and for its message: a false assert names its line, its condition as written, and the value of each operand of the comparison, because only the compiler knows what they were called:

assertion failed at src/tally.nika:4
    assert(blank == 1; message: "an empty line is blank")
    blank is 2

A false assert is unrecoverable, as a panic is (Part III A.2).

D3 — The condition of an assert is pure.

The condition may not pause, may not fail, and may not change anything: it is sync, it does not throw, and it touches no place and calls nothing that does. A condition that does is refused where it is written.

This is what makes D4 one meaning rather than two. A condition with an effect would make the program behave differently depending on whether the check is performed — and whether it is performed is exactly what a proof changes.

D4 — An assert is a contract: proved where the compiler can, checked where it cannot.

An assert claims that its condition holds whenever it is reached. For each one the compiler does one of two things:

the compiler	then
proves the claim (D9, D10)	no check is emitted; the claim costs nothing when the program runs
does not	the condition is checked where it is reached, and a false one is D2’s failure

The claim means the same in both rows. A proof only removes its cost, so a compiler that proves more removes checks and changes nothing a correct program does. No build option chooses between the rows: debug and release programs hold the same claims, as they hold the same overflow checks (Part I 2.2).

An assert and a guard say different things. A guard — throw … if c, return … if c (ADR-255) — handles a case the program expects to meet. An assert says the case cannot occur, and that if it does, the program is wrong. The first is behaviour; the second is a contract, whose breach is a defect and stops the program.

D5 — A claim about a parameter is the caller’s to establish.

An assert at the top of a function’s body that names only its parameters, and that the body cannot prove on its own, is the function’s precondition. The body assumes it. Each call proves it with the arguments in place of the parameters, and a call that does is free; a call that does not carries D4’s check at the call, so that a failure names the caller that broke the contract rather than the function that stated it:

fn percent(part: i64, whole: i64) -> i64 {
    assert(whole > 0)              // a precondition: `whole > 0` at every call
    return part * 100 / whole
}

fn report(done: i64, total: i64) -> i64 {
    return 0 if total <= 0         // the guard proves `percent`'s precondition
    return percent(done, total)
}

Where the calls cannot all be seen — a pub fn (another package calls it), a method, a function handed on as a value instead of called — the check stays in the body, until the ledger carries preconditions.

D6 — A claim about data from outside the program is a guard’s job, and is refused.

A value whose bytes someone else chose (ADR-010 D2: a socket, a request, a database row) has no property the program can claim: its being wrong is a case the program has to handle, not a defect. An assert about it is refused with NK1202, saying where the value came from and naming the way that works — a guard where it arrives, throw BadInput(n) if n > 100 — after which the claim is proved from the guard and costs nothing.

This is the one place D4’s second row is not offered, and it is what keeps D4’s line between a guard and an assert from blurring: a check the program needs in order to be correct is written by the program and handled; a check that only catches a defect is an assert.

D7 — nikaia --asserts answers which claims are not proved, and why.

Beside --sharing, --tethers and --overlaps: every assert of the program by line, and for each one how it is held —

• proved;
• precondition of f, proved at every call, or with the calls that carry a check named;
• checked at run time, with the reason: the claim is outside what the prover reads (D9, naming the part it could not read), or what the prover knew there and that it was not enough;
• checked by the test (D11);

and a count of the claims checked at run time, so that a project can watch it fall and gate on it. The report is how a reader finds the claims that cost something, and how the prover’s progress is seen.

D8 — A refutation needs a counterexample, and it is a warning.

A claim is refuted only with concrete values that reach the assert with the condition false, and the message shows them:

warning: this assert can be false
  --> src/math.nika:7:5
   7 |     assert(b != 0)
     = `divide` is called with `b = 0` at src/main.nika:12

It is a warning, and the claim stays D4’s check. A compiler that refutes more would otherwise refuse, in its next version, a program the previous one accepted — the fault ADR-244 removed for sync.

D9 — What the prover reads.

• Claims: comparisons of whole numbers built from names, number literals, +, -, a unary - and a * by a constant; true, false, &&, || and !. A claim outside that is D4’s second row, and D7 names the part.
• Names: an immutable binding of a whole-number type — a parameter, a let given an integer type or a value of the shape above, and the binding of a for over a range. An unsigned type adds x >= 0. xs.len() of an immutable list, text or array binding is a name of its own: never negative, known for a literal, and in a precondition the argument’s length.
• Facts: the branch an if is in; the condition a branch that always leaves has ruled out, which is exactly what return … if c, throw … if c, break if c and continue if c write (ADR-255); a for over a..<b’s bounds; a let’s value; the function’s preconditions; and every claim proved before. A lambda’s body keeps what holds around it, because a binding the prover reads never changes; its parameters are new names. A block whose bindings the walk cannot see — a match arm — starts with nothing.
• Numbers are integers without a limit. A computation that would leave its type aborts before any comparison sees it (Part I 2.2), so what holds of unbounded integers holds of the program’s.

D10 — The prover may fail to prove a true claim, and never proves a false one.

Fourier-Motzkin elimination over the facts and the claim’s negation, with the integer tightening of each derived bound: a claim is proved when every case of its negation contradicts the facts. It gives up past a fixed amount of work, and giving up is D4’s second row. A later prover that proves more removes checks; it never refuses a program, and never changes what one does.

D11 — An assert in a test block is the test’s verdict.

A test exists to run code and look at the result (D1); its asserts are checked when it runs, and a false one fails the test. The prover does not read a test’s body, and D6 does not apply to it: a test looks at what the program computed, from whatever input it was given.

D12 — nikaia test runs at the project’s setting; both settings on request.

Each test runs under the user_parallelism the project names. nikaia test --both-settings runs each test at no and at yes, and a test whose outcome differs between them fails with both outcomes shown. The meaning of a program is the same at both settings (Part I 1.2); a difference is a compiler fault, and this is how a project asks for it to be looked for.

D13 — An output test is files and no code.

In a package’s tests/ directory, NAME.stdout makes NAME a test of the package’s program:

file	is
NAME.stdout	what the program must print, compared byte for byte
NAME.stdin	optional: what it is given on standard input (empty otherwise)
NAME.args	optional: its arguments, one per line

The program must also end successfully. ADR-247 gives an output test a directory of its own, NAME.in/ and NAME.out/, and --bless.

5. Consequences

• Every assert builds unless its condition is impure (D3) or it claims something about data from outside (D6). NK1202 is D6’s refusal and nothing else; a claim the prover cannot read, or a call that does not prove a precondition, is a check rather than a refusal, so NK1203 and NK1204 are not issued.
• The cost this accepts: a program can stop in production on a claim nobody proved. It is the cost a panic() in the same place would have had, it is listed by D7, and the claim it comes from is one a later prover can remove.
• The compiler’s own invariants can be written as claims. A Rust unreachable! or assert! that moves to Nikaia with its module becomes an assert, and D7 lists which of the compiler’s own claims are still checked — a work list for the prover, taken after the move rather than before it.
• Part III 14.1 and 14.2 state D1-D13; the release-build removal and the nikaia build --with-asserts flag are gone (D4).

6. What this does not decide

• A project that refuses unproved claims. SPARK’s all checks proved as a setting a package opts into, so that a code base that has reached it stays there. D7’s count is what such a setting would read; whether it exists, and whether it is per package or per function, is asked when a package wants it.
• Preconditions and postconditions in a signature — requires b != 0 — and a precondition in the ledger, which lifts D5’s three exclusions. It needs syntax and a record of its own; D4 to D10 are written so that it can reuse them.
• Claims over text, lists, fields and calls beyond len(): the prover grows a theory at a time, each by its own record.
• The implicit checks. An overflow, an index out of bounds and a division by zero are claims of the same kind that nobody wrote. Whether D4 and D7 apply to them — a proved index check not emitted, and listed — is a later decision; D4’s table is written so that the answer can be yes without a new rule.
• Whether a refutation becomes a refusal (D8), decided when there is a prover that refutes and can be measured.
• An assert only for development. A condition too expensive to check in production wants a second name, not a build option on this one. Added when a program needs it.
• Fuzzing and bench (Part III 14.3, 14.4) are unchanged by this record.

This site is open source. Improve this page.