You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This commit was created on GitHub.com and signed with GitHub’s verified signature.
Highlights
One typed program. The checker records each generic call's type arguments, and vera.typed derives the instances a program needs from those records, links the program once and builds each clone once, every node with a type of its own (#1679). Code generation and the verifier read every type, instantiation and clone from it, save seventeen code-generation functions that still read a written type, for v0.2.7, so their own discoveries, the 23 _infer_* walkers of vera/wasm/ and ContractVerifier._resolve_type are deleted (#1525). verify, compile and test take the typed program as their one input (breaking for a program that calls them; the vera commands are unchanged), and a clone is named by its type arguments with their arguments (breaking for a program that names a clone).
A rule that depends on a generic's instantiation is judged at check, at the call that chooses it (#1679). An unsatisfied ability constraint, a State<T> cell or an Exn<E> payload with no lowering, and a handler whose declared state differs from its cell are refused at the root call, naming the chain of instances, where code generation or the verifier refused them after vera check accepted the program; a generic call runs against the clone its arguments fix; and a cycle of generic calls whose instances grow without bound is refused with E139 (breaking).
Thirty-one programs whose types code generation re-derived compile, load and run at the checker's types (#1525): seventeen had a function dropped, seven built a module that did not load, and seven ran to a wrong value, mo(7) == mo(7) printing false among them.
A type variable takes one type. A variable inside a function-typed argument is fixed by that argument's declared type, by the polarity of the position it holds, so a closure no longer carries a negative value into a @Nat (#1525); and a call argument whose type leaves a variable open takes one type for it, so a closure compiled at a type of its own fits no other (#1684's call-argument line). Both are breaking: a @Nat bound from such a call is a narrowing vera verify obligates, and a closure compiled at its own type is refused with E202 where a parameter gives its variable a type.
A construction is modelled at the sort of its checked type, whatever file declares the type (#1525). A call over a construction of a type its function names nowhere proves at Tier 1, 25 runtime checks in 12 corpus programs now prove, and a postcondition its callee's contract does not establish is refused with E500 where it fell to a runtime check (breaking: state the value in the callee's ensures, or keep it as an assert).
An Exn handler's value is the join of its body's and its clauses' (#1794), so a clause of another type is no longer read at the body's type: a clause whose value fits no join is refused with E341 (breaking).
Every diagnostic carries a registered code (#1490). The command line's refusals are E900 to E912 and a runtime trap is E800, each printed as every other diagnostic prints (breaking for a script that matched Error: on stderr), and E604 and E605 give way to E600 and E601.
A message spells a type as the program writes it (#1505): a type argument has no @, a refinement keeps its predicate, and a function type is written out.
A source file that is not UTF-8 is refused with E024 (#1666), by every command and for every module a program imports, at the file and the first byte that does not decode; a \u{...} escape that names a surrogate is E009 (#1728).
The collector no longer marks a block on the free list (#1718), so a stale word no longer keeps the free chain behind it: examples/gc_pressure.vera runs about 12 times faster under VERA_EAGER_GC=1.
A module declares the State cells and Exn tags its code uses (#1744), so a function code generation drops leaves no import for --target wasi-p2 to refuse, and an Exn handler's block takes its result from the checker's type.
The program generator, version two, and a fourth differential. Generated programs hold recursion with decreases, generics, aliases, an imported module, Array, Map, Set and Tuple values, State and Exn handlers and the non-commutative operators; each program and four edits of it go in order through one warm VerificationSession, and each text alone through a fresh one, and the two must agree.
A release starts when CI's run on the merge commit completes (.github/workflows/release.yml); the mutation (diff) lane mutates the lines a pull request changes; the mutation lanes install uv.lock and name an engine failure; and the lock moves to z3-solver 5.3.2.0, ending the hold on 5.x (#1126).
Added
The program generator, version two, and a fourth differential.tests/program_generator.py writes recursion with decreases (a @Nat measure its requires bounds, a mutual pair through a where helper, and a structural measure over a recursive data type), generic helpers called only at types their where clause admits, plain and refinement type aliases at a slot's head and inside a type argument, a module beside the entry that the entry imports by a selective list of what it uses, Array, Map, Set and Tuple values with their readers (array_length, an index under the bound that proves it, array_fold, map_get, set_contains and set_size), handle[State<Int>], handle[State<Nat>] and handle[Exn<T>] with throw, and State and Exn helpers called under them, and pairs of parameters of one type under the non-commutative operators, whose ensures holds for the operands' order the generator meant and not for the other; every contract is still true by construction. tests/test_program_generator.py holds each program to a fourth differential: the program and four edits of it (a literal moved inside its interval, a let added, a pair's operands swapped, a function added with a call to it, a requires tightened, a contract broken and restored) go in order to one warm VerificationSession, as the language server sends a document's text, and each text alone to a fresh session, and the two must report the same obligations, with the same statuses at the same places, and the same diagnostics.
KNOWN_CLASSES counts version one's two nat_bind classes as the one mechanism of #1695 they are (a value the declarations make non-negative, which code generation's declared-name rule does not read as one), and adds three of #1695's that version two's shapes meet: a narrowing into a refinement of Nat, recorded once and checked twice; a refinement check on a value the declarations already give the refinement; and a join of a refined arm with an unrefined one, which the checker types as the refinement. Each predicate reads the program as written, never the checker's tables.
Two counterfactual classes count the finds code generation makes by reading a value's type off the expression rather than the checker's types. A find of the load, reconcile or distrust differential that vanishes with each fold bound in place by a let of the type the checker gives it (a fold's being its initial value's) is #1525's, and one that vanishes once each handler a branch takes is bound too is #1744's; a find that does not vanish is reported. The generator writes those shapes, a fold as a scrutinee or a constructor's argument and a branch whose every arm is a fold, a throw or a handler, and an arithmetic argument at a type variable, whose call runs against the instance the checker chose since #1791 and makes no find.
A warm find whose two sessions differ in a counterexample alone is counted under #1785, with no pin: the differences seen came after other programs in one process and not when the seed ran alone, and the mechanism is not established. The night's report gives each known class its count, its programs and its first seeds.
The generator models as unconstrained what the verifier does not translate (#1696): a generic's call, a fold, a cell's read, an element and a handler's value, an array literal holding a generic call's result, whose length it knows nothing of, a match on a constructor applied in place or on map_get's result, and a call taking a value it has no term for (a constructor of the module's data type among them), whose ensures it drops. A fold takes its initial value's type, as the checker gives it, and the nat_bind class counts a fold from a @Nat bound to a @Nat, which the module guards with no record.
.github/workflows/nightly-generator.yml runs 1,400 seeds a night, where it ran 5,000: on the runner a version-two program with its edits takes 1.24 s, 5.8 times a version-one program's 0.213 s. Every pull request runs ten pinned seeds that between them write every construct of the grammar.
Changed
The lock moves to z3-solver 5.3.2.0, and the hold on z3-solver 5.x that began on 2026-07-21 ends (#1126). The update moves only z3-solver's entry in uv.lock, from 4.16.0.0 to 5.3.2.0. The per-obligation differential over the 323 .vera files under examples/ and tests/conformance/ is identical on the two solvers: the same 3,095 obligations, each with the same kind, status, line, column, code and description. CI's jobs and an installed veralang resolve the unbounded z3-solver>=4.15.5, and have run 5.x since 5.0.0.0 was published on 2026-07-17; the lock governed uv sync environments alone. The floor is unchanged, and the comment above it in pyproject.toml now records that the 5.x wheels are tagged macosx_13_0_arm64 again, where 4.15.5 through 4.16.0 were tagged macosx_15_0_arm64, so README §Supported platforms, not the floor, states the macOS baseline. That section now says what an install does on the platforms it leaves out of scope: on macOS 13 and 14 every dependency resolves to a wheel, and both stay unsupported and untested; where no z3-solver wheel matches, pip install -e . builds z3-solver from source, and --only-binary :all: stops at a "no matching distribution" error. .github/dependabot.yml no longer ignores z3-solver's major updates.
A command's own refusals print as every other diagnostic prints (#1490). A refusal of the command line, and a runtime trap, printed one Error: ... line on stderr. Each now prints the diagnostic block: a header such as [E900] Error at <file>, line 0, column 0:, then the description, the rationale, the fix and the spec section. A trap's source backtrace follows its block. To upgrade, a script that matched Error: on stderr matches the description, which holds the text it matched. The --json envelope keeps every field it had.
Generics are monomorphized once, after the check, and the verifier and code generation read the same instances (#1679). The checker records each generic call's type arguments by the call's identity, and vera.typed derives the instances a program needs from those records, transitively through each instance's own generic calls, links the program once and builds each clone once, every node of it with an identity and a type of its own; each generic call names the instance it calls. The verifier and code generation each ran a discovery of their own, from the AST, and the two sets differed. Breaking for a program that names a clone: a clone is named by its type arguments with their arguments, at the instantiation the checker inferred, so a runtime contract message, a backtrace frame and an exported clone spell it so: gid$Box_LInt_R(@Box<Int> -> @Box<Int>) where it was gid$Box(@Box -> @Box), and option_unwrap_or$Nat where a call's result is bound at @Nat, where it was $Int. To upgrade, a tool or a test that reads a clone's name from a compiled module's exports uses the new spelling, the generic's name and the instance the checker recorded (gid$Box_LInt_R), with a module's data type qualified where another type of its name meets it (#1774): pair at an entry Shape and la's Shape is exported as pair$Shape_Jmod_U24_la_U24_Shape, and a message names it pair$Shape_Jla.Shape. Over the 323 corpus programs, 7 compile to different WAT: one by a clone's name alone, four losing nat_guard checks that could not fail (a clone's Nat result read back at @Nat, a built-in's Nat result, a type-parameter field the scrutinee's type holds at Nat), one checking gid's ensures(@T.result == @T.0) at Box<Int> by structure where it compared heap addresses, and one building two clones where one clone, named at a truncated type, served List<List<Int>> and List<List<List<Int>>>.
verify, compile and test take the typed program as their one input (breaking, for a program that calls them).vera.verifier.verify(typed, source, file, timeout_ms), vera.codegen.compile(typed, source, file) and vera.tester.test(typed, source, file, ...) read every type, instantiation and clone from typed, which vera.typed.build(program, resolved_modules, artifacts) makes from typecheck_with_artifacts's artifacts after a check that reports no error; the optional table parameters (expr_types, expr_semantic_types, expr_target_types, module_artifacts) and the fallbacks that re-derived a table nobody passed are gone, and a program the check refuses has no typed program. The vera commands are unchanged.
A program whose generic instances would grow without bound is refused at check, with E139 (#1679). A cycle of generic calls that instantiates one of its generics at a type larger than the variable it holds, f<T> calling g at Option<T> and g<U> calling f at Option<U>, needs an instance at a larger type for every instance. Code generation served every depth with one clone whose name dropped the type's argument (f$Option), which ran only because every depth had the same representation. Each call that grows the cycle is refused at the call, naming the cycle (f<T> -> g<Option<T>> -> f<Option<Option<T>>> -> ...), with a fix that passes the caller's type variable itself, as a data declaration whose recursion is not regular is refused (E129). Breaking for a program holding such a cycle, which vera check accepted: pass the type variable unchanged at each call the diagnostic names, or carry the nesting in a value of a recursive data type. No example, conformance program or documentation example holds one.
Breaking: a type variable inside a function-typed argument is fixed by that argument's declared type, by the polarity of the position it holds (spec §4.2, #1525). The first argument fixed a generic's variable and a closure was admitted at the other integer type, so with forall<T> fn apply2(@T, @Endo<T> -> @T), apply2(@Nat.0, fn(@Int -> @Int) effects(pure) { @Int.0 - 100 }) was a @Nat holding -95, and apply2(@Int.0, fn(@Nat -> @Nat) effects(pure) { @Nat.0 }) handed -7 to the closure's @Nat parameter, with vera check and vera verify clean. A declared Int at a position whose values the generic receives (the closure's return, a parameter of one of its parameters) now makes the variable Int, and a declared Nat at a position the generic fills (a parameter) makes it Nat, so the Int value argument is a narrowing where it enters, as in pick(@Nat.0, @Int.0); array_fold, a user generic and a constructor take the rule alike. A closure that fixes one variable both ways is refused at that argument with E202, which names the two positions and the two types, and whose fix declares the closure's Int result Nat (replace 'fn(@Nat -> @Int)' with 'fn(@Nat -> @Nat)'). Upgrade: a let @Nat, a @Nat argument or a @Nat result of such a call, which was typed Nat and checked by nothing, is a narrowing, obligated by vera verify (Tier 3, or refuted with E503) and guarded where it is bound: declare the closure's result @Nat, or bind the call at @Int. No example, conformance program or documentation example changes verdict.
Code generation reads every type from the typed program, save seventeen functions that still read a written type (#1525). A value's width is its checked type's, and an if's, a match's and a handler's block result the join's (an Exn handler's the join of its body and its clauses, #1794); a call's, an element's, a key's, a value's, a scrutinee's and an interpolated part's type is the checker's; a value declared at a written type (a let, a parameter, a binder, a cell, a payload) is laid out by the type that resolves to, a parameterised alias's target under its arguments, and a sub-pattern's field by the type it matches; and whether a value narrows into a @Nat slot is the verifier's rule (vera.narrowing.nat_narrowing) over the same types. The 23 _infer_* walkers of vera/wasm/, code generation's @Nat reading by declared name, the @Byte literal marks and the fused-await predicates over syntax are deleted. Over the 323 corpus programs, 44 compile to different WAT and none changes whether it compiles: 26 lose 65 nat_guard checks that could not fail, at the binding of a value the checker types Nat (a @Nat call, a State<Nat> operation, an alias of Nat), which code generation guarded by its own reading and the verifier recorded no narrowing for, and six of them no longer import vera.trap; 17 root a heap value a call returns that code generation could not type and left off the shadow stack (39 pushes), or save the shadow stack's top around an Exn handler; and 3 lose a drop after a throw statement. The seventeen derive a type from the type expression the program writes, a signature's and a closure's WASM types (_type_expr_to_wasm_type), a refinement guard's carrier, a data layout and a clone's key among them; tests/test_typed_program_1525.py's class cell holds them as its known list, and they close with v0.2.7's obligation table (#1695).
A built-in's type variable is bound through a refinement alias of its argument's type (the #1688 line of #1684). map_values(@M.0), for type M = { @Map<String, String> | map_size(@Map<String, String>.0) >= 0 }, left its value variable unbound, so the element fitted any parameter: takes(map_values(@M.0)[0]), with takes(@Nat -> @Nat), passed vera check and compiled to a module that did not load. The variable is bound from the refinement's base, so that call is refused with E202 (Argument 0 of 'takes' has type String, expected Nat.), and at a @String parameter it runs as before.
Breaking: a construction passed to a call is modelled as any argument is, so a postcondition its callee's contract does not establish is refused (#1525). The verifier gave a construction a sort only where the function named its type in its signature or in an earlier let, so a main whose ensures(@Int.result == 2) rested on color_code(Green), under color_code's ensures(true), fell to a runtime check (E522), while the same call over an @Int was refused. A construction is now a term of the sort of its checked type (Fixed, below), and since the verifier is modular (spec §6.4.2), a claim the callee's contract does not make has a counterexample and is refused with E500, as DESIGN.md's pipeline refuses every satisfiable negation. Upgrade: state the value in the callee's ensures, ensures(match @Color.0 { Red -> @Int.result == 1, Green -> @Int.result == 2, Blue -> @Int.result == 3 }). A value a recursion computes cannot be stated there, since a contract may not call its own function or a mutual partner (E138, spec §6.3.1), so a caller that pins one keeps it as an assert, which is checked at run time as the ensures was. An equality between a data type at Nat and the same at Int is a runtime check where a side reads a parameter's or an opaque result's value, through a @Nat binder too, since such a value states no >= 0 of its Nat components (#1814): mk(@Nat.0) == Some(nat_to_int(@Nat.0)) under mk's ensures, which was proved, is one now, and so is @Box<Nat>.0 == MkBox(@Int.0), which was refused with E500 and the counterexample MkBox(-1). Eight conformance programs pinned such a value and are rewritten so: five give the callee the ensures, three keep the value as an assert; their output is unchanged, and no example or documentation example moves.
The verifier reads every type from the typed program and derives none (#1525). A parameter's, a return's, a let's, a binder's, a field's, an operation's, a cell's and an alias's declared type is the type the checker resolved its type expression to, and a generic instance's type arguments are its instance's; ContractVerifier._resolve_type and the verifier's alias resolution are deleted. A construction's sort is the sort of the type the checker gave it, whatever file declares the type, and Nat and Int are one sort, as a refinement and its base are; the recovery of a constructor's instantiation from its arguments' sorts, the selection among the sorts already built and the forced parameter sorts are deleted. Code generation guards a @Nat pattern binder and destructure component where the verifier records a narrowing, reading the component's sources as the verifier does (vera.narrowing.component_narrows), so the binder of match Some(5) { Some(@Nat) -> … } and the 5 of let Tuple<@Nat, @Nat> = Tuple(@Int.0, 5) hold no nat_guard. Over the 323 corpus programs the obligation stream moves in 12, each move a runtime check that now proves (25 in all), and WAT in one, which loses a destructured 5's guard; the reconciliation join's known mismatches go from 33 to 32.
Breaking: a closure from a generic call that leaves its type variable unfixed, or a data value whose type holds a function over that variable, whatever the value holds, fits no parameter, array element or branch that gives the variable a type (#1684). use(mk(())), with mk(@Unit -> @Endo<T>) returning the identity and use taking a fn(Int -> Int), passed vera check and trapped at run time; it is refused with E202, whose fix writes the closure at the type the parameter asks: fn(@Int -> @Int) effects(pure) { ... } in place of mk(()). The None a call of result type Option<Endo<T>> returns is refused the same way at an Option<IntEndo> parameter, which vera run ran: build the value at the parameter's type. Giving the call an argument that fixes T keeps either. A closure whose variable no argument fixes, passed where the parameter's own variable is unfixed too, is refused the same way, which vera run ran. No example, conformance program or documentation example is affected.
A release starts when CI's run on the merge commit completes, rather than polling for it (.github/workflows/release.yml). The workflow runs on workflow_run for CI's completed runs on main, and its first job goes on only for a successful run of the push event on main in this repository, which a fork's pull request whose branch is named main, or the nightly run, is not. It names the commit that run tested, in its job summary beside the CI run, and every later job checks out that commit, builds the archives from it and tags it, where they read the event's own commit, which under workflow_run is main's tip when the event fires. The v0.2.5 release failed at the 100 minutes scripts/await_ci.py waited: CI's push run on the release commit took 106, its macOS cells waiting 31 to 70 minutes for a runner, and the failed job was re-run by hand. A dispatched production recovery, which no CI run starts, still waits for CI's run on its commit, now for at most 180 minutes. Releases start in the order their merges' CI runs complete, so the GitHub Release is marked Latest only when no higher version is already released. tests/test_await_ci.py holds the trigger, the gate over the 144 combinations of a completed run's conclusion, event, branch and repository, every read of the commit, and the Latest mark, by running the release step under a stand-in gh.
The mutation (diff) lane mutates the lines a pull request changes, not the whole functions that hold them (scripts/mutate_diff.py). mutmut generates only the mutants whose node starts within two lines of a line the diff adds, or of a point where it removes lines, or on the first line of a call, match, assignment, operation, comparison, conditional expression or lambda that spans one of those lines, inside the functions the diff changes: mutmut places a mutant on its node's first line, and those nodes' mutants change text below it, as a call's argument or a case (an edit to error_code="E302", at vera/checker/control.py:430 keeps the argument's None and its removal, placed on the call's first line at :419). The script runs mutmut through itself (--as-engine), which counts each function's mutants on every line and in the window with mutmut's own visitor and hands each file's window to mutmut's covered-lines hook; the lane checks the mutants mutmut lists against those counts, and a mutmut without the hook stops the run as an engine failure (exit 2). Of this cycle's eleven runs with mutants, ten stopped at the 2,400 s budget, four of them before deciding any mutant; an edit inside an existing function keeps 21 to 32% of its mutants in the window (#1760's 330, of which 97 were decided at the budget, hold 85), and a diff that writes new functions keeps nearly all of theirs. The job summary names the rule and counts the functions selected, their mutants on every line and in the window, and the mutants generated, decided and surviving. The budget is unchanged.
The budget marker's test allows the float rounding of a deadline read in the tick it was set (#1689). tests/test_budget_marker_1670.py's child test reads the budget left as deadline - time.monotonic(), where the deadline was time.monotonic() + seconds; on a clock that had not advanced between the two reads, as on the Windows runner, that is (t + 5) - t, which rounded to 5.000000000000057 and failed the bound left <= 5. The bound allows 1e-6 above, and a cell runs the child's own assertion at a clock sample that rounds the same way. The same bound failed the [own-budget-xdist] case on the Windows runner (#1771): the child stopped at it, with 5.000000000000057, before its slow stage ran, so the parent found no watchdog header.
scripts/check_wheel_availability.py says when its interpreter has no pip (#1743). It runs python -m pip download for each dependency and platform, and a virtual environment uv sync creates holds no pip, so every one of the 36 cells failed there with No module named pip, and the script said a platform had lost its wheels. It checks for pip once, before the matrix, and without it stops with one message naming the cause and exit 2, which no lost platform returns. CI's job runs under an interpreter that has pip and is unaffected.
Removed
E604 and E605 (#1490). These were the compilability check's codes for a parameter type and a return type with no WASM representation, and the registry titled them for state effects. The check now emits E600 and E601, the codes of those concepts, which the signature compile emits for the same two, and vera errors no longer lists E604 and E605. To upgrade, a consumer keyed on E604 keys on E600, and one keyed on E605 keys on E601.
E619 (#1679). Code generation's refusal of an Eq constraint whose type argument a constructor fixed only in part (id1(MkErr(5)) on Res<A, B>, A unfixed). A type argument no argument fixes is instantiated at the phantom type, as every other one is, at which Res<Bool, Int> derives Eq, and the program runs. vera errors no longer lists the code.
E622 (#1679). The verifier's refusal of a generic call whose type argument its own discovery could not infer. The instances are derived from the check's record of each call, which holds what the call's arguments fix, and a type argument no argument fixes is instantiated at the phantom type, so no call is left uninferred. vera errors no longer lists the code.
Fixed
Every diagnostic carries a registered code (#1490). Spec §0.5.1 requires a stable code on every diagnostic. Five diagnostics about source code carried none, and neither did the command line's 25 JSON diagnostics, so --json had no error_code and the text no [Exxx] prefix, and nothing enforced one.
The missing-visibility error on a fn or data declaration is E188. The removed alias Float is E136, the unknown type name it is. Code generation's guard rail for a call with no target, module-qualified or bare, is E624. The WAT assembler's failure is E699, as its sibling branch is.
The command line's diagnostics are Diagnostics, in two ranges added for them. E8xx is a program's own failure while it runs: E800 is the runtime trap, located at the function that trapped, with its trap_kind, frames and fix kept. E9xx is a refusal of the command line itself: E900 a source file not found, E901 an option a command does not take, E902 options that contradict each other, E903 a value an option does not take, E904 a command line vera does not understand, E905 a module that exports no function, E906 a --fn that names no export, E907 an entry code generation dropped, E908 a program that lacks what its target needs, E909 arguments that do not fit the function, E910 an address vera serve cannot bind, E911 a missing optional dependency, and E912 an output path that cannot be written, which vera compile -o into a missing directory reported as the source file not found, and an unwritable one as a traceback. Each envelope keeps the fields it had and each description its text. Each gains a rationale, a fix and spec §0.5.1, which states what the two ranges mean, and vera errors lists the codes under the phases run and command. vera ast --json prints a file not found in its envelope.
E607 is titled for what it reports: a State cell type that code generation cannot lower.
scripts/check_diagnostic_fields.py fails a diagnostic site with no code, which no opt-out waives. It also fails a diagnostic built by hand (a dict with a severity key, or a string holding one), except at the two sites it names: Diagnostic.to_dict and the internal-error envelope's last resort.
A message spells a type the program writes as it is written, in contract clauses, slot and result references, signatures, the Exn boundary message and the operation signatures in E340's fixes for a user-declared effect or ability: a type argument has no @, a refinement keeps its predicate, and a function type is written out (#1505). ast.format_type_expr rendered each type argument as a type in a slot's position, a refinement as its base and a function type as @?, so vera verify --json's obligation descriptions, runtime contract and trap messages, diagnostics and the vera check --explain-slots header showed @Array<@Int>.0, which fails vera check with E005 when pasted back, and read two parameters that differ only in a refinement's predicate as one type. A type is now rendered by the canonical formatter, as vera fmt writes it: requires(array_length(@Array<@Int>.0) > 0) failed reads requires(array_length(@Array<Int>.0) > 0) failed, and fn f(@Array<@Int>, @Array<@Int> -> @Int) reads fn f(@Array<{ @Int | @Int.0 > 0 }>, @Array<{ @Int | @Int.0 < 0 }> -> @Int). The places that rebuilt the rendering themselves read it as it is:
vera/addEffect keys a handler by the bare rendering, so a handler whose argument holds a function type (handle[Exn<Option<fn(Int -> Int) effects(pure)>>]) bounds a request spelled the same; the key spelled the function type ?, and the caller was given a row it did not need.
E340's fixes write an operation's signature from the program's declaration of its effect or ability, its refined parameters whole, whichever side of the use it is declared on. The fix for a row naming a user-declared effect wrote each refined parameter's base for an effect declared further down the file and {@Int | ...}, which does not parse, for one declared above; the fixes for an operation called under a row without its effect and for a user-declared ability's constraint or operation wrote {@Int | ...} in either order.
The message for an exception escaping an entry point names the row's type: Exn<Array<{ @Int | @Int.0 >= 0 }>> read Exn<Array<Int>>, and the handle[Exn<Array<Int>>] it asked for does not catch it.
The verifier's sentence for an operation in a refinement's predicate (E526, E502 and the other operation diagnostics) names the refinement with its base's arguments bare and its predicate as vera fmt writes it.
A source file that is not UTF-8 is refused with E024, at the file and its first byte that does not decode, by every command and for every module a program imports (#1666). Every reading of a source was read_text(encoding="utf-8"), and the decoding error a file in another encoding raised reached no handler of its own: vera check, vera verify and vera test reported it as the internal error E699; vera compile, vera run, vera ast, vera parse, vera fmt and vera serve exited with a Python traceback, with nothing on stdout under --json; a source on stdin did the same; and an imported module that was not UTF-8 was E013, a module that failed to parse. Every reading now goes through one reader, vera.parser.read_source (decode_source for the bytes vera fmt and stdin read), and a source that does not decode is E024, "Source file is not valid UTF-8": the byte and its offset, located at that byte's line and column in the file that holds it, with the iconv command that converts the file in its fix, and a UTF-16 or UTF-32 byte-order mark named. Under --json it is in the command's envelope. The language server reads a document's imports through the same resolver, so a module that is not UTF-8 is its E024 there too, and reconcile_file (scripts/check_reconciliation.py) records it as the program's refusal where it raised. A file that is UTF-8 reads as before: the 497 .vera files in the tree read the same through the old reader and the new.
A rule whose answer depends on what a generic is instantiated at is applied at check, at the call that chooses the type arguments (#1679). Code generation made four of these judgments per clone, and the verifier a fifth, after vera check had accepted the program: an ability constraint the instantiation does not satisfy (E613, reported at line 0 with no location), a State<T> cell at a type no cell holds (E607, the clone and each caller dropped), an Exn<E> payload at a type with no representation (E612, the same), and a handler whose declared state differs from its cell at the instantiation (E533 at vera verify, and a module that failed to load at vera compile). The check now derives the instances a program needs once, from the type arguments it inferred at each generic call, and refuses each failing one at the root call, the call in a body that is not generic whose type arguments reach it, naming the chain of instances and replacing the call in its fix: lt(true, false) under forall<T where Ord<T>> reads The call 'lt(true, false)' instantiates 'lt' at T = Bool, where type 'Bool' does not satisfy ability 'Ord', ..., fixed by replace 'lt(true, false)' with 'lt(0, 0)'. The codes are kept.
A Map or Set with an Array key, value or element is E135, as a zero-size one is (#1680): where the type is written, at a map or set operation whose component only inference gives, and at each instance of a generic whose component is a type parameter. let @Map<Array<Int>, Int> = map_insert(map_new(), [1, 2], 5) passed vera check and vera verify, and code generation dropped its function (E602).
A generic callee's effect row is read with its type parameters instantiated at the call (#1769): peek(1) under handle[State<Int>], for forall<T> fn peek(@T -> @T) effects(<State<T>>), was refused with E125 (Function 'peek' requires effects(<State<T>>) but call site only allows effects(<State<Int>>)), and the contract-purity read (E187) took the same row.
A generic callee's precondition is checked at the call against its clone's contract, as a monomorphic callee's is (#1468): refuted (E501) where it fails, proved where it holds, and demoted (E532) only where it cannot be decided. Every precondition of a generic callee was demoted, a requires(false) behind a module boundary and a provable one alike.
A generic call is instantiated at what its arguments fix, and runs against that clone (#1679). An empty array literal's element type, a type variable of the caller's spelled as one of the callee's, and a callee's variable a nested call left unresolved each bound the callee's variable to nothing, so the call ran against the clone at the phantom Bool: eq_or([], MkBox(1), MkBox(1)) printed false, pick_first([], 5000000000) failed WASM validation (type mismatch: expected i32, found i64), and wrapped_same(7, 7), calling same(Some(@T.1), Some(@T.0)) with both generics' variable named T, compared two heap addresses. A position an argument's type leaves open is now a hole the arguments beside it fill, and one nothing fills is the phantom, which no value of the arguments holds: same(empty(()), empty(())) instantiates same at Option<Bool> and compares by structure. A variable a nested call leaves unresolved is a hole from that call's own type on, so renaming a generic's type variable never changes what it instantiates. match pick_first([], MkTag("q", Red)) { ... }, refused with a false E313, checks, and a constructor's type is fixed the same way: second_head(MkTwin([], [5000000000])), for data Twin<T> { MkTwin(Array<T>, Array<T>) }, read the element at the phantom's width and printed 0.
E613's fix for a type variable no argument fixes names a parameter that carries it (#1679). It asked for an annotation of the value the variable is fixed from, and the type a result is bound at fills only a literal's hole, so let @Option<Int> = none_ord(()) still instantiated none_ord at Bool.
E135's fix replaces the component it refuses (#1680). It found the component by its text, so for Map<Array<Int>, Array<Int>> the value's fix wrapped the key: Map<Option<Array<Int>>, Array<Int>>, itself refused. It is found by its position in the type as written.
The collector no longer marks a block on the free list, so a word that names a freed block, a stale word in the slack of a block $alloc reused whole or an integer equal to its address, no longer keeps the free chain behind it and every stale graph those blocks still name (#1718). The sweep links a freed block through its first payload word and leaves the rest, $alloc reuses a block whole, and Phase 1 recorded every block on the allocation chain as an object base, so one such word marked a free block, its free-list link marked the next, and memory the program no longer held was retained at every collection that met a free list. Under VERA_EAGER_GC=1, 58 of the 146 runnable corpus programs that carry the collector marked free blocks, examples/gc_pressure.vera 43,500 over 29 collections, up to its whole free list of 2,900 blocks in one; the ordinary collector marked them in a Map<String, Int> of 100 keys and in an Array<String>, a Map<String, Int> and a list of 20,000 values each. Phase 1b now clears the object-base bit of every block on the free list, so $gc_is_base refuses a free block at the shadow-stack seed, the drain and the rescan alike. It costs one step per free block per collection and nothing per allocation, and examples/gc_pressure.vera runs about 12 times faster under VERA_EAGER_GC=1, the free chain it kept no longer marked and scanned at each collection. VERA_GC_CHECK_MARKS=1 also traps on a mark store to a block on the free list, which it finds by walking the list.
A \u{...} escape that names a surrogate, \u{D800} to \u{DFFF}, is refused with E009 where escapes are decoded (#1728). The escape decoder refused only a code point above U+10FFFF, so a lone surrogate, which is no Unicode scalar value and has no UTF-8 encoding, passed vera check and vera verify, and vera compile, vera run and vera serve exited with a Python UnicodeEncodeError traceback from the string pool. Every string literal is decoded at one place, so the refusal holds in an expression, a match pattern, an interpolated string's text, a contract, a refinement and an imported module (there as the module's E013); its fix writes a character outside the Basic Multilingual Plane as one escape of its code point, \u{1F600}, never the UTF-16 pair \u{D83D}\u{DE00}. Spec §1.6's escape table names the domain, a Unicode scalar value. A raw surrogate cannot enter from a file: its UTF-8 form does not decode, which is E024.
A module declares the State cells and Exn tags its emitted code uses, and an Exn handler's block declares the result its arms leave (#1744). Each emitter that calls a cell (a handler's push, put and pop, a get or a put, an inlined clause, an old snapshot, a new read) or throws or catches a tag (a throw, a handler, an export's boundary) records it on its function's context, and the record joins the module's at the merges the host imports' records join it at, so a function code generation drops (E602) declares neither. With a handle[State<Int>] or an effects(<State<Int>>) row in a dropped function, the module declared state_get_Int, state_put_Int, state_push_Int and state_pop_Int with nothing calling them, and --target wasi-p2 refused it (state (Int)). A cell a row names and no code calls is not declared either, so ExecuteResult.state holds an entry for each cell the code calls. An Exn handler's block takes its result from the type the checker gave the handler, or from its throw clause's where the handled body always throws. It took it from code generation's own reading of the two arms, which had no answer for an arm ending in a handler or in an array_fold over a closure, so an Exn handler with a State handler in its body and in its throw clause compiled to a module that did not load (values remaining on stack at end of block). _scan_io_ops, whose walk reached only what the handler walk reaches, is deleted; the handler walk refuses a function whose handler names a cell or payload no lowering exists for (E607, E612) and declares nothing. Of the 458 corpus and documentation programs that compile, one moved: tests/conformance/ch07_state_new_family.vera declares its cells in the order its code first uses them, with the same imports and the same output.
A clone's name qualifies a module's data type wherever the entry file's type of the same name meets it (#1774). The clone-name display counted only module owners of a name, so a clone instantiated at an entry Shape and a module's Shape was spelled pair$Shape_JShape in a runtime contract message and its backtrace frame, beside a signature reading (@Shape, @la.Shape, @Int -> @Int). It reads pair$Shape_Jla.Shape, as display_type_names spells the signature: the entry's type, written bare in the message or in a clone's suffix, counts as an owner.
vera ast --json prints a refused program's diagnostic in the envelope the other commands print (#1789). vera ast printed a parse or transform refusal as text on stderr whatever --json said, so vera ast --json exited 1 with an empty stdout; it prints the envelope vera compile --json prints for the same program, {"ok": false, "file": ..., "diagnostics": [...], "warnings": []}.
vera compile and vera run report an exception in the check as E699 (#1793). An exception raised inside the check escaped both commands as a Python traceback, with an empty stdout under --json, where vera check and vera verify report it as the E699 envelope (#1360). Both commands now report it that way, and their function-scope imports sit inside the backstop too. vera run reports a RuntimeError that is not an argument refusal as E699, where it printed it as Error: text, and VERA_DEBUG_HOST_ERRORS still lets a host binding's exception reach the caller.
An Exn handler's value is the join of its handled body's and its throw clauses', and a clause whose value fits no join is refused with E341 (#1794). The checker typed a handler by its body alone and checked a clause's body against nothing, so a clause of another type passed vera check and vera verify and its value was read at the body's type: with throw(@Int) -> { some_of(@Int.0) } beside a body of type Result<Int, Int>, pick(true) printed 105, the clause's Some(5) read as Err(5), and an Int body beside a Bool clause compiled to a module that did not load (type mismatch: expected i64, found i32). A body that always throws made the handler Never, which fits any type, so handle[Exn<Int>] { throw(@Int) -> { @Int.0 + 1 } } in { throw(@Int.0) } was accepted as the body of a -> @String function and its module did not load; the handler has its clause's type, so that body is refused with E121. A Nat body beside an Int clause joins at Int, so a let @Nat of the handler is a narrowing the verifier records and code generation guards. E341 is reported at the clause's body (The 'throw' clause's value has type Option<Int>, but the handler's value is Result<Int, Int>.), with a fix that writes a value of the handler's type in its place (replace 'some_of(@Int.0)' with 'Ok(0)'). A clause that throws again is Never and keeps the body's type, and a State handler is typed by its body as before. Breaking for a program whose clause produces a value of another type than its handled body's, which vera check accepted: give the two one type, as the fix says. No example, conformance program or documentation example has one.
A program whose types code generation re-derived compiles, loads and runs at the checker's types (thirty-one checklist lines of #1525). Seventeen compiled with the function dropped (E602), so vera run refused to call it: a let or a binder at a parameterised alias (let @Id<Nat> = 5, Some(@Id<Nat>), let @Wrap<Int>, let @Two<Int>), apply_fn on a closure a call returns or a State cell holds, an index into an array literal or into a generic call's array ([true][0], id([4, 5])[1], pick([1, 2][@Nat.0], 5)), a match on an array_fold, an integer pattern over a call returning Byte, an array literal of closures, a constructor of array_map's result, show of array_reverse's, and a literal or wildcard sub-pattern (Some(3), Tuple(@Int, _)). Seven compiled to a module that did not load: a @W<Int> parameter for type W<T> = String (expected a type but nothing on stack), a State<Future<Int>> cell (expected i32, found i64), wrap(3)[0] for forall<T> fn wrap(@T -> @Array<T>) (expected i64, found i32), an if whose arms are a throw and an array_fold, or two State handlers, and an Exn handler valued at a String written as a statement (values remaining on stack at end of block), and a let @Opt<Int> that dropped main and left option_unwrap_or$Int behind (unknown memory 0). Seven ran to a wrong value: == on two calls returning a data value compared heap addresses, so mo(7) == mo(7) and wrap(1) == wrap(1) were false and same's ensures(@Bool.result) over duo(7) == duo(7) trapped; map_get on a State<Map<String, Int>> cell's value returned 0 for 5; map_keys of an if printed an empty line for a; "\(byte_id(65))" printed true for A; and "\(-@Nat.0)" trapped (Negative value bound into a @Nat slot) where it is -5.
A closure argument no longer carries a negative value into a @Nat (#1525). apply2(@Nat.0, fn(@Int -> @Int) effects(pure) { @Int.0 - 100 }) returned -95 from a -> @Nat function, and array_fold(@Array<Int>.0, @Int.0, fn(@Nat, @Int -> @Nat) effects(pure) { @Nat.0 }) handed -7 to the closure's @Nat parameter, with vera check and vera verify clean. Under the polarity rule (Changed, above) each is a narrowing the verifier records and code generation guards: vera verify refutes the second (E503), and both trap at run time rather than return a negative @Nat.
A refinement in an effect's type argument is type-checked as a refinement anywhere else is (#1525). effects(<Exn<{ @Int | @Int.0 + 1 }>>) passed vera check with a predicate that is not a Bool, and its module did not load; it is refused with E126 (Refinement predicate must be Bool, found Int.), in a signature's row, a function type's, a closure's and a handler's effect alike. Breaking for such a predicate in a handler's or a closure's effect, which ran: write the predicate as a Bool. No example, conformance program or documentation example has one.
A construction of a type its function names nowhere is modelled, whatever file declares the type (the constructed-sort lines of #1525). four(Bravo(@Int.0)), in a function that names no Gauge, did not translate, so four's ensures(@Nat.result == 4) was not assumed: a caller's ensures(@Nat.result == 4) over it fell to a runtime check (E522), and pos(@Int.0) after let @Int = four(Bravo(@Int.0)) was refused with E501, where the same call after an unused let @Gauge proved. A constructor of a data type the entry imports had no sort in the entry: need(@Int.0) after let @Int = zero(Amber(0)) was refused with E501, and after let @Tally = Amber(0) and let @Int = zero(@Tally.0) it fell to a runtime check (E532). Each proves at Tier 1 now, and so does an imported generic's decreases measure over its module's data type in the importer's run, as in the module's (the #1577 line of #1561).
A value built from @Nat components and matched back at Int no longer crashes vera verify (the #1594 line of #1525). let @Option<Tuple<Int, Int>> = Some(Tuple(@Nat.0, @Nat.0)) matched with a None -> Tuple(1, 1) arm raised an internal error (E699, a Z3 sort mismatch); it verifies.
A counterexample names each parameter as the source does (the #1767 line of #1525). For private fn foo(@Int, @Int -> @Int) with requires(@Int.1 == 3 && @Int.0 == 4), E500 printed @Int.0 = 3 and @Int.1 = 4, the reverse of the requires; it prints @Int.0 = 4 and @Int.1 = 3, and an instance of a generic names its parameters as the generic does (@T.0).
A call argument whose type leaves a type variable open takes one type for it, and a function compiled before its variable had a type fits no other (the call-argument line of #1684). The argument judgement (CallsMixin._fits) matched each open variable as a wildcard, one position at a time, so a value of type Tuple<Option<T>, Option<T>> fitted a Tuple<Option<Int>, Option<String>> parameter, and the identity closure fn(T -> T) from a call no argument of which fixes T, which code generation compiles at a type of its own, fitted fn(Option<Nat> -> Option<String>) and ran with a Nat read as a String, or trapped against fn(Int -> Int); the closure from mk2([]), whose T is an empty literal's element type, fitted fn(Array<Nat> -> Array<String>) the same way (#1692). A generic call's result also took the data type its context expected on the type's name and arity alone (_synth_fn_call), before the judgement saw it: a data value holding such a closure fitted any instantiation of its type, an if gave twice(None) the other branch's Tuple<Option<Int>, Option<String>> (#1690), and in a forall<A> body Two<A, A> passed as a Two<Int, Int>, so g(true) printed 68719476737. Both now ask the join an array literal's elements and an if's and a match's arms are given (#1668): each open variable is bound once by name, one in a function type or in a data field held over one is not open, and the enclosing function's own are rigid. E202 names the variable, its two positions and the two types the parameter gives it, or, for a function compiled at its own type, the closure to write in place of the call; a built-in's variable a failed substitution lost keeps the verdict it had (#1688). An array literal's element is held to the literal's element type by the same judgement, so an element that would give such a closure's variable a type is refused (E162), as an if's branch and a match's arm already were. No example, conformance program or documentation example changes verdict.
The mutation lanes install uv.lock, and the engine is mutmut 3.8.1 (.github/workflows/mutation-nightly.yml, .github/workflows/mutation-diff.yml). Both lanes installed with pip and resolved every package afresh on every run, so on the night of 28 October 2026 they resolved pytest 9.2.0, published the evening before, which dropped the private item._nodeid that mutmut 3.8.0's stats collector reads at every test's teardown: every test of the stats pass errored there, and the night decided nothing (#1804). At the lock's pytest 9.1.1 the same engine passed both lanes' self-tests. Each lane now runs uv sync --locked --extra mutation and every later step that environment's python, pytest and mutmut; --locked refuses a lock that pyproject.toml has moved past, no workflow names a mutmut version of its own, and the lanes run the lock's z3-solver, 5.3.2.0, the version pip resolved. The diff lane also runs on a pull request that moves uv.lock, either lane's workflow, script (with scripts/mutation_report.py, which the sweep imports) or self-tests, or tests/mutation_oracle.py, and runs both lanes' self-tests against the engine it installs, so a lock bump that breaks the engine is red on its own pull request before any night runs on it. The lock moves mutmut 3.8.0 to 3.8.1, which reads item.nodeid (boxed/mutmut#616), and pytest 9.1.1 to 9.2.0. A new engine version starts every function afresh, so the sweep's cycle 1, from 2026-10-17, restarts; it stood at 12,351 of 12,922 counted mutants decided and 298 of 2,521 functions generated.
A mutation lane names an exception of the engine's own code instead of dropping the tests it stopped (scripts/mutate_diff.py, scripts/mutate_sweep.py). A lane drops a test that fails inside mutmut's copy with no mutant active and runs again, up to five tests; on the night of 28 October every test errored in mutmut's own teardown hook, so the night's self-test dropped both of its tests, and its third attempt deselected every test. A traceback whose first frame outward from its innermost, past the standard library's, is in the installed mutmut package now stops the run at that attempt, dropping no further test, and the record's new engine_error field, the slice's and the diff lane's summaries and the night's problems name the exception and that frame: stopped by the engine: AttributeError: 'Function' object has no attribute '_nodeid'. Did you mean: 'nodeid'? (mutmut/runners/harness.py:157). A hook raising outside a test's phases is read from the traceback pytest prints as its own internal error, and a traceback in a test's captured output decides nothing; tests/test_engine_failure_matrix.py holds the rule over every report, deciding frame, exception and placement of captured output that a stopped pass prints. A RecursionError is the engine's only when none of its ten innermost frames outside the standard library is the copy's, a frame printed with [Previous line repeated N more times] counting N more: a recursion runs out of stack wherever the stack ends, and through mutmut's trampoline that was the engine's own frame at two of eight depths measured, so the sweep still drops tests/test_family_naming.py's cap test for its recursion through ExpressionsMixin._synth_expr.
The program generator writes a comparison that stands as an operand of a comparison of its own level in parentheses (#1781). Version one wrote a let's comparison, inlined into an exact ensures, as 0 == -5 != true, which the parser refuses (E005) since a comparison groups with no comparison of its own level; the generator's first scheduled night failed on three such seeds.
