v0.2.7

Highlights

• One obligation table. One pass over the typed program lists every obligation site once as a row (vera/obligations/table.py); code generation emits a runtime check for every row the table holds guardable and for no other node, and vera verify discharges every row in the context its traversal reaches it in, each record naming the rows it discharges (#1695, #1836). The verifier's 49 guarded= predictions, its six mirrors of code generation's decisions, its narrowing walk and its fallback discharge are gone, and the reconciliation join keys on row identity, so the corpus gate and the program generator allowlist nothing. A row no check can guard is disclosed (E542, E543), never counted. Upgrade: the tier counts move (over the corpus, Tier 1 2,423 to 2,483 and Tier 3 674 to 683), and a signed division whose divisor only a zero check excludes (requires(@Int.1 != 0)) moves from Tier 1 to Tier 3, its INT_MIN / -1 row left to the check; requires(@Int.1 > 0) proves it.
• A refinement recorded at a join is no longer a premise of the value (#1716). An if, match, block or handle is established at the type its leaves share, so a payload that read verified while the run broke it is refuted (E505).
• A generic instantiated at a function type compiles and runs (#1783), where code generation refused the clone and dropped every caller.
• One rule for an expression the verifier cannot translate (#1696): one stand-in of its checked type's sort, carrying its type's facts, and a refutation that rests on one is undecided unless the goal is false for every value it could take. Beside it, a refused binder draws no second error (#1563) and a refuted postcondition's counterexample prints the body's result (#1707).

Changed

• The obligation table's second half (#1695, Stage 27): vera verify discharges the table's rows and lists none of its own. Each record names the rows it discharges (ProofObligation.rows), one record per written site: a site's copies (a measure re-evaluated at each self tail call, a handler clause inlined at each operation call, a predicate lowered by each guard) and a generic's instances share it, with the worst of their statuses, and a record whose status a self tail call decides says so in its description. Whether a site has a runtime check is the row's: the verifier's 49 guarded= predictions and its six mirrors of code generation's decisions are gone. vera verify's join (vera.reconcile.join) pairs a record's rows with the checks that name them, so it reports a mismatch only where a guardable row has no check or a check's row has no record; scripts/check_reconciliation.py and the program generator allowlist none (both lists were 30 entries and 7 classes). The counts move where a row had no record before: a discharged call precondition is a Tier 1 record (34 in the corpus), a division by a non-zero literal (10 in the corpus) and a refined parameter's entry check or a producer's refined return component (9) are Tier 1 rows, a signed division's INT_MIN / -1 row is discharged (#1598: proved where the divisor is positive, as in examples/safe_divide.vera, 7 in the corpus, else Tier 3, 8), a @Nat return is one record per value leaf it narrows at, each discharged under its own branch's conditions (7 records at the body become 12 at the leaves in the corpus), the measure's re-evaluation at a self tail call is the measure's record (2 fewer in the corpus), and two records at a call argument already of the formal's type go (examples/ephemeris.vera 488 and 489); over the corpus, Tier 1 2,423 to 2,483 and Tier 3 674 to 683, and the 29 W004 warnings and the one E541 the corpus carried are gone. A row no check can guard is disclosed, never counted: a decreases on an Exn row (#1530), a quantified ensures or one over a String or Array result (#1607), a refinement over a refinement, with the row's reason as the warning's rationale (#1602); E543 is the disclosure of such a contract or operation, beside E504 and E506 for a narrowing. Upgrade: a consumer that counted tier3_runtime or tier1_verified sees the moves above; a signed division whose divisor only a zero check excludes (requires(@Int.1 != 0), or a branch on the divisor being zero) moves from Tier 1 to Tier 3, its INT_MIN / -1 row left to the check, unless a fact excludes INT_MIN as the dividend; requires(@Int.1 > 0), as examples/safe_divide.vera has, proves it; a program that relied on E541 at an unguardable contract now gets a warning instead, and its exit status is 0.
• A closure written in a position code generation lowers at several sites (a measure at the entry and at each self tail call, a refinement predicate at each guard) is lifted once per function, so the module holds one copy and one check where it held one per site.
• The nightly mutation sweep measures a random sample of the mutants mutmut makes in vera/ instead of every one (#1827): each mutant is in a cycle's sample, 2% of them (SAMPLE_FRACTION), by a hash of the cycle, the function and its number, so every job of a night and every night of the cycle draw the same sample and the next cycle draws another; every function is counted by mutmut's own visitor through the engine's new count command before the plan, and each slice's record carries the counts for the stitch. A cycle closes in a night or two, and mutation-summary.csv and the badge's mutation.json carry the score's 95% Wilson interval beside each module's population. The sweep that measured every mutant decided 300 to 1,300 of about 113,000 a night, so a cycle would have taken months of green nights against a tree that changes daily.
• Both mutation lanes run every pytest session in a process of its own, process_isolation = "forkserver" in [tool.mutmut] (#1827): mutmut's default fork runner ran its stats pass, its test listing and its clean run as sessions of one process and forked the mutant workers from it, and state one session left behind broke the next on five nights (wasmtime's trap handlers put back by the faulthandler plugin, #1745 and #1747; a generator parametrisation consumed by the first collection, #1822). The fork server runs each session in a fresh child of a parent that never imports pytest; the [mutation] extra's floor is mutmut 3.8, which brought the option.
• The nightly mutation sweep draws its sample by line rather than by mutant (#1829): a line of a function is in a cycle's sample by a hash of the cycle, the function and the line, with every mutant on it, and a function's sampled lines reach mutmut as the diff lane's window does, so the copy holds the sample's mutants alone. A sample of mutants drawn one by one filled a job with bins of 150 to 200 functions, since mutmut generates a kept function's mutants whole, and those bins spent 30 minutes to four hours generating and compiling the copy before the first test ran. The sweep's state is schema 2: each function's mutants by line, numbered from the function's first so that an edit above it moves nothing, its identity the text it spans, and its sampled window's verdicts, a survivor named by the number mutmut gives it over the whole function and its line; a schema 1 state loads with its nights and starts every function and its cycle afresh; and the 21:00 UTC schedule runs again.
• Code generation reads only the obligation table's row for a refinement guard at a construction store or a handler clause binder (#1836). The roster of guarded positions (narrowing.REFINED_BIND_GUARDED_SITES) and the two gates that read it beside the row are gone; every position it named was a member at every reader, so no check moves.
• vera verify discharges every obligation from the obligation table's rows (#1836, Stage 27). The verifier's two walks are the two passes of one traversal that discharges a node only where the table lists a row there, each in the context it reaches the node in, and keys each record to its rows where it is made; the anchors that keyed records to rows afterwards, the fallback that discharged a row no record reached and the walk's own site decisions are gone. The verdicts are unchanged over the 323 corpus programs, record for record, with two moves outside it:
  • An operation or a call inside an assume condition is no obligation: an assume is not compiled, so a narrowing, a trapping operation or a call's precondition in its condition is never evaluated. vera verify reported an E503 for such a narrowing, an E501 for such a call, and an E532 warning for such a call whose precondition it cannot state, each with no record beside it; it now reports none of them, and the assume keeps its W003. Upgrade: a program whose only error was a narrowing or a call precondition inside an assume now verifies.
  • The INT_MIN / -1 overflow of a signed quotient written inside a refinement predicate is discharged at the declaration, with the predicate's other operations: { @Int | 100 / @Int.0 > 0 } reads its overflow Tier 1 where it read Tier 3.
• The obligation table, the first half of Stage 27 (vera/obligations/table.py, #1695): one pass over the typed program lists every obligation site once as a row, and code generation emits a runtime check for every row the table holds guardable and for no other node, deciding no guard of its own (WasmContext._record_check takes the row; EmittedCheck.row names it; a check with no row is a compiler invariant). Every vera verify verdict is what it was. The compiled module changes where the table and the old decisions disagreed: a bare put into a refined State cell on the intrinsic route takes the cell's predicate guard beside the sign guard (it took the sign guard alone, so a non-positive value reached a { @Int | @Int.0 > 0 } cell); a handler clause binder over an Array, Map or Set payload declared narrower than the payload is walked at run time, and the verifier records it; a later element of an array literal coerced to the literal's element type by the first element ([@Nat.0, @Int.0]) is guarded; a §2.6.5 guard on a value already of the refined type (a refined slot stored into a field of its own type, or bound by a let of its own type) is no longer emitted, since the slot's own binding is checked; the use of a guarded handler clause binder at a @Nat formal is no longer guarded a second time; and the decreases self-tail prefix is rendered only where a tail call splices it, so a function with no self tail call, or with a runtime postcondition, no longer carries its dead locals. effect_bind joins the obligation kinds: a match arm binder bound at a function type whose effect row is narrower than its field's (#1725), a row no runtime check can evaluate, listed by the table and disclosed by the second half.
• A call precondition refuted only over a stand-in is a runtime check in every position (#1696). The rule of #804, under which a function body's call over an opaque value was refused with E501 whatever the value, is retired: such a call takes the E532 demotion, with the callee's own check behind it, and is E501 only where the precondition is false for every value the stand-in could take. A program refused at such a call now verifies with one more runtime check. The E522 postcondition warning and the E504/E506 undecided rationale name a stand-in for a value the verifier cannot translate, where they named an effect operation's.
• safe_divide's requires is @Int.1 > 0, so its division proves whole. @Int.0 / @Int.1 traps on two divisors, zero and -1 under INT_MIN, and the verifier obligates the first (E526) but not yet the second (#1598), so requires(@Int.1 != 0) left one input to a trap while the landing page says the clause makes the division proved. A positive divisor excludes both. examples/safe_divide.vera, README.md, SKILL.md, EXAMPLES.md, FAQ.md, PYPI_README.md, spec chapters 5 and 6 and the landing page carry the new clause, and every documented call keeps a positive divisor; spec chapter 5's two-requires variant now verifies and runs to 5, where its ensures(@Int.result >= 0) failed under a negative divisor. The examples whose point is the zero-divisor obligation itself (FAQ.md's answer on primitive operations, SKILL.md's fn divide, spec chapter 6's apply_div and the ch06_requires and ch04_primitive_obligations conformance programs) keep @Int.1 != 0.
• The nightly full matrix is a workflow of its own, and every gating job runs on a pinned image (.github/workflows/nightly-matrix.yml). The nightly run was a schedule of ci.yml's own, so each night's completion started a run of release.yml whose gate skipped every job (run 40857508689 on 2026-10-29). Nightly matrix calls ci.yml with nightly: true on the same cron and on demand, and a called workflow's jobs run inside its caller's run, so the release hears CI's push and pull-request runs alone and the matrix keeps one definition. Every gating runs-on names an explicit image: ubuntu-latest gives way to ubuntu-24.04, and windows-latest to windows-2025-vs2026, the Windows Server 2025 image that label and windows-2025 name since June 2026, so the five required shard checks are named test (ubuntu-24.04, 3.12, shard K/3) and test (windows-2025-vs2026, 3.12, shard K/2). The nightly run also watches the floating ubuntu-latest, windows-latest and macos-latest labels and Ubuntu 26.04 under Python 3.12 (the watch job): advisory cells whose failure on a scheduled night files an issue and blocks nothing, and the issue names the image each failed cell ran on (ImageOS, ImageVersion).

Fixed

• A judgement on what an earlier diagnostic refused reports nothing further (#1563). A bare call to a name a function refused for redefining a built-in took (E151) is no longer held to the built-in's signature, which drew E202, E314 and E313 at the call; a data declaration refused for taking a built-in type's name (E158), Map, Set, Array, Decimal, Tuple or Future, is not registered, as a primitive's never was, so its constructor builds no value of the built-in (let @Bool = Wrap(1) was E170, "value has type Map") and @Map<String, Int> keeps the built-in's type arguments (E135), above the declaration as below it; a type name nothing declares (E136) is compatible with every type, as an unknown is, through a generic's substitution too, so the let, return, argument, destructure, comparison and operator (+, -, <, an index) that name it draw no E170, E121, E202, E142, E243, E140, E147, E143 or E161, nor a requires (E123), an effect operation's argument (E204) or apply_fn (E202), every early guard reading one shared predicate; and a match or a destructuring let over a typed hole is not judged for coverage, so match ? { Some(@Int) -> @Int.0, None -> 0 } and let Tuple<@Int, @Int> = ?; report the hole's W001 alone, not E313 beside it. In the verifier, a refused binder holds its predicate for the rest of its scope in every spelling: a @Nat binder's sign, guarded at the bind, as a refined binder's predicate (Some(@Nat) -> need_nn(@Nat.0) drew E501 beside its E503), and a destructure's component as a let's binder, in every walk that reads one (let Tuple<@Pos, @Int> = Tuple(@Int.0 - 5, 1); need_pos(@Pos.0) drew E501 beside its E505), and a guarded binder's fact reaches a query through another guarded binder's fact that names it. The same reading closes #1696's destructure line: a component of a stand-in, let Tuple<@Pos, @Int> = Tuple(get(()), 1), discharges the call its let @Pos = get(()) twin discharges, where it was a Tier 3 runtime check (E532).
• A match arm binder bound at a function type whose effect row is narrower than its field's (an <IO> closure field bound at a pure closure type) is disclosed by vera verify as E542, neither proved nor checked at run time, with the fix to bind the field at its own type; it was silent (#1725's line of #1695). The refusal at check is v0.3.0's.
• A refined binder whose bind is guarded or refused holds its predicate for the rest of its scope, so a call that needs it is no second error (#1563's verifier half), and an index whose bounds check guards it is in range where its element is read (#1696's m04); a throw arm or a join of them is no obligation, so no dead guard follows a throw.
• A handler clause's guarded @Nat binder is one record, and its use at a @Nat formal none (#1782); a call_pre inside a callee's ensures is the callee's (#1567); each guarded component of a tuple-typed argument is its own record (#1642); a verifier diagnostic at a piped stage stands at the stage (#1641); a map_insert value outside a let (#1608) and a payload nested in a container literal (#1613) are recorded where they are guarded.
• A goal over a Float64 stand-in is undecided without asking Z3 (#1696). A value the verifier cannot translate at Float64, such as int_to_float(@Int.0), is a stand-in carrying no fact a refutation may rest on, and a goal over it was asked as a floating-point query that took 1 to 4 s to return the countermodel the rule then set aside; it is Tier 3 without the query, as a symbolic floating-point argument of float_to_int already was. vera verify examples/maximum_syntax.vera takes 1.6 s where it took 9.1 s, its two such goals at the same tier. A call's result over such a stand-in still carries its callee's ensures and is asked, so examples/ephemeris.vera's right_ascension, whose range comes back through wrap_deg, still proves; a goal true for every float value over the stand-in itself no longer proves, and no corpus program has one. The issue's other open line, a destructured component of a stand-in, closes with #1563's reading of a refused binder; its Array<Nat> element line moves to #1814.
• A refuted postcondition's counterexample prints the result the body gives at the printed input (#1707). An ensures is asked with the body's term in place of @T.result, so the declared result constant was in no query and the counterexample printed it as the model left it: @Int.result = 0 beside @Option<Int>.0 = Some(2) for a match that returns 2, and 0 (or False) for every refuted ensures whatever the body's shape. It is now the model's value of the body's term: 2 there, 13 for @Int.0 + 10 at @Int.0 = 3, 5 for @Int.1 - @Int.0 at 7 and 2, 1 for a call whose callee's ensures says so.
• A refinement the type checker recorded a join at is no longer a premise of the value: an if, match, block or handle is established at the one type its leaves share, and at its base where they differ (#1716). A payload handed on as g(if c then { @Option<Int>.0 } else { None }) into an @Option<PosInt> formal, returned or bound by let that way, or a State handler in a match arm returned at @Option<PosInt>, read verified while the run broke the payload; each is now refuted (E505). An Exn handler whose body joins an @Int and a @PosInt no longer proves ensures(@Int.result > 0) from its recorded PosInt; the postcondition is a runtime check (E522), as it was before #1833.
• A generic instantiated at a function type is compiled (#1783). A call that passes a closure, or a value of a function type, for a generic's type parameter passed vera check and vera verify, and code generation refused the clone (E600 at a parameter, E601 at a return) and dropped every function that called it (E620), so vera run had nothing to run. A clone spells its type arguments by name, and the width of a type expression was read from the name, which nothing answered for fn(Int -> Int); it is now read from the typed program, where a function type is a closure pointer. idg(fn(@Int -> @Int) effects(pure) { @Int.0 * 2 }) for forall<T> fn idg(@T -> @T) returns the closure, and the prelude's option_unwrap_or at an Option of a function type, a function type at an Array element, a data type's field, a Map value, a State cell or an Exn payload inside a generic, and a generic where helper each compile and run. No example, conformance program or documentation example changes verdict or emitted WebAssembly.
• The nightly mutation sweep decides mutants again after it drops a test from the oracle (#1822). tests/test_composite_coercion_guards.py parametrised one test over a generator, which has its cells in the first collection of a process alone; mutmut runs its stats pass, its listing and its clean run as sessions of one process, so on a night's rerun the clean run asked for 172 cells its collection no longer had, pytest answered with its usage-error exit, and three nights decided no mutant. The instrument parametrises over a list; pytest's PytestRemovedIn10Warning, which names every such usage, is an error in the suite's configuration, so the pull-request gate refuses the next one; the sweep's own tests collect the oracle twice in one interpreter and ask for every recorded id the second time; and the sweep names an exception that ends the engine's log in its record, where this stop was recorded with no name. Beside it, two nights' finds take their fixes: the generator models an if whose branch holds a let the verifier does not translate as the unconstrained value the verifier sees (#1696's member of 2026-11-02, generator seed 2900205), and the distrust corpus's mode differential compares what --distrust decides about a function it does not distrust rather than the trials Z3 drew, which two runs of one process can draw apart (#1785).
• The nightly mutation sweep no longer spends a slice's budget rediscovering the tests that read the compiler's source (#1827): tests/mutation_oracle.py skips such a test inside mutmut's copy at the read (open, pathlib or inspect.getsource of a .py file under source_paths), as it skips one that starts a process, lists it apart and takes it out of mutmut's record of the tests that reach each function; a test dropped from the oracle on an earlier night is deselected from the start of every night after, until the tree no longer holds its file; and the five tests [tool.mutmut] deselected by hand are the plugin's to skip. On 3 November 2026 four slices each dropped the same four tests at the price of a stats pass apiece, five stats passes of about an hour, and decided nothing.
• A lost runner is weather for the nightly mutation sweep (#1827): a slice with no record is noted and its work waits for the next night, and only more than two in one night stop the night short, where four over seven nights did against a measured rate of about 7% of the sweep's 4.5-hour jobs; and a slice whose budget runs out before its first mutant is a stop the stitch reports, so a green night cannot hide it.
• A refinement unifies by its base, on either side of a call's argument judgement and at every level of the type (two lines of #1684). Type-argument inference unwrapped a refinement only on the argument's side against a data-type parameter, so a refined function type at a function-typed parameter left the callee's variable unbound, and a parameterised refinement alias at a parameter bound nothing: with type Foo = { @fn(Int -> Int) effects(pure) | true }, array_map([1], @Foo.0) was refused with E202 (expected fn(Int -> B)), and with type NE<T> = { @Array<T> | array_length(@Array<T>.0) > 0 } and forall<T> fn head_of(@NE<T> -> @T), head_of(@NE<Int>.0) + 1 was E140 (found ? and Int) while nat_to_int(string_length(head_of(["abc", "d"]))) passed vera check and vera verify and built a module that did not load. A refinement on either side now unifies by its base at every level, in every branch of the type (a data type, a function type, a tuple, an Array, a Map), so B is bound to Int, head_of is recorded at Int and at String, and the three programs run; the refinement's predicate stays the obligation the binding site records (refine_bind). A constructor's field unifies by the same rule: with data Holder<T> { Holder(NE<T>) }, Holder(["hello"]) binds T to String and runs, where it was refused with E213 (field 0 has type Array<String>, expected {@Array<T> | ...}). A result such a call typed as a wildcard is held to its type: let @String = array_map([1], @Foo.0)[0] is E170. No example, conformance program or documentation example changes verdict.
• One rule for an expression the verifier cannot translate (#1696, the lines of #1470, #1571, #1595 and #1601 among them). An expression outside the decidable fragment — a closure applied through apply_fn, an effect operation's result, a generic call, a fold, a Map or Set built in place, a match on map_get's result, a refinement predicate calling a host function — is one stand-in of its checked type's sort, named by the expression and read as one term by every pass, carrying its type's facts: Nat's >= 0, and a refinement's translatable conjuncts over any base (hd(@NEI.0) under type NEI = { @Array<Int> | array_length(@Array<Int>.0) > 0 } proves against a callee's requires of the same predicate). The context translates around it: a branch's facts hold under the condition's stand-in, a match arm runs under the earlier arms' negations and its binders read the payload's declared type, a call with a stand-in argument keeps its ensures, a literal keeps its length, and a State handler whose clauses each resume once has its body's value. A refutation that rests on a stand-in reports the obligation undecided, for every kind, unless the goal is false for every value the stand-in could take: one whose goal names a stand-in, that runs under a condition naming one, or that needs one at a single value. A refutation tied to a stand-in only through an assert over a range of the goal's own inputs still stands. A callee's ensures is no longer assumed on runs that never make the call (#1571's false Tier 1 is a runtime check), an assume over a let-bound call reaches the ensures (#1601), a recursive call with an untranslatable argument keeps its decreases and precondition proofs (#1595), and a refutation no longer rests on a value the type forbids (#1470).
• Both mutation lanes let mutmut's copy cache bytecode, and tests/mutation_oracle.py records each test that fails in the stats pass or the clean run to a file the lane reads (#1829). A mutated module compiles in tens of seconds (vera/checker/calls.py with its mutants inlined is 24 MB and takes 47 s) and loads from its .pyc in a fifth of a second, and under the fork server every pass and every mutant's worker is a fresh process that compiled each mutated module it reached, which made a mutant cost three to ten times what it had; and the fork server's stats child kept its pytest output from the log, so a test that failed in the copy stopped the slice as an engine failure with no name instead of being dropped.
• A negative component no longer reaches a @Nat component through a composite coercion (#1542, #1695). The checker admits a value whose type holds an @Int where its position's type holds a @Nat: an Option<Int> at an Option<Nat> formal, let @Option<Nat> = @Option<Int>.0, a W(@Int.0) inside an array literal bound at Array<Wrap<Nat>>, a binder declared Tuple<Int, Nat> over a Tuple<Int, Int> field, a map key or value or a set element. Nothing obligates the component, and v0.2.6 guarded it nowhere, so vera verify passed and vera run returned a negative from a @Nat function; v0.2.5 had trapped most of these positions only through guards placed on the read side by accident. Code generation now guards every such component by one rule over the typed program: a construction's component where it is stored, an opaque value (a slot, a call's result, an index, a field read) by a walk of every differing component (Some, the differing side of a Result, a tuple's or a record's field, every constructor's field of a data type, every element of an Array, every key, value or element of a Map or Set, a Future's payload), and a pattern binder, a destructure or a handler clause binder declared narrower than what it binds by a walk of the bound value. A negative component traps as a scalar narrowing does, Negative value bound into a @Nat slot (E800 at vera run). A store's in-place guard, a nested literal's hand-down and a function boundary's tuple-component guard stand where they stood, and the rule adds none beside them. vera verify reports each new guard as W004 (a check with no record) until the obligation table (#1695) records the coercion. A Map or Set coercion's guard reads the collection through the same projections map_keys, map_values and set_to_array use, so it is O(n) in the collection's size and allocates. Two positions stay unguarded and disclosed: a handler clause binder over an Array, Map or Set payload keeps its E506, and a function type gaining a @Nat component (fn(Int -> Int) at fn(Int -> Nat)) has no value a walk can read where the function is passed (#1819: v0.3.0 refuses it).