diff --git a/AGENTS.md b/AGENTS.md
index 27b5a836..52738d7c 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -103,7 +103,7 @@ import opened Std.Arithmetic.DivMod     // LemmaMulStrictInequality(x,y,z): x<y
                                         // LemmaModMultiplesBasic(m,p): m>=0 && p>0 ==> (m*p)%p == 0
 ```
 
-`lsc`'s `dafnyVerify` (`tools/dist/dafny-commands.js`) **auto-adds `--standard-libraries` whenever the `.dfy` text contains the substring `Std.`** — so an `import opened` is all you need; no CLI flag or config change, and `lsc check` picks it up. The imports go in as an *inserted* block (additions-only — don't touch the generated header). Euclidean identities (`x == x/p*p + x%p`, `0 <= x%p < p`) and small distributivity (`(k+1)*p == k*p + p`) *are* reliable inline; reserve the library for the cancellation and monotonicity goals.
+`lsc`'s `dafnyVerify` (`tools/dist/dafny-commands.js`) **auto-adds `--standard-libraries` whenever the `.dfy` text contains the substring `Std.`** — so an `import opened` is all you need; no CLI flag or config change, and `lsc check` picks it up. (Exception: a project with `"string-semantics": "javascript-utf16"` cannot use `Std.*` — Dafny's standard library does not load under `--unicode-char:false`; `lsc check` refuses the combination with a message naming the key.) The imports go in as an *inserted* block (additions-only — don't touch the generated header). Euclidean identities (`x == x/p*p + x%p`, `0 <= x%p < p`) and small distributivity (`(k+1)*p == k*p + p`) *are* reliable inline; reserve the library for the cancellation and monotonicity goals.
 
 ## Lean verification workflow
 
diff --git a/DESIGN_CONFIG.md b/DESIGN_CONFIG.md
index 810af9a6..f07db4f8 100644
--- a/DESIGN_CONFIG.md
+++ b/DESIGN_CONFIG.md
@@ -1,6 +1,6 @@
 # DESIGN_CONFIG — Project options via `lemmascript.json`
 
-**Status:** initial implementation complete. The registry, `extern-default`, `safe-slice`, `proof-dir`, file overrides, and `lsc config` are implemented. #211 (Dafny strings as JavaScript UTF-16 code units) and #205 (JavaScript number semantics) remain future users of the mechanism and are not implemented here.
+**Status:** implemented. The registry supports `extern-default`, `safe-slice`, `proof-dir`, file overrides, and `lsc config`. PR #211 adds `string-semantics` and `dafny-library`, including their compatibility check. #205 (JavaScript number semantics) remains a future user of the mechanism.
 **Date:** August 2026
 
 ## Requirements
@@ -50,6 +50,8 @@ export const OPTION_SPECS = {
   "extern-default": { type: "enum", values: ["pure", "impure"], default: "pure", fileOverride: true, description: "…" },
   "safe-slice":     { type: "boolean", default: false, fileOverride: true, directiveAliases: ["safe-slice"], description: "…" },
   "proof-dir":      { type: "path", default: null, fileOverride: false, description: "…" },
+  "string-semantics": { type: "enum", values: ["unicode-scalar", "javascript-utf16"], default: "unicode-scalar", fileOverride: true, description: "…" },
+  "dafny-library":  { type: "enum", values: ["stdlib", "local"], default: "stdlib", fileOverride: true, description: "…" },
 } as const;
 
 export type LscOptions = { readonly [K in keyof typeof OPTION_SPECS]: /* boolean | enum union | string | null */ };
@@ -58,12 +60,12 @@ export const DEFAULT_OPTIONS: LscOptions;
 
 export function validateOptions(raw: unknown, source: string): ExplicitOptions; // per-key checks; returns only explicit keys
 export function parseFileOptions(sourceText: string, source: string): ExplicitOptions;
-export function resolveOptions(explicit: ExplicitOptions, source: string): LscOptions; // defaults + dependent defaults + cross-key checks
+export function resolveOptions(explicit: ExplicitOptions, source: string): LscOptions; // defaults + cross-key checks
 export function loadConfigOptions(sourcePath: string, configPath?: string): { explicit: ExplicitOptions; configFile: string | null };
 export function resolveDafnyArtifactDir(sourcePath: string, configFile: string | null, options: LscOptions): string;
 ```
 
-`validateOptions` and `parseFileOptions` return only the keys that were present. `lsc.ts` merges those two partial objects, file over config, and calls `resolveOptions` once, so future dependent defaults can distinguish an explicit setting from a default. `resolveOptions` applies dependent defaults and then rejects cross-key contradictions; the message names the conflicting explicit settings and the fix. The file parser uses the registry's types, enum values, and `fileOverride` field rather than maintaining a second switch; its only special cases come from declared `directiveAliases`. The `path` type accepts a non-empty relative string; the artifact helper anchors it at the selected config file and performs the containment check from §3.3.
+`validateOptions` and `parseFileOptions` return only the keys that were present. `lsc.ts` merges those two partial objects, file over config, and calls `resolveOptions`. It fills registry defaults and then rejects cross-key contradictions; the message names the conflicting settings and the fix. The file parser uses the registry's types, enum values, and `fileOverride` field rather than maintaining a second switch; its only special cases come from declared `directiveAliases`. The `path` type accepts a non-empty relative string; the artifact helper anchors it at the selected config file and performs the containment check from §3.3.
 
 Adding an independent option is: one registry entry, then `options["<key>"]` in the consuming phase, then a row in SPEC.md §7 and a fixture. An interacting option also adds its dependent-default or incompatibility rule to `resolveOptions` and a negative fixture; consumers still receive only a valid, fully resolved set.
 
@@ -102,21 +104,24 @@ The source must be inside the config directory when `proof-dir` is set (includin
 
 Enabling the option must not silently strand proof additions. If the mapped `.dfy` is absent but a sibling `.dfy`, `.dfy.base`, or `.dfy.merged` exists beside the TS, `lsc` fails with paths and tells the user to move the hand-written `.dfy`, discard or inspect merge-state files, and rerun; `.dfy.gen` is regeneratable. Changing from one non-default proof directory to another likewise requires moving the proof first and is documented as a migration, because the new config cannot discover an arbitrary old root.
 
-## Future options (not part of the initial implementation)
+### 3.4 String and collection options
 
-The registry and resolution path are intended to accept the following options later, but this proposal does not add their keys, change their emitters, add verifier flags, or add their fixtures.
+`string-semantics` selects `unicode-scalar` (default) or `javascript-utf16`.
+The independent `dafny-library` option selects `stdlib` (default) or `local`
+collection helpers. Both accept file overrides. UTF-16 requires an explicit
+`local` choice; `resolveOptions` rejects incompatible effective settings after
+project values and file directives are merged. Lean rejects UTF-16.
 
-### `javascript-utf16` and `dafny-lib` (PR #211, issue #210)
+Source dependencies must use the same effective string model before their
+contracts are copied. The check follows imports, re-exports, and compiler-selected
+cross-file callees; unrelated files are excluded. An explicit `--config` applies
+to dependencies too, while each file retains its directives. Collection-library
+choices may differ because they do not reinterpret contracts.
 
-A later `javascript-utf16: true` option would gate PR #211's Dafny emitter behavior:
+See [DESIGN_STRINGS.md](DESIGN_STRINGS.md) for emission and verification behavior,
+and [SPEC.md §7.6](SPEC.md#76-project-configuration-lemmascriptjson) for setup.
 
-- `string` types and `str` literals set a per-emission flag; literals are written as `\uXXXX` code-unit escapes for everything outside printable ASCII, so astral pairs and lone surrogates survive the UTF-8 file.
-- Preambles that mention chars vary with the mode. This is forced, not stylistic: Dafny 4.11 rejects `\U{…}` escapes under `--unicode-char:false` and `\u…` escapes under the default, so `IsJSWhitespace` (StringTrim) must be emitted with `\u0009…` in UTF-16 mode and `\U{0009}…` otherwise, and `StringFromCharCode`'s `requires` is `0 <= n < 0x10000` vs the surrogate-free scalar range. `PREAMBLE_CODE` entries become `string | (options) => string`.
-- The file header records the model (§5), and `dafnyVerify` passes `--unicode-char:false --allow-warnings` when it sees it. `--allow-warnings` is required: 4.11 prints a deprecation warning for the flag and, by default, a warning fails the run.
-
-A future `dafny-lib` option would select where `filter`/`every`/`reduce` come from: `Std.Collections.Seq.Filter/All/FoldLeft` (today; `dafnyVerify` already auto-adds `--standard-libraries` on a `Std.` substring) or the local `SeqFilter`/`SeqAll`/`SeqFoldLeft` recursive helpers from PR #211, emitted into the preamble on demand like `SeqFind`.
-
-The two would interact: Dafny's precompiled standard library is built for Unicode-scalar chars and cannot load under `--unicode-char:false`. After config and file layers are merged, `resolveOptions` must implement exactly this rule: if `javascript-utf16` is true and `dafny-lib` is absent, supply the dependent default `local-lib`; if `dafny-lib` is explicitly `std-lib`, reject the combination and name both keys. An explicit incompatible choice is never silently replaced. PR #211's per-file fail-closed check would stay as the last line of defense (a UTF-16 file whose *proof additions* import `Std.*`), because the config can't see hand-written proof text; its message should name the config key. A string-free file could keep importing `Std.*` in its proofs: the header marker would only be emitted when strings actually appear.
+## Future options
 
 ### `number-semantics` (issue #205)
 
@@ -130,25 +135,31 @@ JavaScript numbers need an enum-shaped semantic choice, not a `javascript-number
 | `extract.ts` | `extractModule(sourceFile, options = DEFAULT_OPTIONS)`; module-level `_options` set on entry, following the existing `_externs` reset pattern; `externIsImpure` reads it. |
 | `resolve`, `narrow`, `autohavoc`, `peephole` | Unchanged initially. Add an `options` parameter only when a future option needs one. |
 | `transform.ts` | Unchanged. `TransformOptions { backend, monadic }` is backend-intrinsic pipeline configuration; keep it separate rather than merging `LscOptions` into it. |
-| `dafny-emit.ts` | `emitDafnyFile(file, tsFileName, options = DEFAULT_OPTIONS)` replaces the `{ safeSlice }` bag; `_useSafeSlice` becomes `_options["safe-slice"]`. No other emission changes are part of this proposal. |
-| `dafny-commands.ts` | Algorithms are unchanged; `lsc.ts` passes mapped artifact paths and uses the mapped directory as the verifier/regen working directory. Artifact-derived verifier flags belong to the future options in §5. |
-| `lean-emit.ts` | Error text only. Dafny-only options are ignored under Lean without a warning — a per-file warning would be noise in batch mode, and the docs table carries the backend column. |
+| `dafny-emit.ts` | `emitDafnyFile(file, tsFileName, options = DEFAULT_OPTIONS)` receives resolved settings and applies the shared compatibility check for programmatic callers. Each emission resets its safe-slice, string, and collection-library state from those settings. |
+| `dafny-commands.ts` | `lsc.ts` passes mapped artifact paths and uses the mapped directory as the verifier/regen working directory. The generated artifact's options header determines verifier flags (§5). |
+| `lean-emit.ts` | The CLI rejects UTF-16 because Lean has no matching string model. Other Dafny-only settings do not affect Lean emission. |
 | `info-command.ts` | `lsc info --typed` gains a top-level `options` field (the effective set). Additive, so `schema` stays `1`. |
 
 Optional-with-default parameters keep any external programmatic caller of `extractModule`/`emitDafnyFile` working; the CLI always passes explicitly.
 
-## 5. Future artifact headers
+## 5. Artifact headers
 
-The initial options do not require non-default verifier flags, so this proposal does not change generated headers or `dafnyVerify`. When a future option does require flags, preserve PR #211's idea — the artifact, not the config, is what a human hands to `dafny verify` — but generalize the form so each option does not invent another sentence:
+Options requiring non-default verifier flags are recorded in the artifact, so a standalone proof keeps its interpretation without reading the project config:
 
 ```
 // Generated by lsc from foo.ts
-// lsc options: javascript-utf16
+// lsc options: string-semantics=javascript-utf16
 ```
 
-The future line is space-separated `key` (boolean) or `key=value` tokens, listing only non-default options that *materially affected this file* (UTF-16 would appear only when the file has strings; `dafny-lib` would never appear because it changes emitted helpers, not verifier flags). `dafnyVerify` would parse the line and map tokens to flags: `javascript-utf16` → `--unicode-char:false --allow-warnings`; a future `number-semantics=javascript` marker would select the version/capability checks and any flags established by the number-backend spike. The additions-only check already guarantees `.dfy` and `.dfy.gen` share the header, so flipping an option in `lemmascript.json` would surface as an ordinary generator change: `regen` three-way-merges the new header line in, then verifies under the new flags.
+Every UTF-16-selected file receives the token, including files whose declarations
+have no string types. `dafny-library` needs no token because it changes generated
+helpers rather than verifier flags. The verifier reads the saved model;
+without a token it uses Unicode-scalar mode. Existing scalar headers are unchanged.
 
-Reading future flags from the artifact rather than from the config is deliberate: the two could not drift within one `lsc check`, while a standalone `.dfy` (a fixture, a file someone pulled out of a repo) would still verify correctly and a reader would see the model on line 2.
+Parsing rejects unknown models, duplicate options headers, and duplicate string-model tokens.
+The additions-only gate compares the proof's model with its generated companion,
+so an inserted header cannot override it. A model change requires `regen` to
+merge the new generated header before verification.
 
 ## 6. CLI surface
 
@@ -159,7 +170,7 @@ Reading future flags from the artifact rather than from the config is deliberate
 ## 7. Docs and tests
 
 - **SPEC.md §2 and §7**: add `option` to the file-level directive table; add `config` to the command list, `--config=` to flags, and new §7.6 "Project configuration: `lemmascript.json`" with the table from §3 (~15 lines, per AGENTS.md style). §2.7 describes `safe-slice` as both an option and a legacy directive; §2.9/§2.11 extern prose becomes conditional on `extern-default`. **SPEC_DAFNY.md**: document `proof-dir`, its mirrored layout, and proof migration. **SPEC_LEAN.md**: one line on impure externs. **TOOLS.md**: `config.ts` in the file table plus a short "Options" section on the flow in §4. **AGENTS.md**: one line under Toolchain commands pointing at `lsc config`; its regen rules apply to mapped paths unchanged. **site `reference/cli.md`**: directive, flag, and command rows plus a "Project configuration" section (hand-written page; `DESIGN_CONFIG.md` itself joins `sync-docs.mjs` like the other design docs).
-- **`tools/test-fixtures.sh`** keeps a small fixture directory with `lemmascript.json` and a nested source file to exercise nearest-ancestor discovery, plus invalid config fixtures for an unknown key and a bad value. It verifies that `proof-dir` mirrors the nested path, creates `.dfy.gen` and `.dfy` there rather than beside the TS, and refuses to bypass a pre-existing sibling proof. Self-contained source fixtures use `//@ option` to exercise `extern-default`, `safe-slice: false`, a config-only `proof-dir` directive error, bad and duplicate directives, and precedence over the project config. A `lsc config` invocation is grepped for the effective post-directive values and resolved artifact directory. Existing fixtures run without a config and pin the defaults. UTF-16 and JavaScript-number fixtures are deferred with those options.
+- **`tools/test-fixtures.sh`** keeps a small fixture directory with `lemmascript.json` and a nested source file to exercise nearest-ancestor discovery, plus invalid config fixtures for an unknown key and a bad value. It verifies that `proof-dir` mirrors the nested path, creates `.dfy.gen` and `.dfy` there rather than beside the TS, and refuses to bypass a pre-existing sibling proof. Self-contained source fixtures use `//@ option` to exercise `extern-default`, `safe-slice: false`, a config-only `proof-dir` directive error, bad and duplicate directives, and precedence over the project config. A `lsc config` invocation is grepped for the effective post-directive values and resolved artifact directory. Existing fixtures run without a config and pin the defaults. UTF-16 is exercised through both project config and the ordinary file-directive example; unit tests cover dependency compatibility. JavaScript-number fixtures remain deferred.
 - **CI** is otherwise untouched: examples and case studies verify under today's pure-extern default; #211 and #205 are outside the initial scope.
 
 ## 8. Initial scope and future PRs
@@ -167,7 +178,7 @@ Reading future flags from the artifact rather than from the config is deliberate
 - **`extern-default`** generalizes the existing explicit `//@ impure` path and adds config/directive fixtures and conditional docs. No default-flipping PR or regenerated examples are needed; existing examples keep their explicit `//@ impure`, and unmarked externs remain pure.
 - **Existing `safe-slice`** moves from an emitter-specific boolean into the registry without changing generated output. Its old directive remains an alias.
 - **`proof-dir`** adds path routing only; it does not change emitter text or the additions-only/regen algorithms. Existing projects stay beside-source until they opt in and move their hand-written proofs.
-- **#211 and #205** do not land as part of this proposal. When their encodings are ready, they add registry entries and the explicitly future emitter/header work above, with their own fixtures and docs.
+- **#211** adds string models and collection-library selection through the same registry and artifact mechanism. **#205** remains a future number-model extension.
 - **Flipping a default later:** change the registry line, run `./regen-dafny.sh`, and note it in the release. Projects that want the old model add one key. The registry's `default` field is where that decision lives, visibly, rather than being implicit in emitter code.
 
 ## Non-goals
@@ -175,14 +186,8 @@ Reading future flags from the artifact rather than from the config is deliberate
 - Per-function option overrides. `//@ option` is file-level; function facts keep their specific annotations.
 - A `backend` config option. `--backend=` selects the command target and `//@ backend` declares file membership; neither is a semantic model option.
 - Relocating Lean artifacts with `proof-dir`. Lean paths participate in module names and Lake roots, unlike standalone Dafny files, so that needs its own design.
-- Implementing `javascript-utf16`, `dafny-lib`, or `number-semantics`; they are future applications documented above, not initial registry entries.
+- Implementing `number-semantics`; it remains a future application documented above.
 - Nested/namespaced config (`{"dafny": {…}}`). Flat kebab-case keys with a backend column in the docs are enough for the initial options; revisit past ~15.
 - `time-limit` / `extra-flags` as project defaults. `LemmaScript-files.txt` already carries them per file; adding a project-wide default is a registry entry away if a case study asks.
 - JSON Schema generation (`lsc config --schema`). Cheap follow-up from the registry; not needed to land.
 - Options in the Raw IR JSON (`lsc extract`). The IR already reflects their effect (`RawExtern.impure`).
-
-## Open questions
-
-1. **Future string option shape.** Should `javascript-utf16` be a boolean or should a later proposal use `strings: "unicode-scalar" | "javascript-utf16"`? This does not block the initial config implementation.
-2. **Future `--allow-warnings` scope.** UTF-16 mode would need it for Dafny's `--unicode-char` deprecation warning, but it also un-fatals every other warning in the file. Resolve this with the UTF-16 implementation, not here.
-3. **Future header parsing.** When artifact-derived flags exist, should `dafnyVerify` warn when a `.dfy` lacks the `// Generated by lsc` line entirely? Resolve this with the first option that needs such a header.
diff --git a/DESIGN_STRINGS.md b/DESIGN_STRINGS.md
new file mode 100644
index 00000000..b60d3df8
--- /dev/null
+++ b/DESIGN_STRINGS.md
@@ -0,0 +1,98 @@
+# DESIGN_STRINGS — Selectable Dafny string semantics
+
+**Status:** implemented in PR #211.
+**Issue:** [#210](https://github.com/midspiral/LemmaScript/issues/210) · **PR:** [#211](https://github.com/midspiral/LemmaScript/pull/211)
+
+JavaScript strings are UTF-16 code-unit sequences, while Dafny's default strings
+are Unicode scalar sequences. For example, JavaScript gives `"😀".length === 2`;
+the default Dafny model gives 1. LemmaScript keeps that existing model as the
+default and offers an explicit UTF-16 choice for code that depends on code units.
+
+## Models and configuration
+
+| Setting | Meaning |
+|---|---|
+| `unicode-scalar` (default) | One element per Unicode scalar. Length, indexing, slicing, character codes, and search offsets can differ from JavaScript for astral text. Unpaired surrogates are outside the domain. |
+| `javascript-utf16` | One element per UTF-16 code unit. Supported operations use JavaScript's code-unit representation, including astral pairs and unpaired surrogates. |
+
+`string-semantics` selects the model. The independent `dafny-library` option
+selects `stdlib` (default) or generated `local` helpers for `filter`, `every`,
+and `reduce`. Unicode-scalar mode supports either library. UTF-16 requires an
+explicit `local` choice because Dafny's precompiled standard library cannot load
+in that character mode; incompatible combinations are errors.
+
+Both options accept project settings and file directives, with file values
+taking precedence. Configuration syntax lives in [SPEC.md §7.6](SPEC.md#76-project-configuration-lemmascriptjson).
+Before copying contracts or emitting a proof, the CLI checks that source
+dependencies use the same effective string model. Re-exports and compiler-selected
+cross-file callees are included; unrelated files are not. Library choices may
+differ between dependencies because they do not reinterpret contracts.
+The Lean backend rejects UTF-16 because it has no corresponding string model.
+
+## Emission and operation boundaries
+
+UTF-16 literals are emitted as `\uXXXX` code-unit escapes outside printable ASCII,
+so astral pairs and lone surrogates survive writing the UTF-8 artifact.
+Unicode-scalar extraction rejects literals containing unpaired surrogates.
+Character-sensitive helpers use the selected Dafny character representation.
+
+| Operation | Unicode-scalar | UTF-16 |
+|---|---|---|
+| Length, indexing, slicing, `charCodeAt`, search offsets | Scalar positions and values | Code-unit positions and values |
+| Concatenation, equality, prefixes/suffixes, `repeat`, `trim*` | Preserves the operation's meaning on well-formed scalar strings | Preserves the operation's meaning on code-unit strings |
+| `String.fromCharCode(n)` | Requires a Unicode scalar value | Requires `0 <= n < 0x10000`; wrapping is not modeled |
+| `toLowerCase`, `toUpperCase` | ASCII letter conversion; non-ASCII letters unchanged | Same restriction |
+| `split(d)` | Existing axiomatic helper; requires a nonempty delimiter | Same helper and restriction |
+
+These claims are limited to the supported fragment and its preconditions. Selecting
+UTF-16 does not add regular expressions, normalization, locale-aware operations,
+or unrestricted JavaScript argument coercions. `split` remains a trusted axiom.
+
+Case conversion handles ASCII letters only, leaves non-ASCII letters unchanged,
+and preserves length. It can differ from JavaScript: `"ß".toUpperCase()` is
+`"SS"` in JavaScript.
+
+`stdlib` emits `Std.Collections.Seq.Filter/All/FoldLeft`; `local` emits the
+recursive `SeqFilter/SeqAll/SeqFoldLeft` helpers on demand. The choice is visible
+in generated definitions and calls, so it needs no separate artifact marker.
+
+## Proof interpretation and verification
+
+Every file selecting UTF-16 receives this generated header, even if its
+declarations contain no string types:
+
+```dafny
+// Generated by lsc from foo.ts
+// lsc options: string-semantics=javascript-utf16
+```
+
+Default artifacts retain their existing header. Without a string-model token,
+verification explicitly uses Unicode-scalar mode. The verifier reads the saved
+artifact, so its interpretation does not depend on later project-config changes.
+
+Header parsing rejects unknown models, duplicate options-header lines, and
+duplicate string-model tokens. The additions-only check also compares the proof's
+model with its generated companion. Proof additions cannot select a different
+model, including during `regen --no-verify`. Changing the source setting requires
+`regen` to merge the generated header into the proof before verification.
+
+Unicode-scalar verification adds `--unicode-char:true`; UTF-16 adds
+`--unicode-char:false --allow-deprecation`. Dafny 4.11 deprecates the latter
+character mode, so deprecated-feature warnings are allowed while other warning
+categories retain the default fatal policy. `--allow-warnings` is not needed.
+UTF-16 proof additions importing `Std.*` are rejected with a compatibility error;
+the collection-library setting does not control handwritten imports.
+
+## Validation
+
+Tests cover option defaults and overrides, dependency compatibility, literal
+escaping and surrogate handling, helper selection, verifier flags, and header
+validation. Frontend fixtures prove representative UTF-16 results for astral pairs
+and lone surrogates. The helper-only regression also checks the JavaScript result.
+Regression cases cover added model headers and strings introduced only by helpers.
+Existing scalar examples retain their generated output.
+
+## References
+
+- [ECMAScript: The String Type](https://tc39.es/ecma262/multipage/ecmascript-data-types-and-values.html#sec-ecmascript-language-types-string-type)
+- [Dafny 4.11: Strings and characters](https://dafny.org/v4.11.0/Compilation/StringsAndChars)
diff --git a/SPEC.md b/SPEC.md
index ca7d5769..dcca3688 100644
--- a/SPEC.md
+++ b/SPEC.md
@@ -452,6 +452,10 @@ The same coercion applies to non-bool conditions in `if`/`while`/`?:` positions:
 
 ### 3.2 Special Forms
 
+The collection rows show the default `dafny-library: stdlib` setting.
+With `local`, `SeqFilter` and `SeqAll` replace the corresponding
+`Std.Collections.Seq` helpers (§7.6).
+
 | Spec / TS | Lean | Dafny |
 |-----------|------|-------|
 | `arr.length` | `arr.size` | `\|arr\|` |
@@ -682,6 +686,9 @@ The transform uses two strategies for translating `receiver.method(args)`:
 | `s.add(x)` | `setAdd` | `s.insert x` | `(s + {x})` |
 | `s.delete(x)` | `setDelete` | `s.erase x` | `(s - {x})` |
 
+Dafny collection entries use the default `stdlib` setting; `local` uses
+`SeqFilter` and `SeqAll` instead (§7.6).
+
 The transform checks helper-function methods first, then dot-notation methods. If neither matches, it errors.
 
 ### 3.9 Map, Set, and Optional Narrowing
@@ -1021,6 +1028,11 @@ The spec body is purely additive — `regen` three-way-merges and preserves user
 | `A \| B` (union param) | field intersection type | field intersection type |
 | Anything else | Pass through | Pass through |
 
+For the Dafny backend, `string` uses Unicode-scalar semantics by default.
+To use JavaScript's UTF-16 code-unit model, select
+`"string-semantics": "javascript-utf16"` and `"dafny-library": "local"`
+(§7.6). See SPEC_DAFNY.md §4 for the behavior and limitations of each model.
+
 `lsc` reads parameter and variable types from ts-morph. Primitive types are mapped per the table. User-defined types (like `State`, `Event`) are passed through by name — the corresponding backend type is generated from the TS type declaration.
 
 **Tuples.** A tuple type lowers to a native backend tuple (`(A, B)` in Dafny, `A × B` in Lean) only when its element types differ; a *homogeneous* tuple (`[number, number]`) lowers to `seq`/`Array` instead, since a sequence is a superset of what a same-typed tuple offers (dynamic index, `.length`, `.map`). The same homogeneity rule applies to an unannotated array literal: `[1, "a"]` is a tuple, `[1, 2, 3]` a sequence; an explicit expected type wins. Tuple element access **requires a compile-time integer-literal index** — `t[0]`, `t[1]` — because a tuple has a distinct type per slot, so a runtime index has neither a single result type nor a backend projection (`t.0`/`t.1`). A non-literal index into a tuple is a `lsc` error. `const [a, b] = t` destructuring works (it desugars to per-slot access). See [`examples/tuples.ts`](examples/tuples.ts).
@@ -1378,14 +1390,39 @@ it; absent means current behavior. Unknown keys and bad values are errors.
 | `extern-default` | `pure` \| `impure` | `pure` | yes |
 | `safe-slice` | boolean | `false` | yes |
 | `proof-dir` | relative path | source directory | no (Dafny only) |
+| `string-semantics` | `unicode-scalar` \| `javascript-utf16` | `unicode-scalar` | yes (Dafny only) |
+| `dafny-library` | `stdlib` \| `local` | `stdlib` | yes (Dafny only) |
 
 Eligible settings use `//@ option <key> <value>` before the first source
 statement. File values override project values; duplicates are errors.
 `proof-dir` mirrors the source's config-relative path under its configured root
-(see SPEC_DAFNY.md §1). `lsc config foo.ts` prints the config path, effective
+(see SPEC_DAFNY.md §1). `string-semantics` selects which model of JavaScript strings a
+Dafny proof is made under (SPEC_DAFNY.md §4). A source file and the source files it
+imports, directly or indirectly, must use the same `string-semantics` value after
+project settings and file overrides are combined. Declaration files (`.d.ts`)
+are excluded from this comparison. If values differ, `lsc` reports both files
+and stops before generating Dafny.
+`dafny-library` selects standard-library
+or generated local helpers for `filter`, `every`, and `reduce`. UTF-16 requires an explicit
+`"dafny-library": "local"`; omitting it keeps the `stdlib` default and reports an incompatibility.
+Unicode-scalar strings support either library choice. `lsc config foo.ts` prints the config path, effective
 options, and resolved Dafny artifact directory; `lsc config` reports defaults
 from the current directory. `backend` is deliberately not a config option.
 
+To use JavaScript UTF-16 string semantics in a standalone file, add these
+directives before its first statement. These overrides are not needed for the
+default `unicode-scalar` mode:
+
+```typescript
+//@ backend dafny
+//@ option string-semantics javascript-utf16
+//@ option dafny-library local
+```
+
+See [examples/utf16.ts](examples/utf16.ts) and its Dafny proof. Compatibility is checked
+after project values and file directives are merged. Collection libraries may differ
+between files; unlike the string model, they do not change the meaning of contracts.
+
 ---
 
 ## 8. Pipeline
diff --git a/SPEC_DAFNY.md b/SPEC_DAFNY.md
index 9f8be868..c98c5ad0 100644
--- a/SPEC_DAFNY.md
+++ b/SPEC_DAFNY.md
@@ -98,6 +98,7 @@ The Dafny emitter auto-injects helper functions when needed. Each is emitted at
 | Helper | When | Purpose |
 |--------|------|---------|
 | `SeqIndexOf` | `arr.indexOf(x)` | First-index search (`-1` if absent) |
+| `SeqFilter` / `SeqAll` / `SeqFoldLeft` | `filter` / `every` / `reduce` with `dafny-library: local` | Local recursive collection helpers (no Dafny standard-library dependency) |
 | `SeqFindIndex` | `arr.findIndex(f)` | Predicate first-index search |
 | `SeqFind` | `arr.find(f)` | Predicate first-match search |
 | `SeqFindLast` | `arr.findLast(f)` | Predicate last-match search |
@@ -116,6 +117,27 @@ The Dafny emitter auto-injects helper functions when needed. Each is emitted at
 | `StringTrim` | `s.trim()` / `s.trimEnd()` / `s.trimStart()` | Trim (also provides `StringTrimRight` / `StringTrimLeft`); strips the full ECMAScript whitespace set via `IsJSWhitespace`, not just `' '` |
 | `StringToLower` / `StringToUpper` | `s.toLowerCase()` / `s.toUpperCase()` | Case folding |
 
+**String semantics.** Set `string-semantics` in `lemmascript.json` or a file's
+`//@ option` directive (SPEC.md §7.6). Proofs depend on the selected model:
+
+| Setting | Meaning |
+|---|---|
+| `"unicode-scalar"` (default) | Strings are Unicode scalar sequences. `.length`, indexing, `slice`, `charCodeAt`, and `indexOf` can differ from JavaScript for characters such as emoji. Unpaired surrogates are unsupported. |
+| `"javascript-utf16"` | Strings are UTF-16 code-unit sequences. `.length`, indexing, `slice`, and `charCodeAt` use JavaScript code-unit positions and values; indexing and slicing retain the fragment's bounds obligations. Requires `"dafny-library": "local"`. |
+
+Both profiles support ASCII-only case conversion. `String.fromCharCode` requires
+a Unicode scalar in the default profile, or `0 <= n < 0x10000` in UTF-16 mode.
+Generated files record every UTF-16 selection in their header;
+the default profile adds no `string-semantics` setting.
+
+**Collection helpers.** `dafny-library` selects standard-library helpers (`stdlib`,
+the default) or generated helpers (`local`) for `filter`, `every`, and `reduce`.
+Unicode-scalar mode supports either; UTF-16 mode requires an explicit `local` setting.
+
+This choice does not change string semantics or control handwritten proof imports.
+Those imports must still be compatible with the selected string model (see §5).
+Both settings support file directives; see [examples/utf16.ts](examples/utf16.ts).
+
 ---
 
 ## 5. Verification
@@ -128,5 +150,15 @@ The Dafny emitter auto-injects helper functions when needed. Each is emitted at
 
 Standard libraries are auto-detected: if `foo.dfy` contains `import Std.`, the `--standard-libraries` flag is added.
 
-The shared `--time-limit=<seconds>` flag (SPEC.md §7) maps to Dafny's `--verification-time-limit`; `--extra-flags=<string>` is forwarded verbatim to `dafny verify`.
+`lsc` verifies each `.dfy` using the string semantics recorded in its generated
+header, even if the project configuration has changed. A file without a
+`string-semantics` header uses `unicode-scalar`.
+
+Proof additions must preserve the generated file's string model. Conflicting or
+duplicate model settings are errors, including when verification is skipped.
 
+Proofs using `javascript-utf16` cannot import Dafny's precompiled standard library
+(`Std.*`); verification reports an error if they do. Proofs using `unicode-scalar`
+can use that library.
+
+The shared `--time-limit=<seconds>` flag (SPEC.md §7) maps to Dafny's `--verification-time-limit`; `--extra-flags=<string>` is forwarded verbatim to `dafny verify`.
diff --git a/SUBSET.md b/SUBSET.md
index 729e3447..fb0aa914 100644
--- a/SUBSET.md
+++ b/SUBSET.md
@@ -34,7 +34,7 @@ Two things shape what you can verify:
 | `number` (non-integer literal) | real | `0.8`, `3.14` become reals; mixed int/real arithmetic coerces automatically. |
 | `bigint` | integer | Same as `number`; `32n`, `0xffffn` literals supported, exact past 2^53. |
 | `boolean` | bool | |
-| `string` | string | |
+| `string` | string | Modelled per the project's `string-semantics` (SPEC_DAFNY.md §4): Unicode scalars by default, UTF-16 code units under `"javascript-utf16"`. |
 | `T[]` / `Array<T>` / `readonly T[]` | sequence | |
 | `[A, B, ...]` (heterogeneous tuple) | tuple | Native tuple (`(A, B)` / `A × B`). Access needs a literal index (`t[0]`, `t[1]`); `const [a, b] = t` works. |
 | `[T, T, ...]` (homogeneous tuple) | sequence | Same-typed elements model as a `seq` (more capable than a fixed tuple). |
diff --git a/TOOLS.md b/TOOLS.md
index 4f9910e9..331ac8ae 100644
--- a/TOOLS.md
+++ b/TOOLS.md
@@ -60,17 +60,26 @@ Type names: `Expr`, `Stmt`, `Module`, `MatchArm`, `StmtMatchArm`, and `Decl` = `
 `config.ts` owns the `OPTION_SPECS` registry, nearest-ancestor
 `lemmascript.json` discovery, JSON and `//@ option` validation, defaults, and
 cross-option checks. `lsc.ts` merges explicit project values with eligible
-top-of-file overrides and resolves once per source file. It passes the result
-to extraction/emission; those phases never read config files. `proof-dir` is
-consumed only by `lsc.ts`, which maps the complete Dafny companion set before
-calling the unchanged Dafny command helpers. `TransformOptions` remains
-backend-intrinsic pipeline configuration and is deliberately separate.
+top-of-file overrides and resolves once per source file, then passes options to
+extraction and emission. Those phases do not read config files.
+
+Before copying cross-file contracts, the CLI checks that dependencies share the
+root's string model, following imports, re-exports, and selected callees.
+`string-semantics` controls literal validation, Dafny character helpers, and the
+saved model header. Verification reads that header and the additions-only gate
+checks it against the generated companion. `dafny-library` independently selects
+collection helpers; the shared compatibility check requires `local` for UTF-16.
+See [DESIGN_STRINGS.md](DESIGN_STRINGS.md) for the model boundaries.
+
+`proof-dir` is consumed only by `lsc.ts`, which maps the complete Dafny companion
+set before calling the command helpers. `TransformOptions` remains separate
+backend-intrinsic pipeline configuration.
 
 ## Method Calls
 
 All TS `receiver.method(args)` calls produce `methodCall` IR nodes carrying the receiver, its type, the TS method name, the args, and a `monadic` flag. No renaming — the IR stores the TS name (`"map"`, `"indexOf"`, `"with"`, `"get"`, etc.) and the receiver type disambiguates.
 
-Each emitter dispatches on `(receiverTy, method)` to decide syntax. For example, `(array, "filter")` → Lean: `arr.filter f`, Dafny: `Seq.Filter(f, arr)`. Unsupported `(type, method)` pairs error at emit time.
+Each emitter dispatches on `(receiverTy, method)` to decide syntax. For example, `(array, "filter")` → Lean: `arr.filter f`, Dafny: `Std.Collections.Seq.Filter(f, arr)` by default (`SeqFilter(f, arr)` with `dafny-library: local`). Unsupported `(type, method)` pairs error at emit time.
 
 `app` is reserved for receiver-less calls: user-defined functions, `Pure.fnName(...)`, `JSFloorDiv(a, b)`, `SetToSeq(s)`.
 
diff --git a/examples/utf16.dfy b/examples/utf16.dfy
new file mode 100644
index 00000000..68081a4d
--- /dev/null
+++ b/examples/utf16.dfy
@@ -0,0 +1,38 @@
+// Generated by lsc from utf16.ts
+// lsc options: string-semantics=javascript-utf16
+
+predicate SeqAll<T>(xs: seq<T>, p: T -> bool)
+  decreases |xs|
+{
+  |xs| == 0 || (p(xs[0]) && SeqAll(xs[1..], p))
+}
+
+function emojiLength(): int
+{
+  |"\uD83D\uDE00"|
+}
+
+lemma emojiLength_ensures()
+  ensures (emojiLength() == 2)
+{
+}
+
+function emojiFirstCodeUnit(): int
+{
+  ("\uD83D\uDE00"[0..1][0] as int)
+}
+
+lemma emojiFirstCodeUnit_ensures()
+  ensures (emojiFirstCodeUnit() == 55357)
+{
+}
+
+function allTextIsNonempty(): bool
+{
+  SeqAll(["\uD83D\uDE00", "text"], (value: string) => (|value| > 0))
+}
+
+lemma allTextIsNonempty_ensures()
+  ensures (allTextIsNonempty() == true)
+{
+}
diff --git a/examples/utf16.dfy.gen b/examples/utf16.dfy.gen
new file mode 100644
index 00000000..68081a4d
--- /dev/null
+++ b/examples/utf16.dfy.gen
@@ -0,0 +1,38 @@
+// Generated by lsc from utf16.ts
+// lsc options: string-semantics=javascript-utf16
+
+predicate SeqAll<T>(xs: seq<T>, p: T -> bool)
+  decreases |xs|
+{
+  |xs| == 0 || (p(xs[0]) && SeqAll(xs[1..], p))
+}
+
+function emojiLength(): int
+{
+  |"\uD83D\uDE00"|
+}
+
+lemma emojiLength_ensures()
+  ensures (emojiLength() == 2)
+{
+}
+
+function emojiFirstCodeUnit(): int
+{
+  ("\uD83D\uDE00"[0..1][0] as int)
+}
+
+lemma emojiFirstCodeUnit_ensures()
+  ensures (emojiFirstCodeUnit() == 55357)
+{
+}
+
+function allTextIsNonempty(): bool
+{
+  SeqAll(["\uD83D\uDE00", "text"], (value: string) => (|value| > 0))
+}
+
+lemma allTextIsNonempty_ensures()
+  ensures (allTextIsNonempty() == true)
+{
+}
diff --git a/examples/utf16.ts b/examples/utf16.ts
new file mode 100644
index 00000000..85ce0e96
--- /dev/null
+++ b/examples/utf16.ts
@@ -0,0 +1,24 @@
+//@ backend dafny
+//@ option string-semantics javascript-utf16
+//@ option dafny-library local
+
+// JavaScript counts UTF-16 code units: this emoji occupies two.
+export function emojiLength(): number {
+  //@ verify
+  //@ ensures \result === 2
+  return "😀".length;
+}
+
+// Slicing one code unit may produce an unpaired surrogate.
+export function emojiFirstCodeUnit(): number {
+  //@ verify
+  //@ ensures \result === 0xD83D
+  return "😀".slice(0, 1).charCodeAt(0);
+}
+
+// UTF-16 uses local collection helpers rather than Dafny's standard library.
+export function allTextIsNonempty(): boolean {
+  //@ verify
+  //@ ensures \result === true
+  return ["😀", "text"].every(value => value.length > 0);
+}
diff --git a/site/src/content/docs/reference/cli.md b/site/src/content/docs/reference/cli.md
index 9945d539..a06329d4 100644
--- a/site/src/content/docs/reference/cli.md
+++ b/site/src/content/docs/reference/cli.md
@@ -94,11 +94,28 @@ at the current directory. Use `--config=<path>` to pin a particular file.
 ```json
 {
   "extern-default": "impure",
+  "string-semantics": "unicode-scalar",
+  "dafny-library": "stdlib",
   "safe-slice": true,
   "proof-dir": "proofs"
 }
 ```
 
+`dafny-library` selects `stdlib` (default) or generated `local` helpers for collection
+operations. Enabling `"string-semantics": "javascript-utf16"` requires explicitly setting
+`"dafny-library": "local"`; an omitted or explicit `stdlib` choice is an error.
+
+A file can override both project settings before its first statement:
+
+```typescript
+//@ backend dafny
+//@ option string-semantics javascript-utf16
+//@ option dafny-library local
+```
+
+Source dependencies must use the same effective string model. `lsc config file.ts`
+shows the settings after file overrides; `lsc check file.ts` also checks dependencies.
+
 ### `lsc claimcheck`
 
 Forwards to the bundled `lemmascript-claimcheck` CLI, which cross-examines the
diff --git a/tools/fixtures/collection-library-project/collections.ts b/tools/fixtures/collection-library-project/collections.ts
new file mode 100644
index 00000000..2a5cd409
--- /dev/null
+++ b/tools/fixtures/collection-library-project/collections.ts
@@ -0,0 +1,37 @@
+//@ backend dafny
+
+export function positiveNumbers(): number[] {
+  //@ verify
+  //@ ensures \result.length === 2 && \result[0] === 1 && \result[1] === 2
+  return [-1, 1, 2].filter(value => value > 0);
+}
+
+export function everyNumberIsPositive(): boolean {
+  //@ verify
+  //@ ensures \result === true
+  return [1, 2, 3].every(value => value > 0);
+}
+
+export function sumNumbers(): number {
+  //@ verify
+  //@ ensures \result === 6
+  return [1, 2, 3].reduce((total, value) => total + value, 0);
+}
+
+export function nonemptyStrings(): string[] {
+  //@ verify
+  //@ ensures \result.length === 2 && \result[0] === "a" && \result[1] === "bc"
+  return ["a", "", "bc"].filter(value => value.length > 0);
+}
+
+export function everyStringIsNonempty(): boolean {
+  //@ verify
+  //@ ensures \result === true
+  return ["a", "bc"].every(value => value.length > 0);
+}
+
+export function sumStringLengths(): number {
+  //@ verify
+  //@ ensures \result === 3
+  return ["a", "bc"].reduce((total, value) => total + value.length, 0);
+}
diff --git a/tools/fixtures/collection-library-project/lemmascript.json b/tools/fixtures/collection-library-project/lemmascript.json
new file mode 100644
index 00000000..7ec71b58
--- /dev/null
+++ b/tools/fixtures/collection-library-project/lemmascript.json
@@ -0,0 +1,3 @@
+{
+  "dafny-library": "local"
+}
diff --git a/tools/fixtures/config-incompatible-strings/lemmascript.json b/tools/fixtures/config-incompatible-strings/lemmascript.json
new file mode 100644
index 00000000..6211b2ae
--- /dev/null
+++ b/tools/fixtures/config-incompatible-strings/lemmascript.json
@@ -0,0 +1,3 @@
+{
+  "string-semantics": "javascript-utf16"
+}
diff --git a/tools/fixtures/config-incompatible-strings/source.ts b/tools/fixtures/config-incompatible-strings/source.ts
new file mode 100644
index 00000000..c7fa5836
--- /dev/null
+++ b/tools/fixtures/config-incompatible-strings/source.ts
@@ -0,0 +1,7 @@
+//@ backend dafny
+
+export function answer(): number {
+  //@ verify
+  //@ ensures \result === 42
+  return 42;
+}
diff --git a/tools/fixtures/config-incompatible-strings/stdlib.json b/tools/fixtures/config-incompatible-strings/stdlib.json
new file mode 100644
index 00000000..04218445
--- /dev/null
+++ b/tools/fixtures/config-incompatible-strings/stdlib.json
@@ -0,0 +1,4 @@
+{
+  "string-semantics": "javascript-utf16",
+  "dafny-library": "stdlib"
+}
diff --git a/tools/fixtures/string-with-standard-library.dfy b/tools/fixtures/string-with-standard-library.dfy
new file mode 100644
index 00000000..fc27bdc5
--- /dev/null
+++ b/tools/fixtures/string-with-standard-library.dfy
@@ -0,0 +1,4 @@
+// lsc options: string-semantics=javascript-utf16
+import opened Std.Arithmetic.Mul
+
+lemma StringAndStandardLibraryAreIncompatible() {}
diff --git a/tools/fixtures/unpaired-surrogate.ts b/tools/fixtures/unpaired-surrogate.ts
new file mode 100644
index 00000000..5a97b765
--- /dev/null
+++ b/tools/fixtures/unpaired-surrogate.ts
@@ -0,0 +1,7 @@
+// Under the default "unicode-scalar" profile a lone surrogate has no Dafny
+// value; extraction refuses it with the source line (DESIGN_STRINGS.md §3).
+export function lone(): number {
+  //@ verify
+  //@ ensures \result === 1
+  return "\uD83D".length;
+}
diff --git a/tools/fixtures/utf16-project/lemmascript.json b/tools/fixtures/utf16-project/lemmascript.json
new file mode 100644
index 00000000..5fde7fcc
--- /dev/null
+++ b/tools/fixtures/utf16-project/lemmascript.json
@@ -0,0 +1,4 @@
+{
+  "string-semantics": "javascript-utf16",
+  "dafny-library": "local"
+}
diff --git a/tools/fixtures/utf16-project/src/lean-rejected.ts b/tools/fixtures/utf16-project/src/lean-rejected.ts
new file mode 100644
index 00000000..36370998
--- /dev/null
+++ b/tools/fixtures/utf16-project/src/lean-rejected.ts
@@ -0,0 +1,7 @@
+// No `//@ backend` directive, so `--backend=lean` reaches the profile check
+// instead of skipping the file: javascript-utf16 is Dafny-only.
+export function greeting(): string {
+  //@ verify
+  //@ ensures \result.length === 2
+  return "hi";
+}
diff --git a/tools/fixtures/utf16-project/src/utf16.ts b/tools/fixtures/utf16-project/src/utf16.ts
new file mode 100644
index 00000000..efdc6efe
--- /dev/null
+++ b/tools/fixtures/utf16-project/src/utf16.ts
@@ -0,0 +1,37 @@
+//@ backend dafny
+
+export function emojiLength(): number {
+  //@ verify
+  //@ ensures \result === 2
+  return "😀".length;
+}
+
+export function emojiHighSurrogate(): number {
+  //@ verify
+  //@ ensures \result === 0xD83D
+  return "😀".charCodeAt(0);
+}
+
+export function emojiLowSurrogate(): number {
+  //@ verify
+  //@ ensures \result === 0xDE00
+  return "😀".charCodeAt(1);
+}
+
+export function unpairedSurrogateLength(): number {
+  //@ verify
+  //@ ensures \result === 1
+  return "\uD83D".length;
+}
+
+export function slicedHighSurrogate(): number {
+  //@ verify
+  //@ ensures \result === 0xD83D
+  return "😀".slice(0, 1).charCodeAt(0);
+}
+
+export function constructedSurrogate(): number {
+  //@ verify
+  //@ ensures \result === 0xD83D
+  return String.fromCharCode(0xD83D).charCodeAt(0);
+}
diff --git a/tools/src/config.ts b/tools/src/config.ts
index 02f8d6b1..0b8b402a 100644
--- a/tools/src/config.ts
+++ b/tools/src/config.ts
@@ -31,6 +31,20 @@ export const OPTION_SPECS = {
     fileOverride: false,
     description: "Directory for Dafny artifacts, relative to lemmascript.json.",
   },
+  "string-semantics": {
+    type: "enum",
+    values: ["unicode-scalar", "javascript-utf16"],
+    default: "unicode-scalar",
+    fileOverride: true,
+    description: "Which model of JavaScript strings a Dafny proof is made under.",
+  },
+  "dafny-library": {
+    type: "enum",
+    values: ["stdlib", "local"],
+    default: "stdlib",
+    fileOverride: true,
+    description: "Use Dafny's standard library or generated local helpers for collection operations.",
+  },
 } as const;
 
 type OptionSpecs = typeof OPTION_SPECS;
@@ -61,23 +75,24 @@ function isKnownKey(key: string): key is keyof OptionSpecs {
   return Object.hasOwn(OPTION_SPECS, key);
 }
 
-function parseValue(key: keyof OptionSpecs, raw: unknown, source: string): LscOptions[typeof key] {
+/** Validate one option against the registry and return its typed value. */
+export function parseOptionValue<K extends keyof LscOptions>(key: K, raw: unknown, source: string): LscOptions[K] {
   const spec = OPTION_SPECS[key] as AnyOptionSpec;
   if (spec.type === "boolean") {
     if (typeof raw !== "boolean") fail(source, `option '${key}' must be true or false`);
-    return raw as LscOptions[typeof key];
+    return raw as LscOptions[K];
   }
   if (spec.type === "enum") {
     if (typeof raw !== "string" || !(spec.values as readonly string[]).includes(raw)) {
       fail(source, `option '${key}' must be one of: ${spec.values.join(", ")}`);
     }
-    return raw as LscOptions[typeof key];
+    return raw as LscOptions[K];
   }
   if (typeof raw !== "string" || raw.trim().length === 0) {
     fail(source, `option '${key}' must be a non-empty relative path`);
   }
   if (path.isAbsolute(raw)) fail(source, `option '${key}' must be relative to lemmascript.json`);
-  return raw as LscOptions[typeof key];
+  return raw as LscOptions[K];
 }
 
 /** Validate a parsed lemmascript.json object, returning only explicitly set keys. */
@@ -91,7 +106,7 @@ export function validateOptions(raw: unknown, source: string): ExplicitOptions {
     if (!isKnownKey(key)) {
       fail(source, `unknown option '${key}' (known options: ${KNOWN_KEYS.join(", ")})`);
     }
-    out[key] = parseValue(key, value, source);
+    out[key] = parseOptionValue(key, value, source);
   }
   return out as ExplicitOptions;
 }
@@ -102,10 +117,10 @@ function parseDirectiveValue(key: keyof OptionSpecs, text: string, source: strin
     if (text !== "true" && text !== "false") fail(source, `option '${key}' must be true or false`);
     return (text === "true") as LscOptions[typeof key];
   }
-  if (spec.type === "enum") return parseValue(key, text, source);
+  if (spec.type === "enum") return parseOptionValue(key, text, source);
   // Config-only today, but keep the diagnostic precise if a future path is
   // made file-overridable.
-  return parseValue(key, text, source);
+  return parseOptionValue(key, text, source);
 }
 
 /**
@@ -206,13 +221,14 @@ export function parseFileOptions(sourceText: string, source: string): ExplicitOp
   return out as ExplicitOptions;
 }
 
-/** Apply defaults and all cross-option rules after explicit layers are merged. */
+/** Apply defaults, check option compatibility, and freeze the resolved configuration. */
 export function resolveOptions(explicit: ExplicitOptions, source: string): LscOptions {
-  // There are no cross-option constraints in the initial registry. Keep this
-  // as the single resolution gate: future dependent defaults (UTF-16 → local
-  // Dafny library) and incompatibilities belong here, before any consumer runs.
-  void source;
-  return Object.freeze({ ...DEFAULT_OPTIONS, ...explicit });
+  const options = { ...DEFAULT_OPTIONS, ...explicit };
+  // Dafny's precompiled standard library uses Unicode-scalar characters.
+  if (options["string-semantics"] === "javascript-utf16" && options["dafny-library"] === "stdlib") {
+    fail(source, '"string-semantics": "javascript-utf16" is incompatible with "dafny-library": "stdlib"; set "dafny-library": "local" explicitly');
+  }
+  return Object.freeze(options);
 }
 
 /** Find `fileName` at or above `fromPath`. */
diff --git a/tools/src/dafny-commands.ts b/tools/src/dafny-commands.ts
index 26746ae7..9559e305 100644
--- a/tools/src/dafny-commands.ts
+++ b/tools/src/dafny-commands.ts
@@ -5,6 +5,7 @@
 import { existsSync, readFileSync, writeFileSync, copyFileSync, unlinkSync } from "fs";
 import { execFileSync } from "child_process";
 import path from "path";
+import { DEFAULT_OPTIONS, parseOptionValue, type LscOptions } from "./config.js";
 
 function writeGen(genPath: string, text: string) {
   writeFileSync(genPath, text);
@@ -27,6 +28,18 @@ export function dafnyCheckDiff(genPath: string, dfyPath: string): boolean {
     }
   }
 
+  // Proof additions must retain the model chosen by the generated companion.
+  try {
+    const generated = readStringSemantics(readFileSync(genPath, "utf-8"));
+    const proof = readStringSemantics(readFileSync(dfyPath, "utf-8"));
+    if (proof !== generated) {
+      throw new Error(`proof string-semantics=${proof} differs from generated string-semantics=${generated}`);
+    }
+  } catch (error) {
+    console.error(`ERROR: ${path.basename(dfyPath)}: ${error instanceof Error ? error.message : String(error)}`);
+    return false;
+  }
+
   let diff = "";
   try {
     diff = execFileSync(
@@ -68,16 +81,64 @@ export function dafnyCheckDiff(genPath: string, dfyPath: string): boolean {
   return true;
 }
 
+/** Read the saved model, rejecting ambiguous headers before verification. */
+function readStringSemantics(content: string): LscOptions["string-semantics"] {
+  const headers = [...content.matchAll(/^\/\/ lsc options:(.*)$/gm)];
+  if (headers.length > 1) throw new Error("generated header: duplicate lsc options header (string-semantics must be unambiguous)");
+  let model = DEFAULT_OPTIONS["string-semantics"];
+  let seen = false;
+  for (const token of (headers[0]?.[1] ?? "").trim().split(/\s+/).filter(Boolean)) {
+    const eq = token.indexOf("=");
+    const key = eq < 0 ? token : token.slice(0, eq);
+    if (key !== "string-semantics") continue;
+    if (seen) throw new Error("generated header: duplicate string-semantics option");
+    seen = true;
+    model = parseOptionValue(key, eq < 0 ? "" : token.slice(eq + 1), "generated header");
+  }
+  return model;
+}
+
+/**
+ * Build verifier arguments from the generated file's `// lsc options:` header.
+ * Reading the saved string model instead of the current project config keeps
+ * verification consistent with generation, even if the config later changes.
+ * Always pass `--unicode-char` explicitly. UTF-16 mode also needs
+ * `--allow-deprecation` because Dafny 4.11 deprecates `--unicode-char:false`.
+ * Other warning categories remain fatal.
+ */
+export function dafnyVerifyArgs(content: string, timeLimit?: number, extraFlags?: string): { args: string[]; error?: string } {
+  let stringSemantics: LscOptions["string-semantics"];
+  try {
+    stringSemantics = readStringSemantics(content);
+  } catch (error) {
+    return { args: [], error: `ERROR: ${error instanceof Error ? error.message : String(error)}` };
+  }
+  const utf16 = stringSemantics === "javascript-utf16";
+  const usesStandardLibrary = content.includes("Std.");
+  if (utf16 && usesStandardLibrary) {
+    return { args: [], error:
+      "ERROR: this proof combines \"string-semantics\": \"javascript-utf16\" with Dafny's standard library. " +
+      "Dafny 4.11 cannot load its Unicode-scalar standard library under --unicode-char:false. " +
+      "Set \"dafny-library\": \"local\" in lemmascript.json or add //@ option dafny-library local, " +
+      "then run lsc regen to regenerate collection helpers. " +
+      "This does not rewrite handwritten Std.* imports or calls; replace those with local proofs or helpers separately." };
+  }
+  const args: string[] = ["verify"];
+  if (usesStandardLibrary) args.push("--standard-libraries");
+  if (timeLimit) args.push("--verification-time-limit", String(timeLimit));
+  if (extraFlags) {
+    for (const tok of extraFlags.split(/\s+/)) if (tok) args.push(tok);
+  }
+  args.push(utf16 ? "--unicode-char:false" : "--unicode-char:true");
+  if (utf16) args.push("--allow-deprecation");
+  return { args };
+}
+
 export function dafnyVerify(dfyPath: string, dir: string, timeLimit?: number, extraFlags?: string): boolean {
   console.log("Running dafny verify...");
   try {
-    const content = readFileSync(dfyPath, "utf-8");
-    const args: string[] = ["verify"];
-    if (content.includes("Std.")) args.push("--standard-libraries");
-    if (timeLimit) args.push("--verification-time-limit", String(timeLimit));
-    if (extraFlags) {
-      for (const tok of extraFlags.split(/\s+/)) if (tok) args.push(tok);
-    }
+    const { args, error } = dafnyVerifyArgs(readFileSync(dfyPath, "utf-8"), timeLimit, extraFlags);
+    if (error) { console.error(error); return false; }
     args.push(dfyPath);
     execFileSync("dafny", args, { cwd: dir, stdio: "inherit" });
     return true;
diff --git a/tools/src/dafny-emit.ts b/tools/src/dafny-emit.ts
index f848f308..f738d339 100644
--- a/tools/src/dafny-emit.ts
+++ b/tools/src/dafny-emit.ts
@@ -7,7 +7,7 @@ import { exactIntegerLiteral, usesName, usesNameInDecl, usesNameInStmts } from "
 import type { Ty } from "./typedir.js";
 import { freshName, freshNameWhere, userNames } from "./names.js";
 import { renameFreeVar } from "./transform.js";
-import { DEFAULT_OPTIONS, type LscOptions } from "./config.js";
+import { DEFAULT_OPTIONS, resolveOptions, type LscOptions } from "./config.js";
 
 /** Fresh binder for a comprehension wrapping the given subexpressions: `base`
  *  verbatim unless one of them references it, then primed until free. A *local*
@@ -219,6 +219,26 @@ const OP_MAP: Record<string, string> = {
   "arrayConcat": "+",
 };
 
+/** Render a JavaScript string without losing its UTF-16 representation.
+ *
+ * JavaScript iteration by index exposes UTF-16 code units, including unpaired
+ * surrogates. Node's UTF-8 file writer would replace an unpaired surrogate if
+ * we emitted it literally, so every non-printable/non-ASCII unit is written as
+ * a Dafny `\\uXXXX` escape. Under `--unicode-char:false`, each escape denotes
+ * exactly one Dafny char and therefore exactly one JavaScript code unit.
+ */
+function escapeDafnyUTF16String(value: string): string {
+  let out = "";
+  for (let i = 0; i < value.length; i++) {
+    const unit = value.charCodeAt(i);
+    if (unit === 0x22) out += '\\"';
+    else if (unit === 0x5c) out += "\\\\";
+    else if (0x20 <= unit && unit <= 0x7e) out += String.fromCharCode(unit);
+    else out += `\\u${unit.toString(16).toUpperCase().padStart(4, "0")}`;
+  }
+  return out;
+}
+
 function mapOp(op: string): string { return OP_MAP[op] ?? op; }
 
 // ── Expression emission ─────────────────────────────────────
@@ -257,7 +277,12 @@ function emitExpr(e: Expr): string {
     // Already canonical decimal; Dafny's `int` is mathematical, so no `n` suffix.
     case "bigint": return e.value;
     case "bool": return e.value ? "true" : "false";
-    case "str": return `"${e.value.replace(/\\/g, '\\\\').replace(/"/g, '\\"').replace(/\n/g, '\\n')}"`;
+    case "str":
+      // Under the default profile the literal is written exactly as before;
+      // only the UTF-16 profile needs code-unit escapes (DESIGN_STRINGS.md §3).
+      return isUtf16()
+        ? `"${escapeDafnyUTF16String(e.value)}"`
+        : `"${e.value.replace(/\\/g, '\\\\').replace(/"/g, '\\"').replace(/\n/g, '\\n')}"`;
 
     case "constructor": {
       // Option constructors (Some/None) may appear in inferred positions
@@ -350,10 +375,18 @@ function emitExpr(e: Expr): string {
           const comp = `seq(|${s}|, ${idx} requires 0 <= ${idx} < |${s}| => ${core})`;
           return bind ? `(var ${s} := ${obj}; ${comp})` : comp;
         }
-        if (e.method === "filter") return `Std.Collections.Seq.Filter(${args[0]}, ${obj})`;
+        if (e.method === "filter") {
+          if (_dafnyLibrary === "stdlib") return `Std.Collections.Seq.Filter(${args[0]}, ${obj})`;
+          needPreamble("SeqFilter");
+          return `SeqFilter(${args[0]}, ${obj})`;
+        }
         // filterMap (synthesized in resolve): drop Nones and unwrap to seq<T>.
         if (e.method === "filterSome") { needPreamble("SeqFilterSome"); needPreamble("OptionType"); return `SeqFilterSome(${obj})`; }
-        if (e.method === "every")  return `Std.Collections.Seq.All(${obj}, ${args[0]})`;
+        if (e.method === "every") {
+          if (_dafnyLibrary === "stdlib") return `Std.Collections.Seq.All(${obj}, ${args[0]})`;
+          needPreamble("SeqAll");
+          return `SeqAll(${obj}, ${args[0]})`;
+        }
         if (e.method === "find") {
           needPreamble("OptionType");
           needPreamble("SeqFind");
@@ -395,9 +428,11 @@ function emitExpr(e: Expr): string {
           }
           return `(exists ${p} :: ${p} in ${obj} && ${body})`;
         }
-        // `.reduce(f, init)` → Std's FoldLeft(f, init, xs) (same arg order).
+        // `.reduce(f, init)` → FoldLeft(f, init, xs), using the selected library.
         if (e.method === "reduce" && args.length === 2) {
-          return `Std.Collections.Seq.FoldLeft(${args[0]}, ${args[1]}, ${obj})`;
+          if (_dafnyLibrary === "stdlib") return `Std.Collections.Seq.FoldLeft(${args[0]}, ${args[1]}, ${obj})`;
+          needPreamble("SeqFoldLeft");
+          return `SeqFoldLeft(${args[0]}, ${args[1]}, ${obj})`;
         }
       }
       // String methods
@@ -958,6 +993,13 @@ function needPreamble(key: string) { _neededPreambles.add(key); }
  *  config plus file directives before emission. */
 let _useSafeSlice = false;
 
+// Source of generated collection helpers, selected independently of string semantics.
+let _dafnyLibrary: LscOptions["dafny-library"] = DEFAULT_OPTIONS["dafny-library"];
+
+// The selected model controls literals, character helpers, and verifier flags.
+let _stringSemantics: LscOptions["string-semantics"] = DEFAULT_OPTIONS["string-semantics"];
+function isUtf16(): boolean { return _stringSemantics === "javascript-utf16"; }
+
 const POW2 = `function Pow2(n: int): int
   requires n >= 0
   decreases n
@@ -1034,6 +1076,28 @@ const SEQ_FILTER_SOME = `function SeqFilterSome<T>(xs: seq<Option<T>>): seq<T>
   else (if xs[0].Some? then [xs[0].value] else []) + SeqFilterSome(xs[1..])
 }`;
 
+const SEQ_FILTER = `function SeqFilter<T(!new)>(p: T -> bool, xs: seq<T>): seq<T>
+  ensures |SeqFilter(p, xs)| <= |xs|
+  ensures forall x :: x in SeqFilter(p, xs) <==> x in xs && p(x)
+  decreases |xs|
+{
+  if |xs| == 0 then []
+  else (if p(xs[0]) then [xs[0]] else []) + SeqFilter(p, xs[1..])
+}`;
+
+const SEQ_ALL = `predicate SeqAll<T>(xs: seq<T>, p: T -> bool)
+  decreases |xs|
+{
+  |xs| == 0 || (p(xs[0]) && SeqAll(xs[1..], p))
+}`;
+
+const SEQ_FOLD_LEFT = `function SeqFoldLeft<T, A>(f: (A, T) -> A, init: A, xs: seq<T>): A
+  decreases |xs|
+{
+  if |xs| == 0 then init
+  else SeqFoldLeft(f, f(init, xs[0]), xs[1..])
+}`;
+
 const SEQ_FIND_INDEX = `function SeqFindIndex<T>(s: seq<T>, p: T -> bool): int
   ensures -1 <= SeqFindIndex(s, p) < |s|
   ensures SeqFindIndex(s, p) >= 0 ==> p(s[SeqFindIndex(s, p)])
@@ -1213,15 +1277,16 @@ const SEQ_SORT_BY = `function {:axiom} SeqSortBy<T(==,!new)>(s: seq<T>, cmp: (T,
 // U+0020, and NOT U+0085 (NEL, which is Cc). See
 // https://tc39.es/ecma262/#sec-white-space and
 // https://tc39.es/ecma262/#sec-line-terminators.
-// `\\U{..}` are Dafny char escapes (not JS: the string
-// is emitted verbatim), so the enumeration below is Dafny source, not decoded.
+// `\\uXXXX` is Dafny's escape form under --unicode-char:false and `\\U{XXXX}`
+// under :true (each rejects the other); STRING_TRIM_SCALAR derives the latter.
+// The enumeration below is emitted Dafny source, not a decoded JS string.
 const STRING_TRIM = `predicate IsJSWhitespace(c: char)
 {
-  c == '\\U{0009}' || c == '\\U{000A}' || c == '\\U{000B}' || c == '\\U{000C}' || c == '\\U{000D}' ||
-  c == '\\U{0020}' || c == '\\U{00A0}' || c == '\\U{1680}' ||
-  ('\\U{2000}' <= c <= '\\U{200A}') ||
-  c == '\\U{2028}' || c == '\\U{2029}' || c == '\\U{202F}' || c == '\\U{205F}' ||
-  c == '\\U{3000}' || c == '\\U{FEFF}'
+  c == '\\u0009' || c == '\\u000A' || c == '\\u000B' || c == '\\u000C' || c == '\\u000D' ||
+  c == '\\u0020' || c == '\\u00A0' || c == '\\u1680' ||
+  ('\\u2000' <= c <= '\\u200A') ||
+  c == '\\u2028' || c == '\\u2029' || c == '\\u202F' || c == '\\u205F' ||
+  c == '\\u3000' || c == '\\uFEFF'
 }
 
 function StringTrimLeft(s: string): string
@@ -1249,6 +1314,10 @@ function StringTrim(s: string): string
   StringTrimRight(StringTrimLeft(s))
 }`;
 
+// The same predicate and trims under `--unicode-char:true`, which the
+// `unicode-scalar` profile verifies under: byte-identical to what was always emitted.
+const STRING_TRIM_SCALAR = STRING_TRIM.replace(/\\u([0-9A-F]{4})/g, "\\U{$1}");
+
 const STRING_TO_LOWER = `function StringToLower(s: string): string
   ensures |StringToLower(s)| == |s|
   decreases |s|
@@ -1271,18 +1340,25 @@ const STRING_TO_UPPER = `function StringToUpper(s: string): string
     [upper] + StringToUpper(s[1..])
 }`;
 
-// `String.fromCharCode(n)` — the inverse of `s.charCodeAt(i)`'s `(s[i] as int)`.
-// Dafny's `char` is a Unicode scalar value, so the argument must miss the
-// surrogate range; that is the `requires`, discharged at each call site. The two
-// `ensures` give callers the round-trip law without unfolding the body.
+// `String.fromCharCode(n)` — the inverse of `s.charCodeAt(i)`'s `(s[i] as int)`
+// in the UTF-16 code-unit model selected by dafny-commands.ts. LemmaScript
+// currently admits the direct 16-bit range; JavaScript's wider ToUint16 coercion
+// remains outside the verified subset.
 const STRING_FROM_CHAR_CODE = `function StringFromCharCode(n: int): string
-  requires 0 <= n < 0xD800 || 0xE000 <= n < 0x110000
+  requires 0 <= n < 0x10000
   ensures |StringFromCharCode(n)| == 1
   ensures (StringFromCharCode(n)[0] as int) == n
 {
   [n as char]
 }`;
 
+// `unicode-scalar` keeps the scalar range that was always required: a surrogate
+// is refused by precondition rather than admitted as a code unit.
+const STRING_FROM_CHAR_CODE_SCALAR = STRING_FROM_CHAR_CODE.replace(
+  "requires 0 <= n < 0x10000",
+  "requires 0 <= n < 0xD800 || 0xE000 <= n < 0x110000",
+);
+
 // `s.repeat(n)` — n copies of s, concatenated. The per-index ensures is stated
 // for the single-character receiver (the common case: padding with one digit).
 const STRING_REPEAT = `function StringRepeat(s: string, n: int): string
@@ -1389,7 +1465,7 @@ const SET_TO_SEQ = `method SetToSeq<T>(s: set<T>) returns (res: seq<T>)
 }`;
 
 /** Preamble code keyed by name. Emitted in this order when needed. */
-const PREAMBLE_CODE: [string, string][] = [
+const PREAMBLE_CODE: [string, string | (() => string)][] = [
   ["OptionType", "datatype Option<T> = None | Some(value: T)"],
   // Opaque carrier for `unknown`-typed values. `(==)` for compare/map-key/match;
   // `(0)` (auto-init ⇒ nonempty) so `havoc` (`:= *`) is well-formed.
@@ -1407,6 +1483,9 @@ const PREAMBLE_CODE: [string, string][] = [
   ["SeqIndexOf", SEQ_INDEX_OF],
   ["SeqFindIndex", SEQ_FIND_INDEX],
   ["SeqFindLastIndex", SEQ_FIND_LAST_INDEX],
+  ["SeqFilter", SEQ_FILTER],
+  ["SeqAll", SEQ_ALL],
+  ["SeqFoldLeft", SEQ_FOLD_LEFT],
   ["SeqFilterSome", SEQ_FILTER_SOME],
   ["SeqFind", SEQ_FIND],
   ["SeqFindLast", SEQ_FIND_LAST],
@@ -1417,10 +1496,10 @@ const PREAMBLE_CODE: [string, string][] = [
   ["StringSplit", STRING_SPLIT],
   ["SeqSort", SEQ_SORT],
   ["SeqSortBy", SEQ_SORT_BY],
-  ["StringTrim", STRING_TRIM],
+  ["StringTrim", () => isUtf16() ? STRING_TRIM : STRING_TRIM_SCALAR],
   ["StringToLower", STRING_TO_LOWER],
   ["StringToUpper", STRING_TO_UPPER],
-  ["StringFromCharCode", STRING_FROM_CHAR_CODE],
+  ["StringFromCharCode", () => isUtf16() ? STRING_FROM_CHAR_CODE : STRING_FROM_CHAR_CODE_SCALAR],
   ["StringRepeat", STRING_REPEAT],
   ["NatToString", NAT_TO_STRING],
   ["IntToString", INT_TO_STRING],
@@ -1537,7 +1616,11 @@ function translatePattern(p: MatchPattern): string {
 
 
 export function emitDafnyFile(file: Module, tsFileName?: string, options: LscOptions = DEFAULT_OPTIONS): string {
+  // Programmatic callers share the CLI's compatibility checks.
+  options = resolveOptions(options, tsFileName ?? "Dafny emission");
   _useSafeSlice = options["safe-slice"];
+  _stringSemantics = options["string-semantics"];
+  _dafnyLibrary = options["dafny-library"];
   resetDafnyNameCache();
   buildRecordCtorMap(file.decls);
   _neededPreambles.clear();
@@ -1598,8 +1681,10 @@ export function emitDafnyFile(file: Module, tsFileName?: string, options: LscOpt
   // Build output with needed preambles
   const lines: string[] = [];
   if (tsFileName) lines.push(`// Generated by lsc from ${tsFileName}`);
+  // Record every UTF-16 selection, including strings introduced by helpers.
+  if (isUtf16()) lines.push("// lsc options: string-semantics=javascript-utf16");
   for (const [key, code] of PREAMBLE_CODE) {
-    if (_neededPreambles.has(key)) { lines.push(""); lines.push(code); }
+    if (_neededPreambles.has(key)) { lines.push(""); lines.push(typeof code === "function" ? code() : code); }
   }
   lines.push(...declLines);
   return lines.join("\n") + "\n";
diff --git a/tools/src/extract.ts b/tools/src/extract.ts
index a9ffaf97..bd9e7dc5 100644
--- a/tools/src/extract.ts
+++ b/tools/src/extract.ts
@@ -57,6 +57,8 @@ let _currentSourceFile: SourceFile | null = null;
 let _inFunctionExtraction = false;
 /** Effective options for the current extraction. Reset at extractModule entry. */
 let _extractOptions: LscOptions = DEFAULT_OPTIONS;
+/** The CLI validates source options before copying a cross-file contract. */
+let _validateDependency: (source: SourceFile) => void = () => {};
 /** Counter for synthetic names used by let-statement array destructuring
  *  when the initializer isn't a bare variable (single-eval temp). */
 let _destrCounter = 0;
@@ -122,6 +124,8 @@ function detectCrossFileExtern(
   if (externalDecl.getSourceFile().getFilePath().endsWith(".d.ts")) return null;
   const sig = callee.getType().getCallSignatures()[0];
   if (!sig) return null;
+  // Includes global declarations selected by TypeScript without an import edge.
+  _validateDependency(externalDecl.getSourceFile());
   // Generic type parameters (e.g. `step<S, A>`). ts-morph reports param/return
   // types in the callee's own type-parameter namespace, so these names match
   // what `params`/`returnType` reference — declare them on the emitted axiom.
@@ -382,23 +386,23 @@ function extractExpr(node: Expression): RawExpr {
     // Always push the head, even when empty: a leading string literal anchors the
     // whole chain as string-typed so each interpolated value is stringified (not
     // added numerically — `${a}${b}` is concatenation, not `a + b`).
-    parts.push({ kind: "str", value: node.getHead().getLiteralText() });
+    parts.push(stringLiteral(node.getHead().getLiteralText(), node));
     for (const span of node.getTemplateSpans()) {
       parts.push(extractExpr(span.getExpression()));
       const text = span.getLiteral().getLiteralText();
-      if (text) parts.push({ kind: "str", value: text });
+      if (text) parts.push(stringLiteral(text, span));
     }
     return parts.reduce((left, right) => ({ kind: "binop", op: "+", left, right }));
   }
 
   // No-substitution template literal: `hello` → "hello"
   if (Node.isNoSubstitutionTemplateLiteral(node)) {
-    return { kind: "str", value: node.getLiteralText() };
+    return stringLiteral(node.getLiteralText(), node);
   }
 
   // String literal
   if (Node.isStringLiteral(node)) {
-    return { kind: "str", value: node.getLiteralValue() };
+    return stringLiteral(node.getLiteralValue(), node);
   }
 
   // Boolean literals: true, false
@@ -823,6 +827,40 @@ function hasExternModeAnnotation(node: Node, keyword: "pure" | "impure", parentS
     .some(r => r.getText().trim() === `//@ ${keyword}`);
 }
 
+/** The first lone surrogate code unit in `value`, or -1. */
+function findLoneSurrogate(value: string): number {
+  for (let i = 0; i < value.length; i++) {
+    const unit = value.charCodeAt(i);
+    if (unit >= 0xD800 && unit <= 0xDBFF) {
+      const next = value.charCodeAt(i + 1);
+      if (next >= 0xDC00 && next <= 0xDFFF) { i++; continue; }
+      return unit;
+    }
+    if (unit >= 0xDC00 && unit <= 0xDFFF) return unit;
+  }
+  return -1;
+}
+
+/** A source string literal, admitted only if the selected string profile can
+ *  represent it (DESIGN_STRINGS.md §3). Under `unicode-scalar` a lone surrogate
+ *  has no Dafny value — and Node's UTF-8 writer would silently replace it on
+ *  the way out — so it is refused here with the source line instead. */
+function stringLiteral(value: string, node: Node): RawExpr {
+  if (_extractOptions["string-semantics"] === "unicode-scalar") {
+    const lone = findLoneSurrogate(value);
+    if (lone >= 0) {
+      const file = node.getSourceFile();
+      const { line } = file.getLineAndColumnAtPos(node.getStart());
+      throw new Error(
+        `${file.getFilePath()}:${line}: string literal contains an unpaired surrogate ` +
+        `U+${lone.toString(16).toUpperCase()}, which "string-semantics": "unicode-scalar" cannot ` +
+        `represent; select string-semantics=javascript-utf16 and dafny-library=local in lemmascript.json or //@ option directives`,
+      );
+    }
+  }
+  return { kind: "str", value };
+}
+
 function externIsImpure(node: Node, name: string, parentStmt?: Node): boolean {
   const pure = hasExternModeAnnotation(node, "pure", parentStmt);
   const impure = hasExternModeAnnotation(node, "impure", parentStmt);
@@ -2041,8 +2079,10 @@ function extractFunctionInner(fn: FunctionDeclaration, parentAnnotations?: Annot
 
 // ── Module extraction ────────────────────────────────────────
 
-export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFAULT_OPTIONS): RawModule {
+export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFAULT_OPTIONS,
+  validateDependency: (source: SourceFile) => void = () => {}): RawModule {
   _extractOptions = options;
+  _validateDependency = validateDependency;
   // Seed the fresh-name check (names.ts) before anything mints: every
   // Identifier token in the module, a deliberate over-approximation.
   setUserNames(new Set(sourceFile.getDescendantsOfKind(SyntaxKind.Identifier).map(i => i.getText())));
diff --git a/tools/src/lsc.ts b/tools/src/lsc.ts
index 9f81e949..1be98245 100755
--- a/tools/src/lsc.ts
+++ b/tools/src/lsc.ts
@@ -5,7 +5,7 @@
  * Pipeline: extract → resolve → narrow → transform → peephole → emit
  */
 
-import { Project, ScriptTarget } from "ts-morph";
+import { Project, ScriptTarget, type SourceFile } from "ts-morph";
 import { existsSync, mkdirSync, readFileSync } from "fs";
 import { execFileSync } from "child_process";
 import { createRequire } from "module";
@@ -219,6 +219,29 @@ function effectiveOptions(
   return { options, configFile: loaded.configFile };
 }
 
+/** Imported contracts must retain the string model used by their source files. */
+function stringModelValidator(source: SourceFile, options: LscOptions, configPath?: string): (source: SourceFile) => void {
+  const seen = new Set<SourceFile>();
+  return start => {
+    const pending = [start];
+    while (pending.length > 0) {
+      const dependency = pending.pop()!;
+      if (seen.has(dependency)) continue;
+      seen.add(dependency);
+      pending.push(...dependency.getReferencedSourceFiles());
+      // Declaration files describe host APIs; follow re-exports through them,
+      // but compare models only for source files that can carry verified code.
+      if (dependency === source || dependency.isDeclarationFile()) continue;
+      const { options: imported } = effectiveOptions(dependency.getFilePath(), dependency.getFullText(), configPath);
+      if (imported["string-semantics"] !== options["string-semantics"]) {
+        throw new Error(`${source.getFilePath()}: string-semantics=${options["string-semantics"]} differs from `
+          + `${dependency.getFilePath()} (string-semantics=${imported["string-semantics"]}); `
+          + "use the same string model across source dependencies");
+      }
+    }
+  };
+}
+
 /** `lsc config [file.ts]` — report discovery, effective values, and routing. */
 function runConfig(filePath: string | undefined, configPath?: string): void {
   if (!filePath) {
@@ -331,8 +354,13 @@ function runFile(
   const leanModuleDirective = fullText.match(/\/\/@ lean-module ([A-Za-z0-9_.\-]+)/);
   const leanModuleOverride = leanModuleDirective ? leanModuleDirective[1] : undefined;
 
+  // Validate the actual dependency graph, not unrelated files in the tsconfig.
+  // Library selection may differ; only the string model changes contract meaning.
+  const validateDependency = stringModelValidator(sourceFile, options, configPath);
+  validateDependency(sourceFile);
+
   // Extract: ts-morph → Raw IR
-  const raw = extractModule(sourceFile, options);
+  const raw = extractModule(sourceFile, options, validateDependency);
 
   if (cmd === "extract") {
     console.log(JSON.stringify(raw, null, 2));
@@ -410,6 +438,13 @@ function runFile(
   }
 
   // ── Lean backend ──────────────────────────────────────────
+  // Dafny-only profile: Lean's `String` is a sequence of Unicode scalars and
+  // LemmaScript has no UTF-16 encoding for it (DESIGN_STRINGS.md §4). Refuse
+  // rather than emit scalar Lean for a code-unit claim.
+  if (options["string-semantics"] === "javascript-utf16") {
+    console.error('ERROR: "string-semantics": "javascript-utf16" is not available for --backend=lean; use --backend=dafny or select "unicode-scalar" in lemmascript.json or a //@ option directive.');
+    process.exit(1);
+  }
   const leanBase = leanModuleOverride ?? base;
   const specPath = path.join(dir, `${leanBase}.spec.lean`);
   const specImport = existsSync(specPath) ? `«${leanBase}.spec»` : undefined;
diff --git a/tools/test-fixtures.sh b/tools/test-fixtures.sh
index b6fc9e4c..81903d4f 100755
--- a/tools/test-fixtures.sh
+++ b/tools/test-fixtures.sh
@@ -42,6 +42,8 @@ trap 'rm -rf "$fixture_dir"' EXIT
 cp tools/fixtures/deterministic-extern-equality.ts "$fixture_dir/deterministic.ts"
 cp tools/fixtures/impure-extern-equality.ts "$fixture_dir/impure.ts"
 cp examples/safeSlice.ts "$fixture_dir/legacy-safe-slice.ts"
+cp -R tools/fixtures/utf16-project "$fixture_dir/utf16-project"
+cp tools/fixtures/unpaired-surrogate.ts "$fixture_dir/unpaired.ts"
 
 npx tsx tools/src/lsc.ts gen --backend=dafny "$fixture_dir/impure.ts"
 if ! grep -Fq 'method {:axiom} rollDie' "$fixture_dir/impure.dfy.gen"; then
@@ -172,3 +174,108 @@ expect_failure \
   "proof-dir silently bypassed a sibling hand-written proof" \
   npx tsx tools/src/lsc.ts gen --backend=dafny "$config_fixture/src/legacy.ts"
 expect_absent "$config_fixture/proofs/src/legacy.dfy"
+
+# ── String profile and collection library ─────────────────────────────────
+# The ordinary example selects both options in source, without a JSON config.
+cp examples/utf16.ts "$fixture_dir/utf16-example.ts"
+npx tsx tools/src/lsc.ts check --backend=dafny --time-limit=10 "$fixture_dir/utf16-example.ts"
+grep -Fq '// lsc options: string-semantics=javascript-utf16' "$fixture_dir/utf16-example.dfy.gen"
+
+# Under "string-semantics": "javascript-utf16" a JavaScript string is a UTF-16
+# code-unit sequence: astral characters occupy two Dafny chars and lone
+# surrogates stay representable. The header token is what dafnyVerify maps to
+# --unicode-char:false --allow-deprecation.
+utf16="$fixture_dir/utf16-project/src/utf16.ts"
+utf16_gen="$fixture_dir/utf16-project/src/utf16.dfy.gen"
+if ! npx tsx tools/src/lsc.ts config "$utf16" | grep -Fq '"string-semantics": "javascript-utf16"'; then
+  echo "ERROR: lsc config did not report string-semantics=javascript-utf16"
+  exit 1
+fi
+if ! npx tsx tools/src/lsc.ts config "$utf16" | grep -Fq '"dafny-library": "local"'; then
+  echo "ERROR: lsc config did not report the explicit local library choice"
+  exit 1
+fi
+npx tsx tools/src/lsc.ts check --backend=dafny --time-limit=10 "$utf16"
+grep -Fq '// lsc options: string-semantics=javascript-utf16' "$utf16_gen"
+grep -Fq '"\uD83D\uDE00"' "$utf16_gen"
+grep -Fq '"\uD83D"' "$utf16_gen"
+if grep -Fq 'Std.Collections' "$utf16_gen"; then
+  echo "ERROR: javascript-utf16 emitted a Dafny standard-library call"
+  exit 1
+fi
+
+# The library has a fixed stdlib default; UTF-16 never silently changes it.
+cp -R tools/fixtures/config-incompatible-strings "$fixture_dir/incompatible-strings"
+incompatible="$fixture_dir/incompatible-strings/source.ts"
+expect_failure "UTF-16 silently changed the default library" \
+  npx tsx tools/src/lsc.ts gen --backend=dafny "$incompatible"
+expect_failure "UTF-16 accepted an explicit stdlib choice" \
+  npx tsx tools/src/lsc.ts gen --backend=dafny \
+    --config="$fixture_dir/incompatible-strings/stdlib.json" "$incompatible"
+expect_absent "$fixture_dir/incompatible-strings/source.dfy.gen"
+expect_absent "$fixture_dir/incompatible-strings/source.dfy"
+
+# Prove the same collection contracts with default stdlib, scalar/local, and
+# UTF-16/local. All generated artifacts stay in the temporary fixture directory.
+cp -R tools/fixtures/collection-library-project "$fixture_dir/local-collections"
+cp tools/fixtures/collection-library-project/collections.ts "$fixture_dir/standard-collections.ts"
+cp tools/fixtures/collection-library-project/collections.ts "$fixture_dir/utf16-project/collections.ts"
+npx tsx tools/src/lsc.ts gen --backend=dafny "$fixture_dir/standard-collections.ts"
+# Standard Filter is opaque. Add proof steps that expose its definition and
+# unfold the three input elements plus the empty tail; check enforces additions-only.
+node --input-type=module - "$fixture_dir/standard-collections.dfy" <<'JS'
+import { readFileSync, writeFileSync } from "node:fs";
+const path = process.argv[2];
+let proof = readFileSync(path, "utf8");
+for (const [name, type, expected] of [
+  ["positiveNumbers", "int", "[1, 2]"],
+  ["nonemptyStrings", "string", '["a", "bc"]'],
+]) {
+  const start = new RegExp(`lemma ${name}_ensures\\(\\)[\\s\\S]*?\\{\\n`);
+  if (!start.test(proof)) throw new Error(`Missing proof body for ${name}`);
+  proof = proof.replace(start, "$&  reveal Std.Collections.Seq.Filter();\n"
+    + `  assert {:fuel Std.Collections.Seq.Filter<${type}>, 4, 5} ${name}() == ${expected};\n`);
+}
+writeFileSync(path, proof);
+JS
+npx tsx tools/src/lsc.ts check --backend=dafny --time-limit=10 "$fixture_dir/standard-collections.ts"
+for helper in Filter All FoldLeft; do
+  grep -Fq "Std.Collections.Seq.$helper(" "$fixture_dir/standard-collections.dfy.gen"
+done
+for source in "$fixture_dir/local-collections/collections.ts" "$fixture_dir/utf16-project/collections.ts"; do
+  npx tsx tools/src/lsc.ts check --backend=dafny --time-limit=10 "$source"
+  generated="${source%.ts}.dfy.gen"
+  if grep -Fq 'Std.' "$generated"; then
+    echo "ERROR: dafny-library=local emitted a standard-library reference"
+    exit 1
+  fi
+  for helper in SeqFilter SeqAll SeqFoldLeft; do grep -Fq "$helper<" "$generated"; done
+done
+if grep -Fq '// lsc options:' "$fixture_dir/local-collections/collections.dfy.gen"; then
+  echo "ERROR: selecting local helpers changed scalar string semantics"
+  exit 1
+fi
+grep -Fq '// lsc options: string-semantics=javascript-utf16' "$fixture_dir/utf16-project/collections.dfy.gen"
+
+expect_failure \
+  "Dafny standard library was combined with javascript-utf16 strings" \
+  npx tsx -e 'import { dafnyVerify } from "./tools/src/dafny-commands.ts"; process.exit(dafnyVerify("tools/fixtures/string-with-standard-library.dfy", ".") ? 0 : 1)'
+
+expect_failure \
+  "javascript-utf16 was accepted by the Lean backend" \
+  npx tsx tools/src/lsc.ts gen --backend=lean "$fixture_dir/utf16-project/src/lean-rejected.ts"
+expect_absent "$fixture_dir/utf16-project/src/lean-rejected.def.lean"
+
+# The default profile cannot represent a lone surrogate: refused at extraction
+# with the source line, not silently replaced by the UTF-8 file writer.
+expect_failure \
+  "unicode-scalar accepted an unpaired surrogate literal" \
+  npx tsx tools/src/lsc.ts gen --backend=dafny "$fixture_dir/unpaired.ts"
+expect_absent "$fixture_dir/unpaired.dfy.gen"
+
+# The default profile leaves generated text exactly as before: no header token.
+npx tsx tools/src/lsc.ts gen --backend=dafny "$fixture_dir/legacy-safe-slice.ts"
+if grep -Fq '// lsc options:' "$fixture_dir/legacy-safe-slice.dfy.gen"; then
+  echo "ERROR: unicode-scalar stamped an options header"
+  exit 1
+fi
diff --git a/tools/tests/batch-options.test.ts b/tools/tests/batch-options.test.ts
index 0b676321..03151958 100644
--- a/tools/tests/batch-options.test.ts
+++ b/tools/tests/batch-options.test.ts
@@ -104,7 +104,7 @@ for (const { name, entry, flags, expected } of cases) {
   test(name, posixOnly, () => {
     const result = runCli([entry], ["check", ...flags]);
     assert.equal(result.status, 0, result.stderr);
-    assert.deepEqual(result.calls, [["verify", ...expected, join(result.dir, "a.dfy")]]);
+    assert.deepEqual(result.calls, [["verify", ...expected, "--unicode-char:true", join(result.dir, "a.dfy")]]);
   });
 }
 
@@ -112,8 +112,8 @@ test("batch overrides apply to every entry, including entries without defaults",
   const result = runCli(["a.ts 300 --isolate-assertions", "b.ts"], ["check", "--time-limit=120", "--extra-flags=--cores=2"]);
   assert.equal(result.status, 0, result.stderr);
   assert.deepEqual(result.calls, [
-    ["verify", "--verification-time-limit", "120", "--cores=2", join(result.dir, "a.dfy")],
-    ["verify", "--verification-time-limit", "120", "--cores=2", join(result.dir, "b.dfy")],
+    ["verify", "--verification-time-limit", "120", "--cores=2", "--unicode-char:true", join(result.dir, "a.dfy")],
+    ["verify", "--verification-time-limit", "120", "--cores=2", "--unicode-char:true", join(result.dir, "b.dfy")],
   ]);
 });
 
@@ -124,7 +124,7 @@ for (const flags of [[], ["--extra-flags=--cores=2"]]) {
     assert.match(result.stdout, /a\.ts \(timeout 61s > 60s, gen-check only\)/);
     assert.ok(result.files.includes("a.dfy.gen"));
     assert.deepEqual(result.calls, [[
-      "verify", "--verification-time-limit", "11", ...(flags.length ? ["--cores=2"] : []), join(result.dir, "b.dfy"),
+      "verify", "--verification-time-limit", "11", ...(flags.length ? ["--cores=2"] : []), "--unicode-char:true", join(result.dir, "b.dfy"),
     ]]);
   });
 }
@@ -132,7 +132,7 @@ for (const flags of [[], ["--extra-flags=--cores=2"]]) {
 test("an explicit file keeps its existing CLI behavior", posixOnly, () => {
   const result = runCli(["a.ts 11 --isolate-assertions"], ["check", "a.ts", "--time-limit=120", "--extra-flags=--cores=2"]);
   assert.equal(result.status, 0, result.stderr);
-  assert.deepEqual(result.calls, [["verify", "--verification-time-limit", "120", "--cores=2", join(result.dir, "a.dfy")]]);
+  assert.deepEqual(result.calls, [["verify", "--verification-time-limit", "120", "--cores=2", "--unicode-char:true", join(result.dir, "a.dfy")]]);
 });
 
 for (const cmd of ["gen", "gen-check"]) {
diff --git a/tools/tests/config.test.ts b/tools/tests/config.test.ts
index d0bcae33..58714e7a 100644
--- a/tools/tests/config.test.ts
+++ b/tools/tests/config.test.ts
@@ -2,7 +2,7 @@ import { test } from "node:test";
 import assert from "node:assert/strict";
 import { execFileSync } from "node:child_process";
 
-import { parseFileOptions } from "../src/config.ts";
+import { parseFileOptions, resolveOptions, validateOptions } from "../src/config.ts";
 
 test("parses a genuine leading option comment", () => {
   assert.deepEqual(
@@ -145,7 +145,7 @@ for (const [directive, message] of [
   ["option", "expected //@ option <key> <value>"],
   ["option safe-slice", "expected //@ option <key> <value>"],
   ["option safe-slice true extra", "expected //@ option <key> <value>"],
-  ["option missing true", "unknown option 'missing' (known options: extern-default, safe-slice, proof-dir)"],
+  ["option missing true", "unknown option 'missing' (known options: extern-default, safe-slice, proof-dir, string-semantics, dafny-library)"],
   ["option safe-slice yes", "option 'safe-slice' must be true or false"],
   ["option extern-default invalid", "option 'extern-default' must be one of: pure, impure"],
   ["option proof-dir proofs", "option 'proof-dir' is config-only"],
@@ -170,3 +170,63 @@ for (const directives of [
     );
   });
 }
+
+test("string-semantics is an enum whose default is today's Unicode-scalar model", () => {
+  assert.equal(resolveOptions({}, "lemmascript.json")["string-semantics"], "unicode-scalar");
+  assert.deepEqual(
+    validateOptions({ "string-semantics": "javascript-utf16" }, "lemmascript.json"),
+    { "string-semantics": "javascript-utf16" },
+  );
+  assert.throws(
+    () => validateOptions({ "string-semantics": "utf16" }, "lemmascript.json"),
+    /must be one of: unicode-scalar, javascript-utf16/,
+  );
+});
+
+test("string and library directives override project defaults before compatibility checks", () => {
+  const file = parseFileOptions("//@ option string-semantics javascript-utf16\n//@ option dafny-library local\n", "example.ts");
+  const options = resolveOptions({ "string-semantics": "unicode-scalar", "dafny-library": "stdlib", ...file }, "example.ts");
+  assert.equal(options["string-semantics"], "javascript-utf16");
+  assert.equal(options["dafny-library"], "local");
+  assert.throws(() => resolveOptions(parseFileOptions("//@ option string-semantics javascript-utf16\n", "example.ts"), "example.ts"),
+    /incompatible/);
+});
+
+test("Dafny library defaults to stdlib and local works with scalar strings", () => {
+  assert.equal(resolveOptions({}, "lemmascript.json")["dafny-library"], "stdlib");
+  const options = resolveOptions(validateOptions({ "dafny-library": "local" }, "lemmascript.json"), "lemmascript.json");
+  assert.equal(options["dafny-library"], "local");
+  assert.equal(options["string-semantics"], "unicode-scalar");
+  assert.ok(Object.isFrozen(options));
+});
+
+for (const library of [undefined, "stdlib"] as const) {
+  test(`UTF-16 rejects ${library === undefined ? "the default" : "explicit"} stdlib choice`, () => {
+    const explicit = library === undefined
+      ? { "string-semantics": "javascript-utf16" }
+      : { "string-semantics": "javascript-utf16", "dafny-library": library };
+    assert.throws(() => resolveOptions(validateOptions(explicit, "lemmascript.json"), "lemmascript.json"),
+      /lemmascript\.json:.*"string-semantics": "javascript-utf16".*"dafny-library": "stdlib".*"local" explicitly/);
+  });
+}
+
+test("UTF-16 requires an explicit local library choice", () => {
+  const explicit = validateOptions({ "string-semantics": "javascript-utf16", "dafny-library": "local" }, "lemmascript.json");
+  assert.equal(resolveOptions(explicit, "lemmascript.json")["dafny-library"], "local");
+});
+
+test("Dafny library accepts only registered values in config and file directives", () => {
+  for (const value of [true, "standard", null]) {
+    assert.throws(() => validateOptions({ "dafny-library": value }, "lemmascript.json"), /must be one of: stdlib, local/);
+  }
+  assert.deepEqual(parseFileOptions("//@ option dafny-library local\n", "example.ts"), { "dafny-library": "local" });
+  assert.throws(() => parseFileOptions("//@ option dafny-library standard\n", "example.ts"), /must be one of: stdlib, local/);
+});
+
+for (const [key, value] of [["string-semantics", "javascript-utf16"], ["dafny-library", "local"]]) {
+  test(`${key} retains duplicate and placement checks`, () => {
+    const directive = `//@ option ${key} ${value}\n`;
+    assert.throws(() => parseFileOptions(directive + directive, "example.ts"), /duplicate option/);
+    assert.throws(() => parseFileOptions("const value = 1;\n" + directive, "example.ts"), /before the first source statement/);
+  });
+}
diff --git a/tools/tests/dafny-commands.test.ts b/tools/tests/dafny-commands.test.ts
index 6b2c68aa..9ae3ac59 100644
--- a/tools/tests/dafny-commands.test.ts
+++ b/tools/tests/dafny-commands.test.ts
@@ -3,7 +3,8 @@ import assert from "node:assert/strict";
 import { chmodSync, mkdtempSync, rmSync, writeFileSync } from "node:fs";
 import { tmpdir } from "node:os";
 import { join } from "node:path";
-import { dafnyCheckDiff } from "../src/dafny-commands.ts";
+import { DEFAULT_OPTIONS, OPTION_SPECS, validateOptions } from "../src/config.ts";
+import { dafnyCheckDiff, dafnyVerifyArgs } from "../src/dafny-commands.ts";
 
 function fixture(gen: string, proof: string, check: (g: string, p: string, dir: string) => void): void {
   const dir = mkdtempSync(join(tmpdir(), "lsc-git-review-"));
@@ -79,3 +80,119 @@ for (const script of ["exit 1", "printf 'not a patch\\n'; exit 1", "printf 'part
 test("missing Git executable is not success", () => {
   fixture("x\n", "y\n", (g, p, dir) => env({ PATH: dir }, () => assert.equal(dafnyCheckDiff(g, p), false)));
 });
+
+test("no header token uses the configuration default", () => {
+  const explicit = dafnyVerifyArgs(`// lsc options: string-semantics=${DEFAULT_OPTIONS["string-semantics"]}\n`);
+  assert.equal(explicit.error, undefined);
+  assert.deepEqual(dafnyVerifyArgs("// Generated by lsc from a.ts\nmethod M() {}\n"), explicit);
+  assert.deepEqual(dafnyVerifyArgs("method M() {}\n"), explicit);
+});
+
+test("every registered string model is accepted in the proof header", () => {
+  for (const value of OPTION_SPECS["string-semantics"].values) {
+    const result = dafnyVerifyArgs(`// lsc options: string-semantics=${value}\n`);
+    assert.equal(result.error, undefined);
+    assert.ok(result.args.includes(value === "javascript-utf16" ? "--unicode-char:false" : "--unicode-char:true"));
+  }
+});
+
+test("javascript-utf16 selects code-unit chars and only the deprecation waiver", () => {
+  const { args, error } = dafnyVerifyArgs("// Generated by lsc from a.ts\n// lsc options: string-semantics=javascript-utf16\n");
+  assert.equal(error, undefined);
+  assert.deepEqual(args, ["verify", "--unicode-char:false", "--allow-deprecation"]);
+});
+
+for (const secondModel of ["unicode-scalar", "javascript-utf16"]) {
+  test(`duplicate proof options headers are rejected even when the second model is ${secondModel}`, () => {
+    const result = dafnyVerifyArgs("// lsc options: string-semantics=javascript-utf16\n"
+      + `// lsc options: string-semantics=${secondModel}\n`);
+    assert.deepEqual(result.args, []);
+    assert.match(result.error ?? "", /duplicate lsc options header/);
+  });
+  test(`duplicate string model tokens are rejected even when the second model is ${secondModel}`, () => {
+    const result = dafnyVerifyArgs("// lsc options: string-semantics=javascript-utf16 "
+      + `string-semantics=${secondModel}\n`);
+    assert.deepEqual(result.args, []);
+    assert.match(result.error ?? "", /duplicate string-semantics option/);
+  });
+}
+
+test("proof additions cannot introduce UTF-16 over the generated scalar default", () => {
+  const generated = "// Generated by lsc from a.ts\nmethod M() {}\n";
+  fixture(generated, "// lsc options: string-semantics=javascript-utf16\n" + generated,
+    (g, p) => assert.equal(dafnyCheckDiff(g, p), false));
+});
+
+test("proof additions cannot override a generated UTF-16 header", () => {
+  const generated = "// Generated by lsc from a.ts\n"
+    + "// lsc options: string-semantics=javascript-utf16\nmethod M() {}\n";
+  fixture(generated, "// lsc options: string-semantics=unicode-scalar\n" + generated,
+    (g, p) => assert.equal(dafnyCheckDiff(g, p), false));
+  fixture(generated, generated + "\nlemma Proof() {}\n",
+    (g, p) => assert.equal(dafnyCheckDiff(g, p), true));
+});
+
+for (const reference of [
+  "import opened Std.Arithmetic.Mul",
+  "function all(xs: seq<int>): bool { Std.Collections.Seq.All(xs, x => x > 0) }",
+]) {
+  test(`UTF-16 library diagnostic explains local helpers and proof additions: ${reference}`, () => {
+    const { args, error } = dafnyVerifyArgs(`// lsc options: string-semantics=javascript-utf16\n${reference}\n`);
+    assert.deepEqual(args, []);
+    assert.match(error ?? "", /string-semantics/);
+    assert.match(error ?? "", /Set "dafny-library": "local" in lemmascript\.json/);
+    assert.match(error ?? "", /\/\/@ option dafny-library local/);
+    assert.match(error ?? "", /lsc regen/);
+    assert.match(error ?? "", /does not rewrite handwritten Std\.\* imports or calls/);
+  });
+}
+
+test("Unicode-scalar proofs can still use the standard library", () => {
+  const { args, error } = dafnyVerifyArgs("import opened Std.Arithmetic.Mul\n");
+  assert.equal(error, undefined);
+  assert.deepEqual(args, ["verify", "--standard-libraries", "--unicode-char:true"]);
+});
+
+for (const token of ["string-semantics=utf8", "string-semantics=", "string-semantics"]) {
+  test(`proof header uses config validation for invalid token: ${token}`, () => {
+    const value = token.includes("=") ? token.slice(token.indexOf("=") + 1) : "";
+    let message = "";
+    assert.throws(() => validateOptions({ "string-semantics": value }, "generated header"), (error: Error) => {
+      message = error.message;
+      return true;
+    });
+    const result = dafnyVerifyArgs(`// lsc options: ${token}\n`);
+    assert.deepEqual(result, { args: [], error: `ERROR: ${message}` });
+    assert.match(result.error ?? "", /generated header: option 'string-semantics' must be one of:/);
+  });
+}
+
+test("a later valid token does not hide an invalid string model", () => {
+  assert.deepEqual(
+    dafnyVerifyArgs("// lsc options: string-semantics=utf8 string-semantics=javascript-utf16\n"),
+    dafnyVerifyArgs("// lsc options: string-semantics=utf8\n"),
+  );
+});
+
+test("proof header settings are independent of the current project config", () => {
+  fixture("", "", (_gen, _proof, dir) => {
+    const previousDirectory = process.cwd();
+    try {
+      process.chdir(dir);
+      for (const value of OPTION_SPECS["string-semantics"].values) {
+        writeFileSync(join(dir, "lemmascript.json"), JSON.stringify({ "string-semantics": value }));
+        assert.deepEqual(dafnyVerifyArgs("// lsc options: string-semantics=javascript-utf16\n").args,
+          ["verify", "--unicode-char:false", "--allow-deprecation"]);
+        assert.deepEqual(dafnyVerifyArgs("// lsc options: string-semantics=unicode-scalar\n").args,
+          ["verify", "--unicode-char:true"]);
+      }
+    } finally { process.chdir(previousDirectory); }
+  });
+});
+
+test("time limit and extra flags keep their positions before the char-mode pin", () => {
+  assert.deepEqual(
+    dafnyVerifyArgs("method M() {}\n", 30, "--isolate-assertions").args,
+    ["verify", "--verification-time-limit", "30", "--isolate-assertions", "--unicode-char:true"],
+  );
+});
diff --git a/tools/tests/dafny-emit.test.ts b/tools/tests/dafny-emit.test.ts
new file mode 100644
index 00000000..d47ae07f
--- /dev/null
+++ b/tools/tests/dafny-emit.test.ts
@@ -0,0 +1,92 @@
+import { test } from "node:test";
+import assert from "node:assert/strict";
+import { DEFAULT_OPTIONS, resolveOptions } from "../src/config.ts";
+import { emitDafnyFile } from "../src/dafny-emit.ts";
+import type { Decl, Expr, Module } from "../src/ir.ts";
+
+const utf16 = resolveOptions({ "string-semantics": "javascript-utf16", "dafny-library": "local" }, "test");
+const optionsHeader = /^\/\/ lsc options: string-semantics=javascript-utf16$/m;
+
+function moduleWith(...decls: Decl[]): Module {
+  return { comment: "", imports: [], options: [], decls };
+}
+
+const numbers = moduleWith({ kind: "const", name: "answer", type: { kind: "int" }, value: { kind: "num", value: 42 } });
+const stringType: Decl = { kind: "type-alias", name: "Text", target: { kind: "string" } };
+
+test("programmatic emission rejects UTF-16 with the default standard library", () => {
+  assert.throws(() => emitDafnyFile(numbers, "numbers.ts", { ...DEFAULT_OPTIONS, "string-semantics": "javascript-utf16" }),
+    /numbers\.ts:.*javascript-utf16.*dafny-library.*stdlib.*local/);
+});
+
+for (const [method, helper, resultType] of [
+  ["filter", "Filter", { kind: "array", elem: { kind: "int" } }],
+  ["every", "All", { kind: "bool" }],
+  ["reduce", "FoldLeft", { kind: "int" }],
+] as const) {
+  test(`${method} follows the library option independently of string semantics`, () => {
+    const callback: Expr = { kind: "var", name: "callback" };
+    const file = moduleWith({ kind: "const", name: "value", type: resultType, value: {
+      kind: "methodCall", obj: { kind: "var", name: "values" }, objTy: { kind: "array", elem: { kind: "int" } },
+      method, args: method === "reduce" ? [callback, { kind: "num", value: 0 }] : [callback], monadic: false,
+    } });
+    const standard = emitDafnyFile(file, "collections.ts");
+    assert.ok(standard.includes(`Std.Collections.Seq.${helper}(`));
+    for (const options of [resolveOptions({ "dafny-library": "local" }, "test"), utf16]) {
+      const local = emitDafnyFile(file, "collections.ts", options);
+      assert.doesNotMatch(local, /Std\./);
+      assert.match(local, new RegExp(`(?:function|predicate) Seq${helper}<`));
+    }
+    // A local emission must not change the next file's default library.
+    assert.equal(emitDafnyFile(file, "collections.ts"), standard);
+    assert.equal(emitDafnyFile(file, "collections.ts", resolveOptions({ "dafny-library": "stdlib" }, "test")), standard);
+  });
+}
+
+test("UTF-16 stamps numeric-only modules so proof additions use the selected model", () => {
+  assert.match(emitDafnyFile(numbers, "numbers.ts", utf16), optionsHeader);
+  assert.doesNotMatch(emitDafnyFile(numbers, "numbers.ts"), optionsHeader);
+  assert.match(emitDafnyFile(numbers, "numbers.ts", utf16), optionsHeader);
+});
+
+test("string profile and literal encoding reset between files", () => {
+  const literal = moduleWith({ kind: "const", name: "emoji", type: { kind: "string" }, value: { kind: "str", value: "😀" } });
+  const encoded = emitDafnyFile(literal, "literal.ts", utf16);
+  assert.match(encoded, optionsHeader);
+  assert.ok(encoded.includes('"\\uD83D\\uDE00"'));
+
+  // Omit the options argument so the default must replace the previous profile.
+  const scalar = emitDafnyFile(literal, "literal.ts");
+  assert.doesNotMatch(scalar, optionsHeader);
+  assert.ok(scalar.includes('"😀"'));
+  assert.equal(emitDafnyFile(literal, "literal.ts", utf16), encoded);
+});
+
+test("string helper preambles do not leak into the next file", () => {
+  const baseline = emitDafnyFile(numbers, "numbers.ts", utf16);
+  const search = moduleWith({ kind: "const", name: "position", type: { kind: "int" }, value: {
+    kind: "methodCall", obj: { kind: "str", value: "hello" }, objTy: { kind: "string" },
+    method: "indexOf", args: [{ kind: "str", value: "e" }], monadic: false,
+  } });
+  const output = emitDafnyFile(search, "search.ts", utf16);
+  assert.match(output, optionsHeader);
+  assert.match(output, /function StringIndexOf\(/);
+  assert.equal(emitDafnyFile(numbers, "numbers.ts", utf16), baseline);
+});
+
+for (const inNamespace of [false, true]) {
+  test(`string profile resets after failed emission${inNamespace ? " inside a namespace" : ""}`, () => {
+    const baseline = emitDafnyFile(numbers, "numbers.ts", utf16);
+    const declarations: Decl[] = [stringType, {
+      kind: "const", name: "unsupported", type: { kind: "int" }, value: {
+        kind: "methodCall", obj: { kind: "str", value: "hello" }, objTy: { kind: "string" },
+        method: "unsupported", args: [], monadic: false,
+      },
+    }];
+    const failing = inNamespace
+      ? moduleWith({ kind: "namespace", name: "Example", decls: declarations })
+      : moduleWith(...declarations);
+    assert.throws(() => emitDafnyFile(failing, "unsupported.ts", utf16), /Unsupported Dafny method call/);
+    assert.equal(emitDafnyFile(numbers, "numbers.ts", utf16), baseline);
+  });
+}
diff --git a/tools/tests/dafny-string-profile.test.ts b/tools/tests/dafny-string-profile.test.ts
new file mode 100644
index 00000000..3d3eb2a8
--- /dev/null
+++ b/tools/tests/dafny-string-profile.test.ts
@@ -0,0 +1,99 @@
+import { test } from "node:test";
+import assert from "node:assert/strict";
+import { spawnSync } from "node:child_process";
+import { chmodSync, existsSync, mkdirSync, mkdtempSync, readFileSync, realpathSync, rmSync, writeFileSync } from "node:fs";
+import { createRequire } from "node:module";
+import { tmpdir } from "node:os";
+import { delimiter, join } from "node:path";
+import { fileURLToPath } from "node:url";
+
+const cli = fileURLToPath(new URL("../src/lsc.ts", import.meta.url));
+const loader = createRequire(import.meta.url).resolve("tsx");
+const utf16 = "//@ option string-semantics javascript-utf16\n//@ option dafny-library local\n";
+const header = "// lsc options: string-semantics=javascript-utf16\n";
+const posixOnly = { skip: process.platform === "win32" };
+
+function fixture(source: string, useFakeVerifier: boolean, run: (f: {
+  dir: string; proof: string; gen: string; marker: string;
+  cli: (args: string[]) => { status: number | null; output: string };
+}) => void): void {
+  const dir = realpathSync(mkdtempSync(join(tmpdir(), "lsc-string-profile-")));
+  try {
+    writeFileSync(join(dir, "source.ts"), source);
+    const marker = join(dir, "verifier-called");
+    const env = { ...process.env, LSC_TEST_VERIFIER_MARKER: marker };
+    if (useFakeVerifier) {
+      const bin = join(dir, "bin");
+      mkdirSync(bin);
+      const verifier = join(bin, "dafny");
+      writeFileSync(verifier, '#!/bin/sh\nprintf "called\\n" > "$LSC_TEST_VERIFIER_MARKER"\nexit 0\n');
+      chmodSync(verifier, 0o755);
+      env.PATH = `${bin}${delimiter}${env.PATH ?? ""}`;
+    }
+    run({ dir, proof: join(dir, "source.dfy"), gen: join(dir, "source.dfy.gen"), marker,
+      cli(args) {
+        const result = spawnSync(process.execPath, ["--import", loader, cli,
+          ...args, "--backend=dafny", "--time-limit=10", "source.ts"], {
+          cwd: dir, env, encoding: "utf8", timeout: 60_000,
+        });
+        assert.ifError(result.error);
+        return { status: result.status, output: result.stdout + result.stderr };
+      },
+    });
+  } finally {
+    rmSync(dir, { recursive: true, force: true });
+  }
+}
+
+const lengthSource = "export function codeUnitLength(value: string): number { return value.length; }\n";
+for (const command of [["check"], ["gen-check"], ["regen"], ["regen", "--no-verify"]]) {
+  for (const profile of ["javascript-utf16", "unicode-scalar"]) {
+    test(`${command.join(" ")}: proof additions cannot change the generated ${profile} model`, posixOnly, () => {
+      fixture("//@ backend dafny\n" + (profile === "javascript-utf16" ? utf16 : "") + lengthSource, true, f => {
+        const generated = f.cli(["gen"]);
+        assert.equal(generated.status, 0, generated.output);
+        const original = readFileSync(f.proof, "utf8");
+        const override = profile === "javascript-utf16"
+          ? "// lsc options: string-semantics=unicode-scalar\n"
+          : header;
+        const claim = profile === "javascript-utf16"
+          ? 'lemma WrongLength() ensures codeUnitLength("😀") == 1 {}\n'
+          : 'lemma ChangedModel() ensures codeUnitLength("\\uD83D\\uDE00") == 2 {}\n';
+        writeFileSync(f.proof, override + original + "\n" + claim);
+        const result = f.cli(command);
+        assert.equal(result.status, 1, result.output);
+        assert.match(result.output, /string-semantics|duplicate lsc options header/);
+        assert.equal(existsSync(f.marker), false, "the model guard must reject the proof before invoking Dafny");
+        assert.equal(readFileSync(f.gen, "utf8"), original);
+      });
+    });
+  }
+}
+
+test("ordinary UTF-16 proof additions still reach the verifier", posixOnly, () => {
+  fixture("//@ backend dafny\n" + utf16 + lengthSource, true, f => {
+    const generated = f.cli(["gen"]);
+    assert.equal(generated.status, 0, generated.output);
+    writeFileSync(f.proof, readFileSync(f.proof, "utf8")
+      + '\nlemma CorrectLength() ensures codeUnitLength("😀") == 2 {}\n');
+    const result = f.cli(["check"]);
+    assert.equal(result.status, 0, result.output);
+    assert.equal(existsSync(f.marker), true);
+  });
+});
+
+test("numeric-returning surrogate operations verify through the frontend in UTF-16 mode", () => {
+  const source = "//@ backend dafny\n" + utf16 + `export function surrogateCode(): number {
+  //@ verify
+  //@ ensures \\result === 0xD800
+  return String.fromCharCode(0xD800).charCodeAt(0);
+}
+`;
+  assert.equal(String.fromCharCode(0xD800).charCodeAt(0), 0xD800);
+  fixture(source, false, f => {
+    const result = f.cli(["check"]);
+    assert.equal(result.status, 0, result.output);
+    assert.match(result.output, /0 errors/);
+    assert.ok(readFileSync(f.gen, "utf8").includes(header));
+  });
+});
diff --git a/tools/tests/file-options.test.ts b/tools/tests/file-options.test.ts
new file mode 100644
index 00000000..55880336
--- /dev/null
+++ b/tools/tests/file-options.test.ts
@@ -0,0 +1,162 @@
+import { test } from "node:test";
+import assert from "node:assert/strict";
+import { spawnSync } from "node:child_process";
+import { existsSync, mkdirSync, mkdtempSync, readFileSync, realpathSync, rmSync, writeFileSync } from "node:fs";
+import { createRequire } from "node:module";
+import { tmpdir } from "node:os";
+import { dirname, join } from "node:path";
+import { fileURLToPath } from "node:url";
+
+const cli = fileURLToPath(new URL("../src/lsc.ts", import.meta.url));
+const loader = createRequire(import.meta.url).resolve("tsx");
+const utf16 = "//@ option string-semantics javascript-utf16\n//@ option dafny-library local\n";
+const scalar = "//@ option string-semantics unicode-scalar\n//@ option dafny-library stdlib\n";
+const library = "export function size(value: string): number { return value.length; }\n";
+const caller = 'import { size } from "./library";\nexport function read(): number { return size("😀"); }\n';
+
+function runCli(files: Record<string, string>, args: string[] = ["gen", "source.ts"]) {
+  const dir = realpathSync(mkdtempSync(join(tmpdir(), "lsc-file-options-")));
+  try {
+    for (const [name, source] of Object.entries(files)) {
+      const target = join(dir, name);
+      mkdirSync(dirname(target), { recursive: true });
+      writeFileSync(target, source);
+    }
+    const result = spawnSync(process.execPath, ["--import", loader, cli, ...args], {
+      cwd: dir, encoding: "utf8", timeout: 30_000,
+    });
+    assert.ifError(result.error);
+    const gen = join(dir, "source.dfy.gen");
+    return { ...result, generated: existsSync(gen) ? readFileSync(gen, "utf8") : null,
+      proofExists: existsSync(join(dir, "source.dfy")) };
+  } finally {
+    rmSync(dir, { recursive: true, force: true });
+  }
+}
+
+test("lsc config reports file-level options without a project config", () => {
+  const result = runCli({ "source.ts": utf16 + library }, ["config", "source.ts"]);
+  assert.equal(result.status, 0, result.stderr);
+  const report = JSON.parse(result.stdout);
+  assert.equal(report.configFile, null);
+  assert.equal(report.options["string-semantics"], "javascript-utf16");
+  assert.equal(report.options["dafny-library"], "local");
+});
+
+test("file directives can select scalar/stdlib over project UTF-16/local", () => {
+  const result = runCli({
+    "lemmascript.json": JSON.stringify({ "string-semantics": "javascript-utf16", "dafny-library": "local" }),
+    "source.ts": scalar + library,
+  }, ["config", "source.ts"]);
+  assert.equal(result.status, 0, result.stderr);
+  const report = JSON.parse(result.stdout);
+  assert.equal(report.options["string-semantics"], "unicode-scalar");
+  assert.equal(report.options["dafny-library"], "stdlib");
+});
+
+test("a local-library directive completes a UTF-16 project setting before validation", () => {
+  const result = runCli({
+    "lemmascript.json": '{"string-semantics":"javascript-utf16"}',
+    "source.ts": "//@ option dafny-library local\n" + library,
+  });
+  assert.equal(result.status, 0, result.stderr);
+  assert.match(result.generated!, /string-semantics=javascript-utf16/);
+});
+
+for (const [name, project, directive] of [
+  ["default stdlib", "{}", "//@ option string-semantics javascript-utf16\n"],
+  ["inherited stdlib", '{"dafny-library":"stdlib"}', "//@ option string-semantics javascript-utf16\n"],
+  ["file stdlib", '{"string-semantics":"javascript-utf16","dafny-library":"local"}', "//@ option dafny-library stdlib\n"],
+]) {
+  test(`UTF-16 rejects ${name} before writing artifacts`, () => {
+    const result = runCli({ "lemmascript.json": project, "source.ts": directive + library });
+    assert.notEqual(result.status, 0);
+    assert.match(result.stderr, /incompatible.*dafny-library.*stdlib/);
+    assert.equal(result.generated, null);
+    assert.equal(result.proofExists, false);
+  });
+}
+
+for (const [name, rootOptions, dependencyOptions] of [
+  ["UTF-16 calling scalar", utf16, ""],
+  ["scalar calling UTF-16", "", utf16],
+]) {
+  test(`rejects ${name} with both source paths and models`, () => {
+    const result = runCli({ "source.ts": rootOptions + caller, "library.ts": dependencyOptions + library });
+    assert.notEqual(result.status, 0);
+    assert.match(result.stderr, /source\.ts: string-semantics=.*differs from .*library\.ts/);
+    assert.match(result.stderr, /unicode-scalar/);
+    assert.match(result.stderr, /javascript-utf16/);
+    assert.equal(result.generated, null);
+    assert.equal(result.proofExists, false);
+  });
+}
+
+test("matching UTF-16 dependencies work without reinterpreting unrelated tsconfig files", () => {
+  const result = runCli({
+    "tsconfig.json": '{"compilerOptions":{"strict":true},"include":["*.ts"]}',
+    "source.ts": utf16 + caller, "library.ts": utf16 + library,
+    "unrelated.ts": library,
+  });
+  assert.equal(result.status, 0, result.stderr);
+  assert.match(result.generated!, /string-semantics=javascript-utf16/);
+});
+
+test("scalar dependencies may choose different collection libraries", () => {
+  const result = runCli({ "source.ts": caller, "library.ts": "//@ option dafny-library local\n" + library });
+  assert.equal(result.status, 0, result.stderr);
+});
+
+test("checks compiler-selected global callees without an import edge", () => {
+  const result = runCli({
+    "tsconfig.json": '{"compilerOptions":{"strict":true},"include":["*.ts"]}',
+    "source.ts": utf16 + 'export function read(): number { return size("😀"); }\n',
+    "library.ts": library.replace("export ", ""),
+  });
+  assert.notEqual(result.status, 0);
+  assert.match(result.stderr, /differs from .*library\.ts/);
+  assert.equal(result.generated, null);
+});
+
+for (const barrel of ["barrel.ts", "barrel.d.ts"]) {
+  test(`checks transitive model mismatches through ${barrel}`, () => {
+    const result = runCli({
+      "source.ts": caller.replace("./library", "./barrel"),
+      [barrel]: 'export { size } from "./library";\n',
+      "library.ts": utf16 + library,
+    });
+    assert.notEqual(result.status, 0);
+    assert.match(result.stderr, /differs from .*library\.ts/);
+    assert.equal(result.generated, null);
+  });
+}
+
+test("cycles terminate when all dependency models match", () => {
+  const result = runCli({
+    "source.ts": caller,
+    "library.ts": 'export { read } from "./source";\n' + library,
+  });
+  assert.equal(result.status, 0, result.stderr);
+});
+
+test("nested project configs are checked instead of inheriting the caller's model", () => {
+  const result = runCli({
+    "source.ts": caller.replace("./library", "./nested/library"),
+    "nested/lemmascript.json": '{"string-semantics":"javascript-utf16","dafny-library":"local"}',
+    "nested/library.ts": library,
+  });
+  assert.notEqual(result.status, 0);
+  assert.match(result.stderr, /differs from .*nested\/library\.ts/);
+  assert.equal(result.generated, null);
+});
+
+test("--config pins the shared project settings for dependencies too", () => {
+  const result = runCli({
+    "source.ts": caller.replace("./library", "./nested/library"),
+    "shared.json": '{"string-semantics":"javascript-utf16","dafny-library":"local"}',
+    "nested/lemmascript.json": '{"string-semantics":"unicode-scalar"}',
+    "nested/library.ts": library,
+  }, ["gen", "--config=shared.json", "source.ts"]);
+  assert.equal(result.status, 0, result.stderr);
+  assert.match(result.generated!, /string-semantics=javascript-utf16/);
+});