diff --git a/bench/utils/sort/Makefile b/bench/utils/sort/Makefile
new file mode 100644
index 00000000..6bf21a50
--- /dev/null
+++ b/bench/utils/sort/Makefile
@@ -0,0 +1,14 @@
+PROJECT_DIR := $(abspath $(dir $(lastword $(MAKEFILE_LIST))))
+REPO_ROOT := $(abspath $(PROJECT_DIR)/../../..)
+LOCAL_TASK := $(notdir $(PROJECT_DIR))
+
+.PHONY: build verify test
+
+build:
+	python3 -m benchmarks.make_tasks build --root "$(REPO_ROOT)" --task "$(LOCAL_TASK)"
+
+verify:
+	python3 -m benchmarks.verify --project "$(PROJECT_DIR)" --library "$(PROJECT_DIR)/../../core"
+
+test:
+	python3 -m benchmarks.make_tasks test --root "$(REPO_ROOT)" --task "$(LOCAL_TASK)"
diff --git a/bench/utils/sort/Sort.dfy b/bench/utils/sort/Sort.dfy
new file mode 100644
index 00000000..a9778d10
--- /dev/null
+++ b/bench/utils/sort/Sort.dfy
@@ -0,0 +1,49 @@
+include "../../core/BenchmarkItem.dfy"
+include "SortSpec.dfy"
+include "SortCore.dfy"
+include "SortProof.dfy"
+
+module Sort {
+  import BenchIO
+  import BenchWorld
+  import BenchItem
+  import CliTypes
+  import S = SortSchema
+  import Core = SortCore
+  import Spec = SortSpec
+  import Proof = SortProof
+
+  class SortBenchmarkItem extends BenchItem.BenchmarkItemTwostate<S.SortCmdRaw> {
+    constructor() {}
+
+    method Name() returns (name: string) {
+      name := "sort";
+    }
+
+    method Schema() returns (schema: CliTypes.CliSchema) {
+      schema := S.Schema();
+    }
+
+    method ParseConfig() returns (cfg: CliTypes.ParseConfig) {
+      cfg := S.ParserConfig();
+    }
+
+    method Decode(parsed: CliTypes.ParsedArgs) returns (raw: S.SortCmdRaw) {
+      raw := S.Decode(parsed);
+    }
+
+    method FormatParseError(err: CliTypes.ParseError) returns (msg: BenchWorld.Bytes) {
+      // TODO: implement and test GNU parse-error behavior, including early exits.
+      assert false;
+      msg := Spec.ParseErrorText(err);
+    }
+
+    method RunCore(raw: S.SortCmdRaw, io: BenchIO.IO) returns (exit: int)
+      modifies io.stdinRegion, io.stdoutRegion, io.stderrRegion
+      ensures Spec.Spec(raw, io, exit)
+    {
+      exit := Core.RunCore(raw, io);
+      Proof.CoreSummaryImpliesSpec(raw, io, exit);
+    }
+  }
+}
diff --git a/bench/utils/sort/SortCli.dfy b/bench/utils/sort/SortCli.dfy
new file mode 100644
index 00000000..5bf2f305
--- /dev/null
+++ b/bench/utils/sort/SortCli.dfy
@@ -0,0 +1,20 @@
+include "Sort.dfy"
+
+module SortCli {
+  import BenchIO
+  import BenchItem
+  import Sort
+
+  method {:main} Main(args: seq<string>)
+    modifies BenchIO.Process().Footprint()
+    decreases *
+  {
+    // Match the repository's .NET entry convention.
+    var effectiveArgs := if |args| > 0 && args[0] == "dotnet" then args[1..] else args;
+    var argv := ["sort"] + effectiveArgs;
+    var io := BenchIO.Process();
+    var item := new Sort.SortBenchmarkItem();
+    var exit := BenchItem.RunMain(item, argv, io);
+    BenchIO.Exit(exit);
+  }
+}
diff --git a/bench/utils/sort/SortCore.dfy b/bench/utils/sort/SortCore.dfy
new file mode 100644
index 00000000..37a25ef3
--- /dev/null
+++ b/bench/utils/sort/SortCore.dfy
@@ -0,0 +1,23 @@
+include "../../core/IO.dfy"
+include "SortSchema.dfy"
+
+module SortCore {
+  import BenchIO
+  import Schema = SortSchema
+
+  twostate predicate CoreSummary(raw: Schema.SortCmdRaw, io: BenchIO.IO, exit: int)
+    reads io.stdinRegion, io.stdoutRegion, io.stderrRegion
+  {
+    // TODO: state what the implementation establishes.
+    false
+  }
+
+  method RunCore(raw: Schema.SortCmdRaw, io: BenchIO.IO) returns (exit: int)
+    modifies io.stdinRegion, io.stdoutRegion, io.stderrRegion
+    ensures CoreSummary(raw, io, exit)
+  {
+    // TODO: implement the agreed behavior and prove CoreSummary.
+    assert false;
+    exit := 1;
+  }
+}
diff --git a/bench/utils/sort/SortProof.dfy b/bench/utils/sort/SortProof.dfy
new file mode 100644
index 00000000..6b47268f
--- /dev/null
+++ b/bench/utils/sort/SortProof.dfy
@@ -0,0 +1,17 @@
+include "SortSpec.dfy"
+include "SortCore.dfy"
+
+module SortProof {
+  import BenchIO
+  import Schema = SortSchema
+  import Core = SortCore
+  import Spec = SortSpec
+
+  twostate lemma CoreSummaryImpliesSpec(
+    raw: Schema.SortCmdRaw, io: BenchIO.IO, exit: int)
+    requires Core.CoreSummary(raw, io, exit)
+    ensures Spec.Spec(raw, io, exit)
+  {
+    // TODO: prove this connection after replacing the false placeholder relations.
+  }
+}
diff --git a/bench/utils/sort/SortSchema.dfy b/bench/utils/sort/SortSchema.dfy
new file mode 100644
index 00000000..6ecd6109
--- /dev/null
+++ b/bench/utils/sort/SortSchema.dfy
@@ -0,0 +1,27 @@
+include "../../core/CliTypes.dfy"
+
+module SortSchema {
+  import CliTypes
+
+  // TODO: replace this wrapper with the utility's decoded command fields.
+  datatype SortCmdRaw = SortCmdRaw(parsed: CliTypes.ParsedArgs)
+
+  method Schema() returns (schema: CliTypes.CliSchema)
+  {
+    // TODO: declare the accepted options and their argument requirements.
+    assert false;
+    schema := CliTypes.CliSchema([], true);
+  }
+
+  method ParserConfig() returns (cfg: CliTypes.ParseConfig)
+  {
+    // TODO: choose the parsing rules from the pinned GNU source.
+    assert false;
+    cfg := CliTypes.ParseConfig(CliTypes.GNU_Permute, true, true, true);
+  }
+
+  method Decode(parsed: CliTypes.ParsedArgs) returns (raw: SortCmdRaw)
+  {
+    raw := SortCmdRaw(parsed);
+  }
+}
diff --git a/bench/utils/sort/SortSpec.dfy b/bench/utils/sort/SortSpec.dfy
new file mode 100644
index 00000000..14025ce2
--- /dev/null
+++ b/bench/utils/sort/SortSpec.dfy
@@ -0,0 +1,23 @@
+include "SortSchema.dfy"
+include "../../core/IO.dfy"
+
+module SortSpec {
+  import BenchIO
+  import BenchWorld
+  import CliTypes
+  import Schema = SortSchema
+
+  function ParseErrorText(err: CliTypes.ParseError): BenchWorld.Bytes
+  {
+    // TODO: define the exact GNU diagnostic bytes here, including fixed text.
+    []
+  }
+
+  // TODO: define the declarative observable specification.
+  // These stream frames are a starting point; use the utility's exact IO regions.
+  twostate predicate Spec(raw: Schema.SortCmdRaw, io: BenchIO.IO, exit: int)
+    reads io.stdinRegion, io.stdoutRegion, io.stderrRegion
+  {
+    false
+  }
+}
diff --git a/bench/utils/sort/Tests.dfy b/bench/utils/sort/Tests.dfy
new file mode 100644
index 00000000..c27d412a
--- /dev/null
+++ b/bench/utils/sort/Tests.dfy
@@ -0,0 +1,8 @@
+include "SortCore.dfy"
+
+module SortTests {
+  // Replace this placeholder with an observable Core behavior case.
+  method {:test} TestCoreBehavior() {
+    expect false, "TODO: add a representative sort Dafny case";
+  }
+}
diff --git a/bench/utils/sort/Tests.py b/bench/utils/sort/Tests.py
new file mode 100644
index 00000000..4e68f617
--- /dev/null
+++ b/bench/utils/sort/Tests.py
@@ -0,0 +1,60 @@
+"""GNU parity cases for sort."""
+
+from pathlib import Path
+
+import pytest
+
+from tools.bench.bench_test_support import (
+    assert_result_matches_reference,
+    bench_dll_path,
+    build_bench_utility,
+    build_coreutils_utility,
+    coreutils_binary_path,
+    evaluation_target_root,
+    run_bench_utility,
+    run_coreutils_utility,
+    run_dafny_verify,
+)
+
+ROOT = evaluation_target_root(Path(__file__).resolve().parents[3])
+UTILITY = "sort"
+PROJECT = ROOT / "bench" / "utils" / UTILITY
+
+
+@pytest.fixture(scope="session")
+def executables() -> tuple[Path, Path]:
+    """Build the two targets only for runtime cases; local Make targets use -n0."""
+    build_bench_utility(ROOT, UTILITY)
+    build_coreutils_utility(ROOT, UTILITY)
+    return (
+        coreutils_binary_path(ROOT, ROOT / "_build/coreutils/src" / UTILITY),
+        bench_dll_path(ROOT, ROOT / "_build/bench" / f"{UTILITY}_bench.dll"),
+    )
+
+
+def assert_parity(
+    executables: tuple[Path, Path],
+    args: list[str],
+    cwd: Path,
+    *,
+    input_data: bytes = b"",
+) -> None:
+    """Compare a read-only scenario, including stderr on error exits."""
+    reference, candidate = executables
+    expected = run_coreutils_utility(reference, UTILITY, args, cwd, input_data=input_data)
+    actual = run_bench_utility(candidate, args, cwd, input_data=input_data)
+    assert_result_matches_reference(expected, actual, ignore_stderr_when_exit_nonzero=False)
+
+
+# Replace this failure with one agreed GNU scenario using executables and assert_parity.
+def test_gnu_parity() -> None:
+    # TODO: add the upstream source path inside the completed test body.
+    pytest.fail("TODO: add a representative sort GNU parity case")
+
+
+# Check each proof module as well as the entry contract required by make check.
+@pytest.mark.dafny_verify
+@pytest.mark.parametrize("filename", ["SortCore.dfy", "SortProof.dfy", "Sort.dfy"])
+def test_verify_module(filename: str) -> None:
+    # upstream: none - Checks the Dafny proof surface, not GNU runtime behavior.
+    run_dafny_verify(PROJECT / filename)
diff --git a/bench/utils/sort/benchmark.yaml b/bench/utils/sort/benchmark.yaml
new file mode 100644
index 00000000..cbd789b4
--- /dev/null
+++ b/bench/utils/sort/benchmark.yaml
@@ -0,0 +1,8 @@
+schema_version: benchmark.definition.v2
+task_id: sort
+kind: coreutils
+source:
+  status: verified
+  name: GNU coreutils sort
+  url: https://www.gnu.org/software/coreutils/
+  license: GPL-3.0-or-later
diff --git a/bench/utils/sort/dfyconfig.toml b/bench/utils/sort/dfyconfig.toml
new file mode 100644
index 00000000..3701c5cc
--- /dev/null
+++ b/bench/utils/sort/dfyconfig.toml
@@ -0,0 +1,6 @@
+includes = ["SortCli.dfy"]
+
+[options]
+target = "cs"
+no-verify = true
+standard-libraries = false
diff --git a/bench/utils/sort/sort.md b/bench/utils/sort/sort.md
new file mode 100644
index 00000000..43af2e87
--- /dev/null
+++ b/bench/utils/sort/sort.md
@@ -0,0 +1,87 @@
+# sort
+
+## Scope for maintainer review
+
+- Reference: GNU coreutils `src/sort.c` at `2cf491412c199e2211880ec3f4ba387026638a33`;
+  `doc/coreutils.texi`, `@node sort invocation`. License: GPL-3.0-or-later.
+- Model/API revision: `bench/core` at `a98d11a`.
+- AllowedInput:
+  - `-r`, `-u`, `-s`, `-c`, `-C`, `-z`, their long spellings (`--reverse`,
+    `--unique`, `--stable`, `--zero-terminated`,
+    `--check[=diagnose-first|quiet|silent]`), grouped short options and `--`.
+  - `--help` and `--version`.
+  - Zero or more file operands; no operand or `-` reads standard input.
+  - Records are arbitrary bytes ended by newline, or NUL with `-z`. A final
+    record without a delimiter is output with one.
+  - Check mode (`-c`, `-C`) takes exactly one regular file operand.
+- EnvironmentProfile: Linux, C locale, `TZ=UTC0`, fixed non-root user; regular
+  files, directories, missing and unreadable paths in the test tree. Standard
+  output write failures are out of scope.
+- Observation: stdout and stderr bytes, exit status (0 success, 1 disorder in
+  check mode, 2 failure) and standard input consumption.
+- TrustedOperations: `bench/core/IO.dfy` read, write, errno-text and quoting
+  operations. Record splitting, ordering, duplicate removal, disorder
+  detection, diagnostics and exit status are implemented and proved.
+
+### Options left out due to IO.dfy
+
+| Option | Missing API support |
+| --- | --- |
+| `-c` / `-C` on standard input | GNU stops reading at the first disorder; `IO.dfy` reads standard input only as a whole. |
+
+Other GNU options, such as keys, other orderings, `-m` and `-o`, are outside
+this scope.
+
+### Errors
+
+- A file operand that is a directory fails with `read failed`; any other
+  unreadable operand fails with `cannot read` (`open failed` in check mode).
+- `cannot read` is checked for every operand before any input is read, so it
+  takes precedence over `read failed`. Standard input is read only if no
+  operand fails with `cannot read` and `-` comes before the first operand that
+  fails with `read failed`.
+- A failed read produces no stdout.
+
+### Examples
+
+Files: `unsorted` = `b\na\nc\na\n`, `sorted` = `a\nb\nc\n`,
+`dupsorted` = `a\na\nb\n`, `nonl` = `b\na`, `zrecs` = `b\0a\0c`; `dir` is a
+directory and `nofile` does not exist.
+
+| Command | stdout | stderr | exit |
+| --- | --- | --- | --- |
+| `sort unsorted` | `a\na\nb\nc\n` | | 0 |
+| `sort nonl` | `a\nb\n` | | 0 |
+| `sort -r unsorted` | `c\nb\na\na\n` | | 0 |
+| `sort -u unsorted` | `a\nb\nc\n` | | 0 |
+| `sort -z zrecs` | `a\0b\0c\0` | | 0 |
+| `sort dir nofile` | | `sort: cannot read: nofile: No such file or directory` | 2 |
+| `sort dir` | | `sort: read failed: dir: Is a directory` | 2 |
+| `sort -c unsorted` | | `sort: unsorted:2: disorder: a` | 1 |
+| `sort -c -u dupsorted` | | `sort: dupsorted:2: disorder: a` | 1 |
+| `sort -c -z zrecs` | | `sort: zrecs:2: disorder: a\0` | 1 |
+| `sort -C unsorted` | | | 1 |
+| `sort -c nofile` | | `sort: open failed: nofile: No such file or directory` | 2 |
+| `sort -c sorted unsorted` | | `sort: extra operand 'unsorted' not allowed with -c` | 2 |
+| `sort -c -C sorted` | | `sort: options '-cC' are incompatible` | 2 |
+
+## Specification and proof
+
+- SpecificationEntry: `SortSpec.Spec`. The output records are a permutation of
+  the input records, ordered by bytes (reversed by `-r`). With `-u`, they are
+  the set of input records in strict order. `-s` has no observable effect,
+  because equal records are identical.
+- Check mode: the input is sorted if every adjacent pair is ordered (strictly
+  with `-u`); otherwise `-c` reports the first out-of-order record and `-C`
+  prints nothing.
+- Frame: standard input, stdout and stderr only.
+- TerminationPolicy: finite input; `RunCore` terminates.
+- CLI boundary: invalid options, incompatible options and extra operands exit
+  early; `RunCore` directly ensures `Spec(...)`.
+- Normal, boundary, and error behavior: rejected outputs include `a\nb\nc\n`
+  for `sort unsorted`, `a\nb` for `sort nonl`, and any stdout for
+  `sort sorted nofile`.
+
+## Contribution and review evidence
+
+Recorded in the pull request.