Verification

How a contract is discharged

Each refinement compiles to an obligation: a predicate to prove, a context of every fact in scope, and the sorts of the symbols involved. The compiler hands it to an SMT solver, which proves context implies predicate by checking the negation for unsatisfiability. An unsat result discharges the obligation. A sat result is a counterexample, rendered back into edda values rather than left as a raw solver model. There is no warning level for an obligation that does not discharge; the build fails.

The decidable fragment

The fragment is chosen so that every obligation terminates with a definite answer, rather than timing out. It is the combination of these theories:

In SMT-LIB terms, AUFLIA + extensionality + bounded quantifiers. Non-linear arithmetic, bitvectors, floating-point predicates, and unbounded quantifiers fall outside it. Where they are undecidable, they stay outside permanently.

The native compiler discharges this fragment with its own in-tree solver — a CDCL(T) core that runs in-process, with no external dependency. The Rust bootstrap that builds it today uses an embedded Z3 over the identical fragment, so a proof one accepts, the other accepts too.

Certificates and the re-checker

Each discharged obligation produces a certificate, one of five kinds: an SMT unsat core, a comptime trace, a built-in obligation, a recorded @unverified reason, or a recorded @trust reason. Certificates are content-addressed and cached under the obligation and its context.

A separate verifier, around 500 lines, sits between the cache and the build and re-checks every cached unsat claim. It reconstructs the obligation from the canonical encoder and re-runs the solver from scratch, ignoring the cached core. If the two disagree, the build fails. The cache is only a hint the verifier can reject: because every cached result is re-derived by an independent check before it is trusted, a poisoned or stale entry can never slip a false proof into a build.

Termination

A recursive function or an unbounded loop either supplies a decreases measure that strictly drops and is bounded below, or it admits effect divergence in its row. There is no third option, so divergence becomes a property a caller can see and decide to inherit.

function factorial(n: i64) -> i64
    requires n >= 0
    decreases n
{
    if n == 0 { return 1 }
    return n * factorial(n - 1)
}

Properties, stability, contract diff

When a proof is out of reach

The solver is decidable, not omniscient. A claim can depend on a theory the fragment excludes, or come from an external proof, or be true for a reason the encoder will not accept. Two annotations cover these cases. Both require a written reason, both produce certificates that are visibly not SMT proofs, and both are listed by edda lint --trust-points.

@unverified(reason: "Knuth TAOCP 2 4.5.3")
function gcd_extended(a: i64, b: i64) -> GcdResult
    requires a > 0 and b > 0
{ ... }

@trust(reason: "bit-shift packing")
let header: u32 = (version << 8) or kind

The trust-points list is the project's full exemption surface. A reviewer can read it, CI can fail on an unreviewed addition, and a published package carries its list in the manifest.