diff --git a/CHANGELOG.md b/CHANGELOG.md
index cf21387..b6c7e2d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -8,6 +8,40 @@ together).
 
 ### Added
 
+- **Selecting four options selected one, and said nothing.** `Select` commits
+  through the control's value setter, which is correct and is also a
+  *replacement*. So the obvious spelling — four `Select` steps at one
+  `<select multiple>` — left the last option standing, fired four `change`
+  events at an app expecting one, and reported success.
+
+  Nothing was available to write instead. The grammar had one option per
+  step, and a multi-selection is not a sequence of selections; it is one
+  state the control ends up in.
+
+  ```yaml
+  - Select "Functional testing", "GUI testing" and "End2End testing" from the "Methods" field
+  ```
+
+  Set-a-state, like `Check`: what is named becomes selected, what is not
+  named does not, and the step means the same thing however the environment
+  arrived. One `input`+`change` for the final state, because what the app's
+  handler expects to see is a user finishing a selection rather than three
+  of them.
+
+  **Every item is quoted**, and that is the design rather than decoration.
+  Option text is arbitrary application text: `"Rock, Paper and Scissors"` is
+  one option on somebody's page, and a list split on commas and the word
+  "and" would read it as three — silently, by selecting the wrong set. Only
+  the quotes delimit.
+
+  Names are resolved before anything is selected, so a typo in the third
+  option leaves the control untouched rather than half-applied, and the step
+  then reads the selection back to verify it took. Found while writing that
+  check: a JS exception inside the driver does **not** reach Rust as an
+  error, so the first version of this reported success on an option that
+  does not exist. The outcome is now a value that comes back and is
+  inspected, not an exception nobody catches.
+
 - **A count could be asserted but never used.** `the "css:.row" appears 5
   times` has always worked, and it is the right step when you know the
   answer. When the app decides the answer — a table built from whatever the
diff --git a/crates/flowproof-adapters/src/web.rs b/crates/flowproof-adapters/src/web.rs
index 82a6e92..e9e4d71 100644
--- a/crates/flowproof-adapters/src/web.rs
+++ b/crates/flowproof-adapters/src/web.rs
@@ -2297,6 +2297,118 @@ impl AppDriver for WebAppDriver {
         })
     }
 
+    fn select_options(
+        &mut self,
+        selector: &UiaSelector,
+        values: &[String],
+    ) -> Result<(), DriverError> {
+        let locator = Self::locator(selector)?;
+        let outcome = self.with_element(
+            &locator,
+            &format!("selecting options in [{selector}]"),
+            |element| {
+                element.call_js_fn(
+                    // The whole selection is set in ONE pass and committed
+                    // with ONE input+change pair, because that is what the
+                    // app's own handler expects to see: a user finishing a
+                    // selection, not four of them.
+                    //
+                    // Every name is resolved BEFORE anything is selected,
+                    // so a typo in the third option leaves the control
+                    // untouched rather than half-applied. A step that
+                    // failed partway would be worse than one that failed.
+                    // Returns a STATUS STRING rather than throwing. A JS
+                    // exception does not reach Rust as an `Err` here - the
+                    // single-option path quietly falls back to typing when
+                    // that happens - so an outcome that must be checked has
+                    // to be a value that comes back.
+                    r#"function(wanted) {
+                        if (this.tagName !== 'SELECT') { return 'not_a_select'; }
+                        if (!this.multiple) { return 'not_multiple'; }
+                        const options = Array.from(this.options);
+                        const pick = (w) => options.find(o => o.value === w)
+                            || options.find(o => o.textContent.trim() === w)
+                            || options.find(o => o.textContent.trim().startsWith(w));
+                        const chosen = [];
+                        for (const raw of wanted) {
+                            const w = String(raw).trim();
+                            const match = pick(w);
+                            // Every name is resolved BEFORE anything is
+                            // selected, so a typo in the third option
+                            // leaves the control untouched rather than
+                            // half-applied.
+                            if (!match) { return 'no_option:' + w; }
+                            chosen.push(match);
+                        }
+                        // Set-a-state, like Check: what is named becomes
+                        // selected and what is not named does not, however
+                        // the control arrived.
+                        for (const o of options) {
+                            o.selected = chosen.indexOf(o) !== -1;
+                        }
+                        this.dispatchEvent(new Event('input', { bubbles: true }));
+                        this.dispatchEvent(new Event('change', { bubbles: true }));
+                        // The post-condition, read back from the control
+                        // itself: what IS selected now.
+                        return 'ok:' + Array.from(this.selectedOptions)
+                            .map(o => o.textContent.trim()).join('\u001f');
+                    }"#,
+                    vec![serde_json::json!(values)],
+                    false,
+                )
+            },
+        )?;
+        let status = outcome
+            .value
+            .as_ref()
+            .and_then(|v| v.as_str())
+            .unwrap_or_default()
+            .to_string();
+        let selected = match status.as_str() {
+            "not_a_select" => {
+                return Err(DriverError::Browser(format!(
+                    "[{selector}] is not a <select>, so it has no options to select"
+                )))
+            }
+            "not_multiple" => {
+                return Err(DriverError::Browser(format!(
+                    "[{selector}] does not allow multiple options - select one option instead"
+                )))
+            }
+            s if s.starts_with("no_option:") => {
+                return Err(DriverError::Browser(format!(
+                    "no option matching '{}' in [{selector}] - the selection was left untouched",
+                    &s["no_option:".len()..]
+                )))
+            }
+            s if s.starts_with("ok:") => s["ok:".len()..].to_string(),
+            other => {
+                return Err(DriverError::Browser(format!(
+                    "selecting options in [{selector}] returned no answer ({other:?})"
+                )))
+            }
+        };
+        // Verify the state took, exactly as `Check` does. A control that
+        // accepted the assignment and then re-derived its own selection
+        // (a framework re-render) must fail here rather than pass on the
+        // strength of having been asked.
+        let got: Vec<&str> = if selected.is_empty() {
+            Vec::new()
+        } else {
+            selected.split('\u{1f}').collect()
+        };
+        if got.len() != values.len() {
+            return Err(DriverError::Browser(format!(
+                "selecting in [{selector}] did not take: asked for {} option(s), \
+                 the control now has {} ({})",
+                values.len(),
+                got.len(),
+                got.join(", ")
+            )));
+        }
+        Ok(())
+    }
+
     fn clear_text(&mut self, selector: &UiaSelector) -> Result<(), DriverError> {
         let locator = Self::locator(selector)?;
         // Go through the native value setter so framework-controlled inputs
diff --git a/crates/flowproof-agent/src/recorder.rs b/crates/flowproof-agent/src/recorder.rs
index e82ea1f..387ff07 100644
--- a/crates/flowproof-agent/src/recorder.rs
+++ b/crates/flowproof-agent/src/recorder.rs
@@ -595,6 +595,21 @@ fn step_for(id: usize, intent: &str, app: &str, action: &ResolvedAction) -> Step
                 selector_ref: Some(0),
             }),
         ),
+        ResolvedAction::SelectOptions { target, values } => {
+            let mut params = flowproof_trace::format::TypeTextParams {
+                // `text` keeps the FIRST option so the step still names
+                // something concrete in a reader that shows only text.
+                // `values` is authoritative wherever it is present - see
+                // docs/trace-format.md.
+                text: values.first().cloned().unwrap_or_default(),
+                submit: None,
+                extra: Default::default(),
+            };
+            params
+                .extra
+                .insert("values".into(), serde_json::json!(values));
+            (selectors_for(app, target, None), Action::TypeText(params))
+        }
         ResolvedAction::Capture {
             target,
             name,
@@ -929,6 +944,7 @@ fn action_selector(action: &ResolvedAction) -> Option<UiaSelector> {
     let target = match action {
         ResolvedAction::Press { target, .. }
         | ResolvedAction::TypeText { target, .. }
+        | ResolvedAction::SelectOptions { target, .. }
         | ResolvedAction::Upload { target, .. }
         | ResolvedAction::ContextClick { target, .. }
         | ResolvedAction::DoubleClick { target, .. }
@@ -1940,6 +1956,11 @@ pub fn record_with_reuse<D: AppDriver, C: ModelClient>(
             }
             match &action {
                 ResolvedAction::Press { .. } => driver.invoke(targeted())?,
+                ResolvedAction::SelectOptions { values, .. } => {
+                    // One commit for the whole set. A missing option fails
+                    // the step in the driver, before anything is selected.
+                    driver.select_options(targeted(), values)?;
+                }
                 ResolvedAction::TypeText { text, .. } => {
                     // `${captured.x}` and `${VAR}` both resolve at the moment
                     // of typing; the trace only ever stores the reference
diff --git a/crates/flowproof-agent/src/rules.rs b/crates/flowproof-agent/src/rules.rs
index ec437eb..fb8c9a3 100644
--- a/crates/flowproof-agent/src/rules.rs
+++ b/crates/flowproof-agent/src/rules.rs
@@ -201,6 +201,10 @@ pub enum ResolvedAction {
     /// Read a target's text into a flow-scoped name for later comparison
     /// (`Remember the "Balance" as balance`). The VALUE never enters the
     /// trace - only the name does, exactly like a `${VAR}` secret.
+    /// Drive a `<select multiple>` to EXACTLY these options. Not a sequence
+    /// of single selections: committing one option replaces the selection,
+    /// so a sequence would leave the last one standing and say nothing.
+    SelectOptions { target: Target, values: Vec<String> },
     /// Remember something about the target under `name`, for a later
     /// assertion or a later `Type` to use. `count` picks WHICH reading:
     /// false is the element's text, true is how many elements match.
@@ -518,6 +522,49 @@ fn unresolvable(step: &str, reason: impl Into<String>) -> RulesError {
     }
 }
 
+/// Parse `"A", "B" and "C"` into its items.
+///
+/// Only the QUOTES delimit. Splitting on `,` or ` and ` would break the
+/// moment an option reads "Rock, Paper and Scissors", which is ordinary app
+/// text, and the break would be silent - three options selected where one
+/// was meant. Separators between quoted items are skipped, not parsed.
+fn quoted_list(step: &str, text: &str) -> Result<Vec<String>, RulesError> {
+    let mut items = Vec::new();
+    let mut rest = text.trim();
+    while let Some(after_open) = rest.strip_prefix('"') {
+        let Some((item, tail)) = quoted_label(after_open) else {
+            return Err(unresolvable(step, "an option is missing its closing quote"));
+        };
+        if item.is_empty() {
+            return Err(unresolvable(step, "an option name may not be empty"));
+        }
+        items.push(item.to_string());
+        // Whatever sits between two quoted items is a separator - `,`,
+        // `and`, or both - and none of it is part of an option name.
+        rest = tail
+            .trim_start()
+            .trim_start_matches(',')
+            .trim_start()
+            .trim_start_matches("and")
+            .trim_start();
+    }
+    if !rest.is_empty() {
+        return Err(unresolvable(
+            step,
+            "every option in a list must be quoted, because option text can \
+             itself contain a comma or the word 'and'",
+        ));
+    }
+    if items.len() < 2 {
+        return Err(unresolvable(
+            step,
+            "a quoted list needs at least two options; to select one, write it \
+             unquoted - 'Select Admin from the \"Role\" field'",
+        ));
+    }
+    Ok(items)
+}
+
 fn refused(step: &str, reason: impl Into<String>) -> RulesError {
     RulesError::Refused {
         step: step.to_string(),
@@ -2542,6 +2589,14 @@ mod web {
                     None
                 };
                 if let (Some(target), false) = (target, value.is_empty()) {
+                    // A QUOTED list is the multi form. Quoted because option
+                    // text is arbitrary app text: "Rock, Paper and Scissors"
+                    // is one option on some page, and an unquoted list could
+                    // not tell it from three.
+                    if value.starts_with('"') {
+                        let values = quoted_list(trimmed, value)?;
+                        return Ok(vec![ResolvedAction::SelectOptions { target, values }]);
+                    }
                     return Ok(vec![ResolvedAction::TypeText {
                         target,
                         text: value.to_string(),
@@ -3843,6 +3898,10 @@ mod tests {
             ("web", "Clear the taskName field"),
             ("web", r#"Select Admin from the "Role" field"#),
             ("web", r#"Select Admin in the "Role" dropdown"#),
+            (
+                "web",
+                r#"Select "Functional testing", "GUI testing" and "End2End testing" from the "Methods" field"#,
+            ),
             ("web", r#"Press the "Save" button"#),
             ("web", "Press the submitButton button"),
             ("web", r#"Click "Templates""#),
@@ -5016,6 +5075,66 @@ mod framed_target_tests {
     /// the model author, which grounds it into some recording; a refused
     /// one stops. Each message must also say what to write instead, or the
     /// refusal is a dead end rather than a redirection.
+    /// The quoting is the whole design, not decoration. Option text is
+    /// arbitrary app text: "Rock, Paper and Scissors" is ONE option on some
+    /// page, and an unquoted list could not tell it from three - silently,
+    /// by selecting the wrong set.
+    #[test]
+    fn a_multi_select_list_is_delimited_by_quotes_and_nothing_else() {
+        let three = plain(
+            r#"Select "Functional testing", "GUI testing" and "End2End testing" from the "Methods" field"#,
+        )
+        .expect("parses");
+        assert_eq!(
+            three,
+            vec![ResolvedAction::SelectOptions {
+                target: Target::Text("Methods".into()),
+                values: vec![
+                    "Functional testing".into(),
+                    "GUI testing".into(),
+                    "End2End testing".into(),
+                ],
+            }]
+        );
+
+        // One quoted option whose TEXT contains both separators stays one
+        // option. This is the case that a split on `,`/` and ` gets wrong.
+        let one = plain(r#"Select "Rock, Paper and Scissors", "Chess" from the "Game" field"#)
+            .expect("parses");
+        assert_eq!(
+            one,
+            vec![ResolvedAction::SelectOptions {
+                target: Target::Text("Game".into()),
+                values: vec!["Rock, Paper and Scissors".into(), "Chess".into()],
+            }]
+        );
+
+        // A comma-separated list is accepted without the trailing `and`.
+        assert!(plain(r#"Select "A", "B" from the "L" field"#).is_ok());
+        // And the single form is untouched: no quotes, one value, TypeText.
+        assert_eq!(
+            plain(r#"Select Admin from the "Role" field"#).expect("parses"),
+            vec![ResolvedAction::TypeText {
+                target: Target::Text("Role".into()),
+                text: "Admin".into(),
+            }]
+        );
+    }
+
+    /// Half-quoted is a mistake worth naming, because the alternative is
+    /// selecting an option called `B" and "C`.
+    #[test]
+    fn a_partly_quoted_list_is_a_parse_error_that_says_why() {
+        let err = plain(r#"Select "A", B and "C" from the "L" field"#)
+            .expect_err("a bare item in a quoted list must be refused");
+        let message = err.to_string();
+        assert!(message.contains("must be quoted"), "{message}");
+        // A one-item quoted list points at the unquoted single form rather
+        // than silently meaning the same thing.
+        let err = plain(r#"Select "A" from the "L" field"#).expect_err("one item is not a list");
+        assert!(err.to_string().contains("at least two options"), "{err}");
+    }
+
     #[test]
     fn declined_shapes_are_refused_and_name_the_alternative() {
         let cases: &[(&str, &str, &str)] = &[
diff --git a/crates/flowproof-driver/src/app.rs b/crates/flowproof-driver/src/app.rs
index 38a1470..86ab224 100644
--- a/crates/flowproof-driver/src/app.rs
+++ b/crates/flowproof-driver/src/app.rs
@@ -521,6 +521,28 @@ pub trait AppDriver {
         ))
     }
 
+    /// Drive a multi-selection control to EXACTLY `values` — the ones named
+    /// become selected and every other one does not, in a single commit.
+    ///
+    /// Not a loop over the single-option path, and it cannot be: committing
+    /// one option goes through the control's value setter, which REPLACES
+    /// the selection. Four sequential single selects therefore leave one
+    /// option chosen and no error anywhere — the silent-partial-success
+    /// shape. Setting the whole set at once is the only honest spelling.
+    ///
+    /// Idempotent, following `Check`: the step means the same thing however
+    /// the environment arrived, so a control that already carries some of
+    /// the selection is not a different case.
+    fn select_options(
+        &mut self,
+        _selector: &UiaSelector,
+        _values: &[String],
+    ) -> Result<(), DriverError> {
+        Err(DriverError::Uia(
+            "selecting several options at once is not supported by this driver".into(),
+        ))
+    }
+
     /// Whether a RESOLVED element is actually rendered — backs the second
     /// half of `the "<target>" is [not] visible`. Resolution alone is not
     /// visibility: a `display:none` input is in the DOM and answers every
@@ -1563,6 +1585,14 @@ impl AppDriver for Box<dyn AppDriver> {
         (**self).element_visible(selector)
     }
 
+    fn select_options(
+        &mut self,
+        selector: &UiaSelector,
+        values: &[String],
+    ) -> Result<(), DriverError> {
+        (**self).select_options(selector, values)
+    }
+
     fn surface_text(&mut self) -> Result<String, DriverError> {
         (**self).surface_text()
     }
diff --git a/crates/flowproof-replay/src/lib.rs b/crates/flowproof-replay/src/lib.rs
index f11f4bd..ee3dfaf 100644
--- a/crates/flowproof-replay/src/lib.rs
+++ b/crates/flowproof-replay/src/lib.rs
@@ -1852,6 +1852,23 @@ fn execute_step<D: AppDriver>(
                 if let Err(reason) = wait_actionable(driver, &target, actionable_timeout(step))? {
                     return Ok((Err(reason), matched));
                 }
+                // A multi-selection is one commit of a whole set, so it is
+                // decided before the single-value path: `values` is
+                // authoritative wherever it is present, and `text` carries
+                // only the first option for a reader that shows text.
+                if let Some(values) = params.extra.get("values").and_then(|v| v.as_array()) {
+                    let wanted: Vec<String> = values
+                        .iter()
+                        .filter_map(|v| v.as_str().map(str::to_string))
+                        .collect();
+                    return Ok((
+                        match driver.select_options(&target, &wanted) {
+                            Ok(()) => Ok(()),
+                            Err(e) => Err(e.to_string()),
+                        },
+                        matched,
+                    ));
+                }
                 // The trace stores references, never values. A
                 // `${captured.x}` resolves from this run's captures and a
                 // `${VAR}` from the environment, both at the moment of
diff --git a/docs/authoring.md b/docs/authoring.md
index 1cfe3bc..5b78366 100644
--- a/docs/authoring.md
+++ b/docs/authoring.md
@@ -51,6 +51,7 @@ before migrating a suite's setup helpers step by step.
 | `Remember how many "<target>" appear as <name>` | the COUNT of matching elements, not their text. Same family and the same indirection as the reading above: taken at execution time on record and on every replay, so a page that grew a row does not need the trace rewritten. Counting rides the ordinal every adapter implements, so it means on each adapter exactly what `the 2nd "Row"` means there. **Zero fails** - a selector typo matches nothing and so does an empty table, and `0` is a confident wrong number to hand to an app; the step that MEANS zero is `assert: the "<target>" appears 0 times`. `appears` is accepted for `appear` |
 | `Check the [2nd ]"<label>" checkbox` / `Uncheck the …` | drives a checkbox, radio, or `role=switch` to a STATE, not a toggle: `Check` on an already-checked box is a no-op, so the step means the same thing however the environment arrives. Resolves the control inside a wrapper too (the common pattern of a visually hidden `input` inside a styled label), performs a real click so the app's own handlers fire, then verifies the state took |
 | `Select <option> from the [2nd ]"<label>" field` | native `<select>`: committed via the value setter, fires `input`+`change` (React-safe). `in the` and `… dropdown` also accepted |
+| `Select "<A>", "<B>" and "<C>" from the [2nd ]"<label>" field` | a `<select multiple>`, driven to EXACTLY the named set in one commit with one `input`+`change` - what the app's own handler expects to see is a user finishing a selection, not three of them. Set-a-state like `Check`, not a toggle: what is named becomes selected and what is not named does not, so the step means the same thing however the environment arrived. **Every item is quoted**, because option text is arbitrary app text - `"Rock, Paper and Scissors"` is one option, and an unquoted list could not tell it from three. Names are resolved before anything is selected, so a typo in the third option leaves the control untouched rather than half-applied, and the step then verifies the selection took. Web only |
 | `Press the [2nd ]"<label>" button` / `Press the <id> button` | |
 | `Right-click [the [2nd ]]"<text>"` | opens the element's context menu; `Right click` also accepted |
 | `Double-click [the [2nd ]]"<text>"` | fires a real `dblclick` on the element; `Double click` also accepted. Web only. Like `Click`, its effect is app-defined, so the step verifies the element resolved and the event dispatched, not app state |
diff --git a/docs/trace-format.md b/docs/trace-format.md
index 46f0409..3d7a3bc 100644
--- a/docs/trace-format.md
+++ b/docs/trace-format.md
@@ -143,6 +143,14 @@ these fields existed) is byte-identical:
   matches nothing and so does an empty table, and the step that means zero
   is an `assert` with `element_count: 0`.
 
+  A `type_text` step may carry `params.values: [...]` — a **multi-selection**,
+  the whole set committed at once. Where `values` is present it is
+  authoritative; `params.text` repeats only the first option, so a reader
+  that shows text still names something concrete. A consumer that honours
+  `text` alone would under-select, which is why `values` is the field to
+  read. A new param key rather than a new action type, so a trace written
+  before multi-selection existed still loads.
+
   `type_text` variants: an **empty `selectors` array** means "type into the
   element that currently has keyboard focus"; `params.replace: true` marks
   fill semantics — the input's current value is cleared before typing (a