aallan · aallan · Jul 28, 2026 · Jul 28, 2026 · Jul 28, 2026 · Jul 28, 2026
@@ -6,6 +6,14 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 
 ## [Unreleased]
 
+### Documentation
+
+- **The VeraBench section carries the v0.0.18 sweep** ([#1169](https://github.com/aallan/vera/pull/1169)), the first in which all 60 problems are graded — v0.0.17 took the gradeable set from 36 to 46 and v0.0.18 closed it. One problem is now worth 1.7 percentage points rather than 2.8. Six of the nine models solve every Vera problem, and Vera is highest or level with it for six of the nine. Measured against [Vera v0.1.8](https://github.com/aallan/vera/releases/tag/v0.1.8). The section also gains the reading the wider gradeable set supports: Python is dynamically typed and TypeScript is not, Vera sits with TypeScript and goes further, and sorting the three by how much they constrain the model rather than by how much of them it has read puts the two constraining languages ahead — TypeScript with training data behind it, Vera without.
+
+  Every figure was cross-checked cell by cell against [vera-bench#120](https://github.com/aallan/vera-bench/pull/120), the pending results rewrite in the benchmark repo; all 27 published cells agree, as do both headline counts. The landing page's numbers and the benchmark repo's are the same measurement, not two independent transcriptions of it.
+
+  Propagated to every surface that carries the figures, which the HTML edit alone does not reach: `build_index_md()` in `scripts/build_site.py` — the generator that *is* `docs/index.md`, since that file is not derived from the HTML — plus `README.md` and `FAQ.md`, then `docs/index.md` and `docs/llms-full.txt` regenerated. This is the drift class [#1154](https://github.com/aallan/vera/issues/1154) describes: `check_site_assets.py` regenerates from the same function it compares against, so a stale generator validates as up to date and only a reader notices.
+
 ## [0.1.8] - 2026-07-27
 
 ### Added

@@ -187,11 +187,11 @@ HTTP, JSON, and Markdown are now built-in, which supports the primary agent work
 
 ## Is there evidence this actually works?
 
-Vera-specific benchmark data is now available across multiple models. **[VeraBench](https://github.com/aallan/vera-bench)** — a 60-problem benchmark across 5 difficulty tiers — covers 9 models across 3 providers (v0.0.16). The headline result: seven of the nine write 100% correct Vera, a language none of them was trained on. Against Python, Vera wins outright for four of the nine models, draws with three and loses two. The metric is **% solved** (pass@1): a refusal, a compile failure, a crash and a wrong answer all count alike as not solved, so a model cannot score higher by answering less.
+Vera-specific benchmark data is now available across multiple models. **[VeraBench](https://github.com/aallan/vera-bench)** — a 60-problem benchmark across 5 difficulty tiers — covers 9 models across 3 providers (v0.0.18). The headline result: six of the nine write 100% correct Vera, a language none of them was trained on. Vera has the highest score, or level with it, for six of the nine models. The metric is **% solved** (pass@1): a refusal, a compile failure, a crash and a wrong answer all count alike as not solved, so a model cannot score higher by answering less.
 
 The sharpest evidence that the design choices are doing the work is Vera against [Aver](https://averlang.dev), a second language that is also absent from every training set and also learned from a single document in the prompt — so familiarity cannot explain a difference between them. What separates them is that Aver has ordinary variable names where Vera has typed slot references. Vera scores higher on all five models that ran both. The two languages differ in more than one respect, so this isolates the variable better than the Python comparison without isolating it completely.
 
-These caveats matter: single run per model, no pass@k, and the headline is measured over the 36 problems that can be output-graded, where one problem is worth 2.8 percentage points — so most of the gaps are one or two problems wide. Stable rates will require pass@k evaluation with multiple trials — see the [full report](https://github.com/aallan/vera-bench) for details.
+These caveats matter: single run per model, no pass@k. v0.0.18 is the first sweep in which all 60 problems are graded, so one problem is worth 1.7 percentage points — which narrows the increment but does not remove the caveat, since most of the gaps are still one or two problems wide. Stable rates will require pass@k evaluation with multiple trials — see the [full report](https://github.com/aallan/vera-bench) for details.
 
 The broader literature is also encouraging. The type-constrained decoding paper (Mündler, He, Wang et al., "Type-Constrained Code Generation with Language Models", PLDI 2025, [ACM DL](https://dl.acm.org/doi/10.1145/3729274)) found that enforcing type constraints during LLM code generation cut compilation errors by more than half and improved functional correctness by 3.5–4.5%. Syntax constraints alone provided limited improvement — it was the *type* constraints that made the difference. The same paper found that 94% of LLM-generated compilation errors are type-check failures — exactly the class of error that a strong static type system catches at compile time.
 

@@ -269,7 +269,7 @@ The reference compiler — parser, AST, type checker, contract verifier (Z3), WA
 
 **Key features delivered:** [typed De Bruijn indices](DE_BRUIJN.md) (`@T.n`), mandatory contracts, algebraic effects (IO, Http, HttpServer, State, Exceptions, Async, Inference, DB, Random, Diverge), refinement types, constrained generics (Eq, Ord, Hash, Show), algebraic data types, pattern matching, modules, 164 built-in functions (strings, arrays, maps, sets, decimals, math, JSON, HTML, Markdown, regex, base64, URL), contract-driven testing, canonical formatter, browser runtime, three-tier verification design (Z3 static and runtime fallback shipped; the Z3-guided tier is specified, not yet implemented), a [language server](LSP_SERVER.md) with warm incremental verification and agent-facing proof-delta methods, and contract-verified HTTP handlers served natively (`vera serve`) or as wasi:http components for stock `wasmtime serve` (`--target wasi-p2 --world server`).
 
-**What's next:** the path from "working language" to "the language agents actually use" — see **[ROADMAP.md](ROADMAP.md)** for the four strategic milestones. The flagship goal is a verified MCP tool server where contracts guarantee tool schemas at compile time. **[VeraBench](https://github.com/aallan/vera-bench)** — a 60-problem benchmark across 5 difficulty tiers — now covers 9 models across 3 providers (v0.0.16). The headline result: seven of the nine write 100% correct Vera, a language none of them was trained on. Against Python, Vera wins outright for four of the nine models, draws with three and loses two. The metric is **% solved** (pass@1): a refusal, a compile failure, a crash and a wrong answer all count alike as not solved. These are single-run results over the 36 output-gradeable problems, where one problem is worth 2.8 percentage points — see the [full report](https://github.com/aallan/vera-bench) for details.
+**What's next:** the path from "working language" to "the language agents actually use" — see **[ROADMAP.md](ROADMAP.md)** for the four strategic milestones. The flagship goal is a verified MCP tool server where contracts guarantee tool schemas at compile time. **[VeraBench](https://github.com/aallan/vera-bench)** — a 60-problem benchmark across 5 difficulty tiers — now covers 9 models across 3 providers (v0.0.18). The headline result: six of the nine write 100% correct Vera, a language none of them was trained on. Vera has the highest score, or level with it, for six of the nine models. The metric is **% solved** (pass@1): a refusal, a compile failure, a crash and a wrong answer all count alike as not solved. This is the first sweep in which all 60 problems are graded, so a single problem moves a score by 1.7 percentage points and most gaps are one or two problems wide — see the [full report](https://github.com/aallan/vera-bench) for details.
 
 Known bugs and open issues are tracked on the **[issue tracker](https://github.com/aallan/vera/issues)**. See **[KNOWN_ISSUES.md](KNOWN_ISSUES.md)** for a consolidated list.
 

@@ -422,12 +422,12 @@ <h2>What Vera Looks Like</h2>
       <div class="eyebrow"><span class="slot">@section.03</span> · empirical evidence</div>
       <h2>VeraBench</h2>
       <div class="bench-masthead">
-        <p class="bench-stat">Seven of nine frontier models write <b>100% correct</b> Vera &mdash; a language none of them has ever been trained on.</p>
+        <p class="bench-stat">Six of nine frontier models write <b>100% correct</b> Vera &mdash; a language none of them has ever seen before.</p>
         <img src="vera-bench-meerkat-only.png" alt="VeraBench meerkat" class="bench-meerkat" width="542" height="640" loading="lazy">
       </div>
 
       <div class="bench-body">
-        <p style="color:var(--ink-500)">A 60-problem benchmark across 5 difficulty tiers &mdash; pure arithmetic, strings and arrays, ADTs and exhaustive matching, recursion with termination proofs, multi-function effect propagation. Nine models, three providers, four modes each. The table reports <b>% solved</b>: the model wrote code, it compiled, it ran, and the output matched. A refusal, a compile failure, a crash and a wrong answer all count alike as not solved.</p>
+        <p style="color:var(--ink-500)">A 60-problem benchmark across 5 difficulty tiers &mdash; pure arithmetic, strings and arrays, ADTs and exhaustive matching, recursion with termination proofs, multi-function effect propagation. Nine models, three providers, four modes each: Vera written against a full specification, Vera written from a plain English description with the model authoring its own contracts, and the same problems in Python and TypeScript. The table shows three of the four, and reports <b>% solved</b>: the model wrote code, it compiled, it ran, and the output matched. A refusal, a compile failure, a crash and a wrong answer all count alike as not solved.</p>
 
           <table class="bench-table">
             <thead>
@@ -441,32 +441,32 @@ <h2>VeraBench</h2>
               <tr>
                 <td class="lang">Claude Fable 5 <span class="tag">ceiling</span></td>
                 <td class="win">100%</td>
-                <td class="loss">94%</td>
-                <td class="loss">92%</td>
+                <td class="loss">97%</td>
+                <td class="loss">97%</td>
               </tr>
               <tr>
                 <td class="lang">GPT-5.6 Sol (pro) <span class="tag">ceiling</span></td>
                 <td>100%</td>
-                <td class="loss">97%</td>
+                <td class="loss">95%</td>
                 <td>100%</td>
               </tr>
               <tr class="sep">
                 <td class="lang">Claude Opus 5 <span class="tag">flagship</span></td>
-                <td class="win">100%</td>
-                <td class="loss">94%</td>
-                <td class="loss">94%</td>
+                <td>100%</td>
+                <td class="loss">95%</td>
+                <td>100%</td>
               </tr>
               <tr>
                 <td class="lang">Claude Opus 4.8 <span class="tag">flagship</span></td>
-                <td class="loss">94%</td>
-                <td>100%</td>
-                <td>100%</td>
+                <td class="loss">93%</td>
+                <td class="loss">98%</td>
+                <td class="win">100%</td>
               </tr>
               <tr>
                 <td class="lang">GPT-5.6 Sol <span class="tag">flagship</span></td>
-                <td>100%</td>
-                <td class="loss">97%</td>
-                <td>100%</td>
+                <td class="loss">98%</td>
+                <td class="loss">95%</td>
+                <td class="win">100%</td>
               </tr>
               <tr>
                 <td class="lang">Kimi K3 <span class="tag">flagship</span></td>
@@ -477,32 +477,36 @@ <h2>VeraBench</h2>
               <tr class="sep">
                 <td class="lang">Claude Sonnet 5 <span class="tag">workhorse</span></td>
                 <td class="loss">97%</td>
-                <td>100%</td>
-                <td>100%</td>
+                <td class="loss">98%</td>
+                <td class="win">100%</td>
               </tr>
               <tr>
                 <td class="lang">GPT-5.6 Terra <span class="tag">workhorse</span></td>
                 <td>100%</td>
-                <td>100%</td>
+                <td class="loss">95%</td>
                 <td>100%</td>
               </tr>
               <tr>
                 <td class="lang">Kimi K2.6 <span class="tag">workhorse</span></td>
                 <td>100%</td>
-                <td>100%</td>
+                <td class="loss">97%</td>
                 <td>100%</td>
               </tr>
             </tbody>
           </table>
 
-          <p class="bench-caveat">Frontier models now write Vera <strong style="color:var(--ink-900)">as well as they write the languages they were trained on, and in a good many cases better</strong>. Vera wins outright for four of the nine models, draws with three and loses two.</p>
+          <p class="bench-caveat">Frontier models now write Vera <strong style="color:var(--ink-900)">as well as they write the languages they were trained on</strong>. Vera has the highest score, or level with it, for six of the nine models.</p>
 
-          <p class="bench-caveat" style="margin-top:.75rem">Mandatory contracts and typed slot references appear to provide enough structure to compensate for zero training data. Every green bar below was earned from a single document in the prompt, by a model that had never seen the language before.</p>
+          <p class="bench-caveat" style="margin-top:.75rem">Mandatory contracts and typed slot references appear to provide enough structure to compensate for zero training data. Every successful program came from a single skill file in context, written by a model that had never seen the language before.</p>
 
           <a href="https://github.com/aallan/vera-bench"><img src="verabench-delta-chart.png" alt="Does Vera beat Python / TypeScript?" class="bench-chart" loading="lazy" width="2689" height="1302"></a>
 
-          <p class="bench-caveat">Still early days. The benchmark is just a single run per model, no pass@k, and with 36 output-gradeable problems one problem is worth just under three percentage points, so most of the gaps above are only one or two problems wide. However it looks like language design can, at least sometimes, outweigh sheer volume of training data. Which, if you're in the business of generating code at any scale, is a reasonably interesting thing to be true.</p>
-          <p class="bench-caveat" style="margin-top:.75rem">Results from <a href="https://github.com/aallan/vera-bench#results">VeraBench v0.0.16</a> against <a href="https://github.com/aallan/vera/releases/tag/v0.1.7">Vera v0.1.7</a>. Inspired by <a href="https://github.com/openai/human-eval">HumanEval</a>, <a href="https://github.com/google-research/google-research/tree/master/mbpp">MBPP</a>, and <a href="https://github.com/sun-wendy/DafnyBench">DafnyBench</a>.</p>
+          <p class="bench-caveat">The difference between the Python and TypeScript results is probably not random. Python is dynamically typed, so a type error surfaces when the code runs; TypeScript is statically typed and rejects the same error before anything runs. Vera sits with TypeScript but goes further, making <code>requires</code>, <code>ensures</code> and <code>effects</code> mandatory on every function and replacing variable names with typed slot references. Sort the three languages by how much they constrain the model rather than by how much of them it has read, and the ordering stops looking accidental: the two languages that constrain the model finish ahead of the one that doesn't.</p>
+
+          <p class="bench-caveat" style="margin-top:.75rem">TypeScript earns its results due to its inclusion in model training data. Vera earns very nearly the same results without that. Whatever familiarity is buying TypeScript, the additional constraints Vera provides appear to be supplying by other means.</p>
+
+          <p class="bench-caveat">It's still early days. The benchmark is just a single run per model, no pass@k; and with just sixty problems each problem is worth just under two percentage points, so most of the gaps above are only one or two problems wide. However, it looks like language design can, at least sometimes, outweigh sheer volume of training data. Which, if you're in the business of generating code at any scale, is a reasonably interesting thing to be true.</p>
+          <p class="bench-caveat" style="margin-top:.75rem">Results from <a href="https://github.com/aallan/vera-bench#results">VeraBench v0.0.18</a> against <a href="https://github.com/aallan/vera/releases/tag/v0.1.8">Vera v0.1.8</a>. Inspired by <a href="https://github.com/openai/human-eval">HumanEval</a>, <a href="https://github.com/google-research/google-research/tree/master/mbpp">MBPP</a>, and <a href="https://github.com/sun-wendy/DafnyBench">DafnyBench</a>.</p>
           <p style="margin-top:1.25rem"><a href="https://github.com/aallan/vera-bench" class="btn btn-primary"><svg viewBox="0 0 16 16" fill="currentColor" aria-hidden="true"><path d="M8 0C3.58 0 0 3.58 0 8c0 3.54 2.29 6.53 5.47 7.59.4.07.55-.17.55-.38 0-.19-.01-.82-.01-1.49-2.01.37-2.53-.49-2.69-.94-.09-.23-.48-.94-.82-1.13-.28-.15-.68-.52-.01-.53.63-.01 1.08.58 1.23.82.72 1.21 1.87.87 2.33.66.07-.52.28-.87.51-1.07-1.78-.2-3.64-.89-3.64-3.95 0-.87.31-1.59.82-2.15-.08-.2-.36-1.02.08-2.12 0 0 .67-.21 2.2.82.64-.18 1.32-.27 2-.27.68 0 1.36.09 2 .27 1.53-1.04 2.2-.82 2.2-.82.44 1.1.16 1.92.08 2.12.51.56.82 1.27.82 2.15 0 3.07-1.87 3.75-3.65 3.95.29.25.54.73.54 1.48 0 1.07-.01 1.93-.01 2.2 0 .21.15.46.55.38A8.013 8.013 0 0016 8c0-4.42-3.58-8-8-8z"/></svg>vera-bench</a></p>
       </div>
     </div>