diff --git a/README.md b/README.md
index e0b0ad4a11..8eca369851 100644
--- a/README.md
+++ b/README.md
@@ -76,6 +76,28 @@ See [Verification Modes](docs/VerificationModes.md) for details on
 the `--check-mode` flag and the deductive and bug-finding verification
 modes.
 
+## Split-Solve-Reconcile (cloud-based SMT solving)
+
+For large programs, SMT solving dominates wall-clock time. The
+split-solve-reconcile workflow lets you run all solver queries in parallel
+(e.g. in the cloud) while keeping Strata's pipeline local:
+
+```bash
+# 1. Generate VCs and a manifest describing them.
+lake exe strata verify Examples/SimpleProc.core.st --no-solve --vc-directory ./vcs/
+
+# 2. Solve each .smt2 file (locally, in parallel, or in the cloud).
+for f in ./vcs/*.smt2; do
+  cvc5 --produce-models "$f" > "${f%.smt2}.result" 2>&1
+done
+
+# 3. Reconcile solver results with the manifest to produce the final report.
+lake exe strata reconcile --vc-directory ./vcs/
+```
+
+See [Cloud Solving](docs/CloudSolving.md) for the manifest format and
+more detail.
+
 ## Troubleshooter
 
 ### When running unit tests: "error: no such file or directory (error code: 2)"
diff --git a/Scripts/ssr_py.sh b/Scripts/ssr_py.sh
new file mode 100755
index 0000000000..26566c224d
--- /dev/null
+++ b/Scripts/ssr_py.sh
@@ -0,0 +1,261 @@
+#!/usr/bin/env bash
+# ------------------------------------------------------------------------------
+# ssr_py.sh — Split-Solve-Aggregate Results workflow for Python analysis.
+#
+# Runs the three phases of cloud-compatible SMT solving for a Python file:
+#
+#   1. Generate — convert .py to Strata Ion, run `strata pyAnalyzeLaurel
+#      --no-solve` to produce .smt2 files.
+#   2. Solve    — run an SMT solver on every .smt2 file (in parallel).
+#   3. Aggregate Results — run `strata aggregate-results` against the .smt2 +
+#      .result files and produce the final report.
+#
+# By default, everything runs locally (the Solve phase fans out over
+# `xargs -P`). To wire in a real cloud solver, override the SOLVER_CMD
+# environment variable or edit the `solve_phase` function.
+#
+# Prerequisites:
+#   - strata executable available (default: ./.lake/build/bin/strata)
+#   - Python 3.13+ with the strata package installed
+#     (`cd Tools/Python && pip install .`)
+#   - An SMT solver on PATH (cvc5 by default; Z3 works too)
+#   - The Python dialect file at ./dialects/Python.dialect.st.ion
+#     (regenerate with `python -m strata.gen dialect dialects`)
+#
+# Usage:
+#   ./ssr_py.sh [options] <input.py>
+#
+# Options:
+#   -o, --output-dir <dir>   Where to place the .smt2, .result files
+#                            (default: ./ssr_out/<basename>)
+#   -s, --solver <cmd>       SMT solver command. Receives the .smt2 path as
+#                            the first arg; its stdout becomes the .result.
+#                            (default: "cvc5 --produce-models")
+#   -j, --jobs <N>           Number of parallel solver processes (default: 4)
+#   -c, --check-mode <mode>  Strata check mode: deductive, bugFinding,
+#                            bugFindingAssumingCompleteSpec (default: deductive)
+#   -l, --check-level <lev>  Strata check level: minimal, minimalVerbose, full
+#                            (default: minimal)
+#      --spec-dir <dir>      Directory with compiled PySpec Ion files
+#                            (default: ".")
+#      --sarif               Also emit aggregate-results.sarif in <output-dir>
+#      --strict              Fail if any .result file is missing
+#      --keep                Keep intermediate files even on failure
+#      --skip-generate       Skip phase 1 (reuse existing <output-dir>)
+#      --skip-solve          Skip phase 2 (reuse existing .result files)
+#      --skip-reconcile      Skip phase 3 (only generate + solve)
+#      --strata <path>       Path to the strata binary
+#                            (default: ./.lake/build/bin/strata)
+#      --dialect <path>      Path to Python dialect Ion file
+#                            (default: ./dialects/Python.dialect.st.ion)
+#      --dispatch <module>   Dispatch module name (may be repeated)
+#      --pyspec <module>     PySpec module name (may be repeated)
+#   -h, --help               Show this help
+#
+# Exit codes:
+#   0  — all goals passed
+#   1  — user error (missing prerequisites, bad args)
+#   2  — failures found during aggregate results
+#   3  — internal error (generate/solve/aggregate crashed)
+# ------------------------------------------------------------------------------
+
+set -u  # Treat unset variables as errors. We handle non-zero ourselves.
+
+# -------- defaults --------
+OUTPUT_DIR=""
+SOLVER_CMD="${SOLVER_CMD:-cvc5 --produce-models}"
+JOBS=4
+CHECK_MODE="deductive"
+CHECK_LEVEL="minimal"
+SPEC_DIR="."
+EMIT_SARIF=0
+STRICT=0
+KEEP=0
+SKIP_GENERATE=0
+SKIP_SOLVE=0
+SKIP_AGGREGATE=0
+STRATA_BIN="./.lake/build/bin/strata"
+DIALECT_FILE="./dialects/Python.dialect.st.ion"
+DISPATCH_MODULES=()
+PYSPEC_MODULES=()
+INPUT_PY=""
+
+# -------- helpers --------
+err()   { printf '\033[1;31merror:\033[0m %s\n' "$*" >&2; }
+warn()  { printf '\033[1;33mwarn:\033[0m %s\n'  "$*" >&2; }
+info()  { printf '\033[1;34m==>\033[0m %s\n'   "$*" >&2; }
+step()  { printf '\033[1;32m-->\033[0m %s\n'   "$*" >&2; }
+
+usage() {
+  sed -n '3,62p' "$0" | sed 's/^# \{0,1\}//'
+}
+
+die_user() {
+  err "$*"
+  exit 1
+}
+
+die_internal() {
+  err "$*"
+  exit 3
+}
+
+require_cmd() {
+  command -v "$1" >/dev/null 2>&1 || die_user "'$1' not found on PATH"
+}
+
+# -------- arg parsing --------
+while [ $# -gt 0 ]; do
+  case "$1" in
+    -o|--output-dir)   OUTPUT_DIR="$2"; shift 2 ;;
+    -s|--solver)       SOLVER_CMD="$2"; shift 2 ;;
+    -j|--jobs)         JOBS="$2"; shift 2 ;;
+    -c|--check-mode)   CHECK_MODE="$2"; shift 2 ;;
+    -l|--check-level)  CHECK_LEVEL="$2"; shift 2 ;;
+    --spec-dir)        SPEC_DIR="$2"; shift 2 ;;
+    --sarif)           EMIT_SARIF=1; shift ;;
+    --strict)          STRICT=1; shift ;;
+    --keep)            KEEP=1; shift ;;
+    --skip-generate)   SKIP_GENERATE=1; shift ;;
+    --skip-solve)      SKIP_SOLVE=1; shift ;;
+    --skip-reconcile)  SKIP_AGGREGATE=1; shift ;;
+    --strata)          STRATA_BIN="$2"; shift 2 ;;
+    --dialect)         DIALECT_FILE="$2"; shift 2 ;;
+    --dispatch)        DISPATCH_MODULES+=("$2"); shift 2 ;;
+    --pyspec)          PYSPEC_MODULES+=("$2"); shift 2 ;;
+    -h|--help)         usage; exit 0 ;;
+    --)                shift; INPUT_PY="${1:-}"; break ;;
+    -*)                die_user "unknown option: $1" ;;
+    *)                 INPUT_PY="$1"; shift ;;
+  esac
+done
+
+# -------- validate args --------
+[ -z "$INPUT_PY" ] && { usage; exit 1; }
+[ -f "$INPUT_PY" ] || die_user "input file '$INPUT_PY' does not exist"
+
+case "$INPUT_PY" in
+  *.py|*.python.st.ion) ;;
+  *) warn "input file '$INPUT_PY' is not a .py or .python.st.ion file; proceeding anyway" ;;
+esac
+
+# Derive output directory if not provided.
+if [ -z "$OUTPUT_DIR" ]; then
+  base="$(basename "$INPUT_PY")"
+  base="${base%.py}"
+  base="${base%.python.st.ion}"
+  OUTPUT_DIR="./ssr_out/${base}"
+fi
+
+[ -x "$STRATA_BIN" ] || die_user "strata binary not found at '$STRATA_BIN'. Run 'lake build strata:exe' first, or pass --strata <path>."
+
+mkdir -p "$OUTPUT_DIR"
+
+# -------- phase 1: generate --------
+# Compiles the Python source to an Ion file (if needed) and runs
+# `strata pyAnalyzeLaurel --no-solve` to emit *.smt2 files.
+
+ION_FILE="$OUTPUT_DIR/input.python.st.ion"
+
+generate_phase() {
+  step "Phase 1: generate"
+
+  # If the input is already an Ion file, just symlink it into place.
+  if [ "${INPUT_PY##*.}" = "ion" ] || [ "${INPUT_PY: -14}" = ".python.st.ion" ]; then
+    info "Input is already a Python Ion file; copying into place"
+    cp -f "$INPUT_PY" "$ION_FILE"
+  else
+    [ -f "$DIALECT_FILE" ] || die_user "dialect file '$DIALECT_FILE' not found. Regenerate with 'python -m strata.gen dialect dialects'."
+    require_cmd python3
+    info "Converting $INPUT_PY -> $ION_FILE"
+    if ! python3 -m strata.gen py_to_strata --dialect "$DIALECT_FILE" "$INPUT_PY" "$ION_FILE"; then
+      die_internal "py_to_strata failed on '$INPUT_PY'. Is the strata Python package installed? Try 'cd Tools/Python && pip install .'"
+    fi
+  fi
+
+  info "Running strata pyAnalyzeLaurel --no-solve"
+  local py_args=(
+    pyAnalyzeLaurel "$ION_FILE"
+    --no-solve
+    --vc-directory "$OUTPUT_DIR"
+    --spec-dir "$SPEC_DIR"
+    --check-mode "$CHECK_MODE"
+    --check-level "$CHECK_LEVEL"
+  )
+  for m in "${DISPATCH_MODULES[@]}"; do py_args+=( --dispatch "$m" ); done
+  for m in "${PYSPEC_MODULES[@]}";  do py_args+=( --pyspec "$m" );  done
+
+  if ! "$STRATA_BIN" "${py_args[@]}" > "$OUTPUT_DIR/generate.log" 2>&1; then
+    err "strata pyAnalyzeLaurel --no-solve failed (see $OUTPUT_DIR/generate.log)"
+    tail -n 30 "$OUTPUT_DIR/generate.log" >&2 || true
+    exit 3
+  fi
+  info "Generate phase complete. Log: $OUTPUT_DIR/generate.log"
+}
+
+# -------- phase 2: solve --------
+# Runs the SMT solver on every .smt2 file, in parallel, capturing stdout
+# (and stderr) into matching .result files.
+
+solve_one() {
+  local smt="$1"
+  local base="${smt%.smt2}"
+  local result="${base}.result"
+  # shellcheck disable=SC2086  # we *want* word splitting on $SOLVER_CMD
+  $SOLVER_CMD "$smt" > "$result" 2>&1
+}
+export -f solve_one
+
+solve_phase() {
+  step "Phase 2: solve"
+  local solver_bin="${SOLVER_CMD%% *}"
+  require_cmd "$solver_bin"
+
+  local smt2_count
+  smt2_count=$(find "$OUTPUT_DIR" -maxdepth 1 -name '*.smt2' -type f | wc -l)
+  if [ "$smt2_count" -eq 0 ]; then
+    info "No .smt2 files to solve (all obligations resolved by evaluator)."
+    return
+  fi
+  info "Solving $smt2_count .smt2 files with $JOBS parallel workers"
+  info "Solver: $SOLVER_CMD"
+
+  export SOLVER_CMD
+  # Use xargs for portable parallelism. `-P $JOBS` runs up to $JOBS in
+  # parallel; `-I {}` implies one argument per invocation.
+  find "$OUTPUT_DIR" -maxdepth 1 -name '*.smt2' -type f -print0 \
+    | xargs -0 -P "$JOBS" -I {} bash -c 'solve_one "$@"' _ {}
+  info "Solve phase complete."
+}
+
+# -------- phase 3: aggregate results --------
+# Runs `strata aggregate-results` to classify results and produce the final report.
+
+aggregate_phase() {
+  step "Phase 3: aggregate results"
+  local rec_args=(
+    aggregate-results
+    --vc-directory "$OUTPUT_DIR"
+    --check-mode "$CHECK_MODE"
+    --check-level "$CHECK_LEVEL"
+  )
+  [ "$EMIT_SARIF" -eq 1 ] && rec_args+=( --sarif )
+  [ "$STRICT"     -eq 1 ] && rec_args+=( --strict )
+
+  "$STRATA_BIN" "${rec_args[@]}" | tee "$OUTPUT_DIR/aggregate-results.log"
+  local rc="${PIPESTATUS[0]}"
+  info "Aggregate results phase complete. Log: $OUTPUT_DIR/aggregate-results.log"
+  return "$rc"
+}
+
+# -------- drive the workflow --------
+[ "$SKIP_GENERATE"  -eq 0 ] && generate_phase
+[ "$SKIP_SOLVE"     -eq 0 ] && solve_phase
+if [ "$SKIP_AGGREGATE" -eq 0 ]; then
+  aggregate_phase
+  rc=$?
+  if [ "$KEEP" -eq 0 ] && [ "$rc" -eq 0 ]; then
+    info "Success. Artifacts kept in $OUTPUT_DIR (pass --keep or rerun with --skip-* to reuse)."
+  fi
+  exit "$rc"
+fi
diff --git a/Strata.lean b/Strata.lean
index b64f7abbd0..ee3cb45553 100644
--- a/Strata.lean
+++ b/Strata.lean
@@ -25,6 +25,7 @@ import Strata.Languages.Core.FactoryWF
 import Strata.Languages.Core.SeqModel
 import Strata.Languages.Core.StatementSemantics
 import Strata.Languages.Core.SarifOutput
+import Strata.Languages.Core.AggregateResults
 import Strata.Languages.Laurel.LaurelCompilationPipeline
 
 /- Code Transforms -/
diff --git a/Strata/Languages/Core/AggregateResults.lean b/Strata/Languages/Core/AggregateResults.lean
new file mode 100644
index 0000000000..5053b8d006
--- /dev/null
+++ b/Strata/Languages/Core/AggregateResults.lean
@@ -0,0 +1,185 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import Strata.Languages.Core.Verifier
+
+/-!
+# Aggregate Results Phase for Split-Solve-Aggregate Results
+
+This module implements the **Aggregate Results** phase of the
+Split-Solve-Aggregate Results workflow. It reads `.smt2` files (produced by
+`strata verify --no-solve`) and their corresponding `.result` files from an
+SMT solver, and produces `VCResults` identical to what a full `strata verify`
+would have returned.
+
+All obligation metadata is embedded directly in the `.smt2` files via
+`set-info` directives, so no separate manifest file is needed.
+-/
+
+namespace Core
+open Imperative
+open Strata
+
+public section
+
+/-! ## String ↔ type conversions for set-info values -/
+
+/-- Parse a property type from its string form (as emitted in `set-info :property`). -/
+def propertyTypeOfString (s : String) : Imperative.PropertyType :=
+  match s with
+  | "cover" => .cover
+  | "assert" => .assert
+  | "divisionByZero" => .divisionByZero
+  | "arithmeticOverflow" => .arithmeticOverflow
+  | _ => .assert
+
+/-- Parse a verdict string into a `Core.SMT.Result` with no model. -/
+def smtResultOfString (s : String) : Core.SMT.Result :=
+  match s with
+  | "sat" => .sat []
+  | "unsat" => .unsat
+  | "unknown" => .unknown
+  | _ => .err s!"unrecognized verdict: {s}"
+
+/-! ## Result file parsing -/
+
+/-- Classify a raw solver output line as a verdict. -/
+private def lineVerdict? (line : String) : Option Core.SMT.Result :=
+  match line.trimAscii.toString with
+  | "sat" => some (.sat [])
+  | "unsat" => some .unsat
+  | "unknown" => some .unknown
+  | _ => none
+
+/-- Parse a `.result` file's contents into `(satResult, valResult)`. -/
+def parseResultFile (content : String)
+    (satisfiabilityCheck validityCheck : Bool) :
+    Core.SMT.Result × Core.SMT.Result :=
+  let lines := content.splitOn "\n"
+  let verdicts := lines.filterMap lineVerdict?
+  match satisfiabilityCheck, validityCheck with
+  | true, true =>
+    match verdicts with
+    | v1 :: v2 :: _ => (v1, v2)
+    | [v1] => (v1, .err "missing validity verdict")
+    | _ => (.err "missing satisfiability verdict", .err "missing validity verdict")
+  | true, false =>
+    match verdicts with
+    | v1 :: _ => (v1, .unknown)
+    | [] => (.err "missing satisfiability verdict", .unknown)
+  | false, true =>
+    match verdicts with
+    | v1 :: _ => (.unknown, v1)
+    | [] => (.unknown, .err "missing validity verdict")
+  | false, false =>
+    (.unknown, .unknown)
+
+/-! ## SMT2-based result aggregation -/
+
+/-- Metadata extracted from a single `.smt2` file's `set-info` directives. -/
+structure SMT2Meta where
+  smtMetadataVersion : Option String := none
+  file : Option String := none
+  start : Option Nat := none
+  stop : Option Nat := none
+  label : String := "unknown"
+  property : String := "assert"
+  resolvedSat : Option String := none
+  resolvedVal : Option String := none
+  hasSatCheck : Bool := false
+  hasValCheck : Bool := false
+  deriving Repr
+
+private def extractQuoted (line : String) : Option String :=
+  match line.splitOn "\"" with
+  | _ :: val :: _ => some val
+  | _ => none
+
+/-- Parse `set-info` directives from SMT2 file content. -/
+def parseSMT2Meta (content : String) : SMT2Meta :=
+  content.splitOn "\n" |>.foldl (init := ({} : SMT2Meta)) fun info line =>
+    let l := line.trimAscii.toString
+    if l.startsWith "(set-info :strata-smt-metadata-version " then
+      { info with smtMetadataVersion := extractQuoted l }
+    else if l.startsWith "(set-info :file " then
+      { info with file := extractQuoted l }
+    else if l.startsWith "(set-info :start " then
+      { info with start := (l.drop 17 |>.dropEnd 1 |>.trimAscii).toNat? }
+    else if l.startsWith "(set-info :stop " then
+      { info with stop := (l.drop 16 |>.dropEnd 1 |>.trimAscii).toNat? }
+    else if l.startsWith "(set-info :final-message " then
+      { info with label := extractQuoted l |>.getD "unknown" }
+    else if l.startsWith "(set-info :property " then
+      { info with property := extractQuoted l |>.getD "assert" }
+    else if l.startsWith "(set-info :resolved-sat " then
+      { info with resolvedSat := extractQuoted l }
+    else if l.startsWith "(set-info :resolved-val " then
+      { info with resolvedVal := extractQuoted l }
+    else if l.startsWith "(set-info :sat-message " then
+      { info with hasSatCheck := true }
+    else if l.startsWith "(set-info :unsat-message " then
+      { info with hasValCheck := true }
+    else info
+
+/-- Build a `VCResult` from parsed SMT2 metadata and solver output. -/
+def aggregateFromSMT2 (smt2 : SMT2Meta) (solverOutput : Option String)
+    (options : VerifyOptions) : VCResult :=
+  let property := propertyTypeOfString smt2.property
+  let fileRange : Option Strata.FileRange :=
+    match smt2.file, smt2.start, smt2.stop with
+    | some f, some s, some e => some { file := .file f, range := { start := ⟨s⟩, stop := ⟨e⟩ } }
+    | _, _, _ => none
+  let md : Imperative.MetaData Expression :=
+    match fileRange with
+    | some fr => (Imperative.MetaData.empty).pushElem Imperative.MetaData.fileRange (.fileRange fr)
+    | none => Imperative.MetaData.empty
+  let obligation : Imperative.ProofObligation Expression :=
+    { label := smt2.label, property, assumptions := [], obligation := default, metadata := md }
+  let satisfiabilityCheck := smt2.hasSatCheck || smt2.resolvedSat.isSome
+  let validityCheck := smt2.hasValCheck || smt2.resolvedVal.isSome
+  let peSat? := smt2.resolvedSat.map smtResultOfString
+  let peVal? := smt2.resolvedVal.map smtResultOfString
+  let (solverSat, solverVal) := match solverOutput with
+    | some content =>
+      parseResultFile content (satisfiabilityCheck && peSat?.isNone) (validityCheck && peVal?.isNone)
+    | none => (.unknown, .unknown)
+  let satResult := peSat?.getD solverSat
+  let valResult := peVal?.getD solverVal
+  buildVCResult obligation satResult valResult
+    satisfiabilityCheck validityCheck [] options
+
+/-- Aggregate results from all `.smt2` files in a directory. Reads each `.smt2`
+file for obligation metadata and pairs it with the corresponding `.result` file.
+Warns on stderr if any file has an unrecognized schema version. -/
+def aggregateResultsDirectory (vcDir : System.FilePath)
+    (options : VerifyOptions) : IO VCResults := do
+  let entries ← vcDir.readDir
+  let smt2Files := entries.filter (·.fileName.endsWith ".smt2")
+    |>.qsort (fun a b => a.fileName < b.fileName)
+  let mut results : VCResults := #[]
+  for entry in smt2Files do
+    let content ← IO.FS.readFile entry.path
+    let smt2 := parseSMT2Meta content
+    -- Warn if the SMT metadata version is missing or unrecognized.
+    match smt2.smtMetadataVersion with
+    | none =>
+      IO.eprintln s!"warning: {entry.fileName} has no strata-smt-metadata-version; results may be unreliable"
+    | some v =>
+      if v != Strata.SMT.Encoder.smtMetadataVersion then
+        IO.eprintln s!"warning: {entry.fileName} has strata-smt-metadata-version \"{v}\" but this build expects \"{Strata.SMT.Encoder.smtMetadataVersion}\"; results may be unreliable"
+    let resultPath := vcDir / ((entry.fileName.dropEnd 5).toString ++ ".result")
+    let solverOutput ← do
+      if ← resultPath.pathExists then
+        some <$> IO.FS.readFile resultPath
+      else
+        pure none
+    let r := aggregateFromSMT2 smt2 solverOutput options
+    results := results.push r
+  return results.mergeByAssertion
+
+end -- public section
+end Core
diff --git a/Strata/Languages/Core/Verifier.lean b/Strata/Languages/Core/Verifier.lean
index 45bb025509..fc80422355 100644
--- a/Strata/Languages/Core/Verifier.lean
+++ b/Strata/Languages/Core/Verifier.lean
@@ -32,6 +32,12 @@ open Strata
 
 public section
 
+/-- The current schema version for SMT metadata (`set-info` directives).
+    Bump this when the set of directives or their semantics change
+    in a backwards-incompatible way. The aggregate results phase checks this
+    and warns if it encounters a version it does not understand. -/
+def smtMetadataVersion : String := "1"
+
 /-- Encode a verification condition into SMT-LIB format.
 
 This function encodes the path conditions (P) and obligation (Q) into SMT,
@@ -53,10 +59,15 @@ def encodeCore (ctx : Core.SMT.Context) (prelude : SolverM Unit)
     (md : Imperative.MetaData Core.Expression)
     (satisfiabilityCheck validityCheck : Bool)
     (label : String)
+    (property : String := "assert")
+    (resolvedSat : Option String := none)
+    (resolvedVal : Option String := none)
     (varDefinitions : List Core.VarDefinition := [])
     (varDeclarations : List Core.VarDeclaration := []) :
     SolverM (List String × EncoderState) := do
   Solver.setLogic "ALL"
+  -- Emit SMT metadata version so the aggregate results phase can detect incompatible changes.
+  Solver.setInfo "strata-smt-metadata-version" s!"\"{smtMetadataVersion}\""
   prelude
   let _ ← ctx.sorts.mapM (fun s => Solver.declareSort s.name s.arity)
   ctx.emitDatatypes
@@ -133,6 +144,14 @@ def encodeCore (ctx : Core.SMT.Context) (prelude : SolverM Unit)
   let rawMsg := md.getPropertySummary.getD label
   let escaped := rawMsg.replace "\\" "\\\\" |>.replace "\"" "\\\""
   Solver.setInfo "final-message" s!"\"{escaped}\""
+  -- Emit the property type so aggregate results can classify without a manifest.
+  Solver.setInfo "property" s!"\"{property}\""
+  -- Emit evaluator-resolved results (if any) so aggregate results knows which
+  -- checks were already decided before the solver ran.
+  if let some r := resolvedSat then
+    Solver.setInfo "resolved-sat" s!"\"{r}\""
+  if let some r := resolvedVal then
+    Solver.setInfo "resolved-val" s!"\"{r}\""
 
   return (ids, estate)
 
@@ -147,6 +166,28 @@ open Lambda Strata.SMT
 
 public section
 
+/-- Short verdict string for embedding in SMT2 `set-info` directives.  Note:
+This intentionally differs from the `ToFormat` instance on `SMT.Result` which
+includes model details. Solver result aggregation needs bare keywords that can
+be round-tripped via `smtResultOfString`. -/
+def verdictString : Imperative.SMT.Result Core.Expression.Ident → String
+  | .sat _ => "sat"
+  | .unsat => "unsat"
+  | .unknown _ => "unknown"
+  | .err _ => "err"
+
+/-- Property type as a short machine-readable string for `set-info`.  Note: This
+intentionally differs from the `ToFormat PropertyType` instance which produces
+human-readable labels like "division by zero check".  Solver result aggregation
+needs identifiers that can be round-tripped via `propertyTypeOfString` in
+`AggregateResults.lean`. -/
+def propertyString (p : Imperative.PropertyType) : String :=
+  match p with
+  | .cover => "cover"
+  | .assert => "assert"
+  | .divisionByZero => "divisionByZero"
+  | .arithmeticOverflow => "arithmeticOverflow"
+
 /-- Replace characters that are problematic on common filesystems
     (parens, quotes, spaces, path separators, and Windows-invalid characters
     such as `< > : | ? *`) with underscores or remove them.
@@ -158,7 +199,7 @@ def sanitizeFilename (s : String) : String :=
          || c == '<' || c == '>' || c == ':' || c == '|' || c == '?' || c == '*' then some '_'
     else some c
 
-private def typedVarToSMTFn (ctx : SMT.Context) (id : Core.Expression.Ident)
+def typedVarToSMTFn (ctx : SMT.Context) (id : Core.Expression.Ident)
   (ty : Core.Expression.Ty) := do
     -- Type of identifier has to be monotye
     let some mty := LTy.toMonoType? ty | .error s!"not monotype: {id}"
@@ -201,6 +242,9 @@ def dischargeObligation
   (ctx : SMT.Context)
   (satisfiabilityCheck validityCheck : Bool)
   (label : String)
+  (property : String := "assert")
+  (resolvedSat : Option String := none)
+  (resolvedVal : Option String := none)
   (varDefinitions : List VarDefinition := [])
   (varDeclarations : List VarDeclaration := [])
   : IO (Except Format (SMT.Result × SMT.Result × EncoderState)) := do
@@ -216,7 +260,9 @@ def dischargeObligation
     (P := Core.Expression)
     (Strata.SMT.Encoder.encodeCore ctx (getSolverPrelude options.solver)
       assumptionTerms obligationTerm md satisfiabilityCheck validityCheck
-      (label := label) (varDefinitions := varDefinitions) (varDeclarations := varDeclarations))
+      (label := label) (property := property)
+      (resolvedSat := resolvedSat) (resolvedVal := resolvedVal)
+      (varDefinitions := varDefinitions) (varDeclarations := varDeclarations))
     (typedVarToSMTFn ctx)
     vars
     options.solver
@@ -887,7 +933,7 @@ def coreAbstractedPhases (procs : Option (List String) := none)
   (corePipelinePhases procs options moreFns).map (·.phase)
 
 /-- Build the solver log from raw results and phase validation logs. -/
-private def buildSolverLog (satResult valResult : SMT.Result)
+def buildSolverLog (satResult valResult : SMT.Result)
     (satisfiabilityCheck validityCheck : Bool)
     (satPhaseLog valPhaseLog : List SolverPhaseLog) : Array SolverPhaseLog :=
   let sat : Array SolverPhaseLog :=
@@ -908,6 +954,34 @@ def SMT.Result.adjustForPhases (r : SMT.Result)
   | .sat _ | .unknown _ => AbstractedPhase.validateModel phases r obligation
   | other => (other, [])
 
+/-- Build a `VCResult` from raw solver results, applying phase validation,
+solver log construction, and outcome masking. This is the single source of
+truth for turning `(satResult, valResult)` into a classified `VCResult`,
+used by both the integrated verifier (`getObligationResult`) and the
+aggregate results path (`aggregateFromSMT2`). -/
+def buildVCResult
+    (obligation : ProofObligation Expression)
+    (satResult valResult : SMT.Result)
+    (satisfiabilityCheck validityCheck : Bool)
+    (phases : List AbstractedPhase)
+    (options : VerifyOptions)
+    (lexprModel : LExprModel := []) : VCResult :=
+  let (adjSat, satPhaseLog) := satResult.adjustForPhases phases obligation
+  let (adjVal, valPhaseLog) := valResult.adjustForPhases phases obligation
+  let smtLog := buildSolverLog satResult valResult
+    satisfiabilityCheck validityCheck satPhaseLog valPhaseLog
+  let rawOutcome : VCOutcome := {
+    satisfiabilityProperty := adjSat,
+    validityProperty := adjVal,
+    solverLog := #[smtLog] }
+  let outcome := maskOutcome rawOutcome satisfiabilityCheck validityCheck
+  { obligation,
+    outcome := .ok outcome,
+    verbose := options.verbose,
+    checkLevel := options.checkLevel,
+    checkMode := options.checkMode,
+    lexprModel }
+
 /--
 Invoke a backend engine and get the analysis result for a
 given proof obligation.
@@ -918,6 +992,8 @@ def getObligationResult (assumptionTerms : List Term) (obligationTerm : Term)
     (options : VerifyOptions) (counter : IO.Ref Nat)
     (tempDir : System.FilePath) (satisfiabilityCheck validityCheck : Bool)
     (phases : List AbstractedPhase)
+    (peSatResult? : Option Core.SMT.Result := none)
+    (peValResult? : Option Core.SMT.Result := none)
     (varDefinitions : List VarDefinition := [])
     (varDeclarations : List VarDeclaration := [])
     : EIO DiagnosticModel VCResult := do
@@ -944,7 +1020,11 @@ def getObligationResult (assumptionTerms : List Term) (obligationTerm : Term)
             obligation.metadata
             filename.toString
           assumptionTerms obligationTerm ctx satisfiabilityCheck validityCheck
-          (label := obligation.label) (varDefinitions := varDefinitions) (varDeclarations := varDeclarations))
+          (label := obligation.label)
+          (property := SMT.propertyString obligation.property)
+          (resolvedSat := peSatResult?.map SMT.verdictString)
+          (resolvedVal := peValResult?.map SMT.verdictString)
+          (varDefinitions := varDefinitions) (varDeclarations := varDeclarations))
   match ans with
   | .error e =>
     dbg_trace f!"\n\nObligation {obligation.label}: SMT Solver Invocation Error!\
@@ -953,17 +1033,7 @@ def getObligationResult (assumptionTerms : List Term) (obligationTerm : Term)
     .error <| DiagnosticModel.fromFormat e
   | .ok (satResult, validityResult, estate) =>
     -- Convert unvalidated sat results to unknown when phases require validation
-    let (adjSat, satPhaseLog) := satResult.adjustForPhases phases obligation
-    let (adjVal, valPhaseLog) := validityResult.adjustForPhases phases obligation
-    -- Build solver log: raw solver results followed by phase validation logs
-    let smtLog := buildSolverLog satResult validityResult
-      satisfiabilityCheck validityCheck satPhaseLog valPhaseLog
-    let rawOutcome : VCOutcome := {
-      satisfiabilityProperty := adjSat,
-      validityProperty := adjVal,
-      solverLog := #[smtLog] }
-    let outcome := maskOutcome rawOutcome satisfiabilityCheck validityCheck
-    -- Extract model from sat results (using raw solver results)
+    -- and build the classified VCResult.
     let model := match satResult, validityResult with
       | .sat m, _ => convertModel m (SMT.Context.getConstructorNames ctx)
       | _, .sat m => convertModel m (SMT.Context.getConstructorNames ctx)
@@ -971,14 +1041,9 @@ def getObligationResult (assumptionTerms : List Term) (obligationTerm : Term)
     -- Filter out managed variables from model display
     let managedVarNames := (varDefinitions.map (·.name)) ++ (varDeclarations.map (·.name))
     let model := model.filter fun (name, _) => !managedVarNames.contains name.name
-    let result := { obligation,
-                    outcome := .ok outcome,
-                    estate,
-                    verbose := options.verbose,
-                    checkLevel := options.checkLevel,
-                    checkMode := options.checkMode,
-                    lexprModel := model }
-    return result
+    let result := buildVCResult obligation satResult validityResult
+      satisfiabilityCheck validityCheck phases options (lexprModel := model)
+    return { result with estate }
 
 
 def verifySingleEnv (oblProgram : Program)
@@ -1075,6 +1140,7 @@ def verifySingleEnv (oblProgram : Program)
       let t4 ← IO.monoNanosNow
       let result ← getObligationResult assumptionTerms obligationTerm ctx obligation p options
                     counter tempDir needSatCheck needValCheck (externalPhases ++ corePhases)
+                    peSatResult? peValResult?
                     (varDefinitions := varDefs) (varDeclarations := varDecls)
       let t5 ← IO.monoNanosNow
       solverNs := solverNs + (t5 - t4)
diff --git a/StrataMain.lean b/StrataMain.lean
index 77cc6491e9..7c66ab3f83 100644
--- a/StrataMain.lean
+++ b/StrataMain.lean
@@ -12,6 +12,7 @@ import Strata.Backends.CBMC.GOTO.CoreToGOTOPipeline
 import Strata.DDM.Integration.Java.Gen
 import Strata.Languages.Core.Verifier
 import Strata.Languages.Core.SarifOutput
+import Strata.Languages.Core.AggregateResults
 import Strata.Languages.Core.ProgramEval
 import Strata.Languages.Core.StatementEval
 import Strata.Languages.C_Simp.Verify
@@ -1284,7 +1285,7 @@ def verifyCommand : Command where
         else if pgm.dialect == "Boole" then
           Boole.verify opts.solver pgm inputCtx proceduresToVerify opts
         else
-          verify pgm inputCtx proceduresToVerify opts
+          Strata.verify pgm inputCtx proceduresToVerify opts
       catch e =>
         println! f!"{e}"
         IO.Process.exit ExitCode.internalError
@@ -1310,6 +1311,60 @@ def verifyCommand : Command where
         println! f!"Finished with {provedGoalCount} goals passed, {failedGoalCount} failed."
         IO.Process.exit ExitCode.failuresFound
 
+/-- Aggregate results: read `.smt2` files and solver `.result` files from a
+    directory, produce the final verification report. -/
+def aggregateResultsCommand : Command where
+  name := "aggregate-results"
+  args := []
+  flags := [
+    { name := "vc-directory",
+      help := "Directory containing .smt2 and solver .result files (required).",
+      takesArg := .arg "dir" },
+    { name := "check-mode",
+      help := s!"Check mode: {Core.VerificationMode.options}.",
+      takesArg := .arg "mode" },
+    { name := "check-level",
+      help := s!"Check level: {Core.CheckLevel.options}.",
+      takesArg := .arg "level" },
+    { name := "verbose", help := "Enable verbose output." },
+    { name := "quiet", help := "Suppress default output." },
+    { name := "sarif",
+      help := "Write results as SARIF to <vc-directory>/aggregate-results.sarif." }
+  ]
+  help := "Aggregate solver results with .smt2 files."
+  callback := fun _v pflags => do
+    let vcDirStr ← match pflags.getString "vc-directory" with
+      | .some d => pure d
+      | .none => exitFailure "--vc-directory is required for aggregate-results."
+    let vcDir : System.FilePath := ⟨vcDirStr⟩
+    let checkMode ← match pflags.getString "check-mode" with
+      | .none => pure Core.VerificationMode.deductive
+      | .some s => match Core.VerificationMode.ofString? s with
+        | .some m => pure m
+        | .none => exitFailure s!"Invalid check mode: '{s}'. Must be {Core.VerificationMode.options}."
+    let checkLevel ← match pflags.getString "check-level" with
+      | .none => pure Core.CheckLevel.minimal
+      | .some s => match Core.CheckLevel.ofString? s with
+        | .some l => pure l
+        | .none => exitFailure s!"Invalid check level: '{s}'. Must be {Core.CheckLevel.options}."
+    let verbose : Core.VerboseMode :=
+      if pflags.getBool "verbose" then .normal
+      else if pflags.getBool "quiet" then .quiet
+      else .normal
+    let options : Core.VerifyOptions :=
+      { Core.VerifyOptions.default with
+        checkMode, checkLevel, verbose }
+    let vcResults ← Core.aggregateResultsDirectory vcDir options
+    if pflags.getBool "sarif" then
+      let files := Map.empty
+      let outputPath := (vcDir / "aggregate-results.sarif").toString
+      Core.Sarif.writeSarifOutput options.checkMode files vcResults outputPath
+    for vcResult in vcResults do
+      let posStr := Imperative.MetaData.formatFileRangeD vcResult.obligation.metadata none
+      println! f!"{posStr} [{vcResult.obligation.label}]: \
+                    {vcResult.formatOutcome}"
+    printPyAnalyzeSummary vcResults options.checkMode
+
 def pyInterpretCommand : Command where
   name := "pyInterpret"
   args := [ "file" ]
@@ -1363,7 +1418,7 @@ def pyInterpretCommand : Command where
 
 def commandGroups : List CommandGroup := [
   { name := "Core"
-    commands := [verifyCommand, transformCommand, checkCommand, toIonCommand, printCommand, diffCommand]
+    commands := [verifyCommand, aggregateResultsCommand, transformCommand, checkCommand, toIonCommand, printCommand, diffCommand]
     commonFlags := [includeFlag] },
   { name := "Code Generation"
     commands := [javaGenCommand] },
diff --git a/StrataTest/Languages/Core/Tests/SMTEncoderTests.lean b/StrataTest/Languages/Core/Tests/SMTEncoderTests.lean
index 9448b4a2dd..164edc93ce 100644
--- a/StrataTest/Languages/Core/Tests/SMTEncoderTests.lean
+++ b/StrataTest/Languages/Core/Tests/SMTEncoderTests.lean
@@ -319,10 +319,12 @@ end ArrayTheory
 
 /--
 info: (set-logic ALL)
+(set-info :strata-smt-metadata-version "1")
 ; Validity
 (assert false)
 (check-sat)
 (set-info :final-message "assert_bounds_check")
+(set-info :property "assert")
 -/
 #guard_msgs in
 #eval show IO _ from do
@@ -346,10 +348,12 @@ info: (set-logic ALL)
 
 /--
 info: (set-logic ALL)
+(set-info :strata-smt-metadata-version "1")
 ; Validity
 (assert false)
 (check-sat)
 (set-info :final-message "Division by zero is impossible")
+(set-info :property "assert")
 -/
 #guard_msgs in
 #eval show IO _ from do
diff --git a/StrataTest/Languages/Core/VCOutcomeTests.lean b/StrataTest/Languages/Core/VCOutcomeTests.lean
index c4a2b5374c..c45ef1acef 100644
--- a/StrataTest/Languages/Core/VCOutcomeTests.lean
+++ b/StrataTest/Languages/Core/VCOutcomeTests.lean
@@ -280,4 +280,27 @@ private def cleanObligation : Imperative.ProofObligation Core.Expression :=
 -- frontEndPhase: unsat is unchanged
 #guard (unsatResult.adjustForPhases [Strata.frontEndPhase] cleanObligation).1 == unsatResult
 
+/-! ### Meta-test: phase validators are stubs
+
+The solver result aggregation path passes `phases = []` to `buildVCResult`
+because phase validation cannot be reconstructed from `.smt2` metadata alone.
+This is safe ONLY because `frontEndPhase` currently always rejects (returns
+`false`).
+
+If you are implementing a real model validator for `frontEndPhase` (i.e., one
+that can return `true` for some models), you MUST also update the solver results
+aggregation path to either:
+  1. Embed phase validation decisions in `set-info` metadata during generation, or
+  2. Re-run phase validation during aggregate results by serializing enough context.
+
+See `docs/design/SplitSolveReconcile.md` for details.
+-/
+
+-- Assert that frontEndPhase is still a stub that always rejects sat.
+-- If this test fails, the solver results aggregation path needs updating.
+#guard (satResult.adjustForPhases [Strata.frontEndPhase] cleanObligation).1 == unknownResult
+#guard (satResult.adjustForPhases [Strata.frontEndPhase]
+  { label := "arbitrary", property := .assert,
+    assumptions := [], obligation := .true (), metadata := {} }).1 == unknownResult
+
 end Core
diff --git a/StrataTest/Languages/Python/run_py_ssr_test.sh b/StrataTest/Languages/Python/run_py_ssr_test.sh
new file mode 100755
index 0000000000..e3f5de4154
--- /dev/null
+++ b/StrataTest/Languages/Python/run_py_ssr_test.sh
@@ -0,0 +1,129 @@
+#!/bin/bash
+# ------------------------------------------------------------------------------
+# run_py_ssr_test.sh — Validate the Split-Solve-Aggregate Results workflow for Python.
+#
+# For each test_*.py file with an expected output, this script:
+#   1. Runs the SSR workflow via Scripts/ssr_py.sh (generate → solve → aggregate results)
+#   2. Compares the DETAIL/RESULT summary lines against the expected output
+#      from direct verification (the expected_laurel/*.expected files)
+#
+# Usage:
+#   ./run_py_ssr_test.sh [--filter <pattern>] [--solver <cmd>]
+# ------------------------------------------------------------------------------
+
+set -euo pipefail
+
+filter=""
+solver_cmd="cvc5 --produce-models"
+
+while [ $# -gt 0 ]; do
+  case "$1" in
+    --filter) filter="$2"; shift 2 ;;
+    --solver) solver_cmd="$2"; shift 2 ;;
+    -h|--help)
+      sed -n '3,12p' "$0" | sed 's/^# \{0,1\}//'
+      exit 0 ;;
+    *) echo "Unknown argument: $1"; exit 1 ;;
+  esac
+done
+
+SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)"
+REPO_ROOT="$(cd "$SCRIPT_DIR/../../.." && pwd)"
+SSR_SCRIPT="$REPO_ROOT/Scripts/ssr_py.sh"
+STRATA="$REPO_ROOT/.lake/build/bin/strata"
+DIALECT="$REPO_ROOT/dialects/Python.dialect.st.ion"
+# Fall back to the dialect file shipped with the Python tools.
+if [ ! -f "$DIALECT" ]; then
+  DIALECT="$REPO_ROOT/Tools/Python/dialects/Python.dialect.st.ion"
+fi
+EXPECTED_DIR="$SCRIPT_DIR/expected_laurel"
+
+# Verify prerequisites.
+command -v python3 >/dev/null 2>&1 || { echo "error: python3 not found"; exit 1; }
+command -v "${solver_cmd%% *}" >/dev/null 2>&1 || { echo "error: solver '${solver_cmd%% *}' not found"; exit 1; }
+[ -x "$STRATA" ] || { echo "error: strata not built. Run 'lake build strata:exe' first."; exit 1; }
+[ -f "$SSR_SCRIPT" ] || { echo "error: ssr_py.sh not found at $SSR_SCRIPT"; exit 1; }
+
+passed=0
+failed=0
+skipped=0
+
+# Extract DETAIL and RESULT lines from output — these summarize the outcome.
+extract_summary() {
+  grep -E '^(DETAIL|RESULT):' "$1" 2>/dev/null || true
+}
+
+for test_file in "$SCRIPT_DIR"/tests/test_*.py; do
+  [ -f "$test_file" ] || continue
+  base_name=$(basename "$test_file" .py)
+
+  # Apply filter.
+  if [ -n "$filter" ] && [[ "$base_name" != *"$filter"* ]]; then
+    continue
+  fi
+
+  expected_file="$EXPECTED_DIR/${base_name}.expected"
+  [ -f "$expected_file" ] || { skipped=$((skipped + 1)); continue; }
+
+  # Skip tests that use non-default check modes (bugFinding etc.) — the
+  # aggregate-results command would need matching --check-mode flags.
+  extra_args=$(grep '^# strata-args:' "$test_file" | sed 's/^# strata-args://' | head -1)
+  if echo "$extra_args" | grep -q "check-mode"; then
+    skipped=$((skipped + 1))
+    continue
+  fi
+
+  # Create a temp directory for this test's SSR artifacts.
+  ssr_dir=$(mktemp -d)
+
+  # Run the SSR workflow via ssr_py.sh.
+  ssr_output=$("$SSR_SCRIPT" \
+    --output-dir "$ssr_dir" \
+    --solver "$solver_cmd" \
+    --strata "$STRATA" \
+    --dialect "$DIALECT" \
+    "$test_file" 2>&1) || ssr_rc=$?
+  ssr_rc=${ssr_rc:-0}
+
+  if [ "$ssr_rc" -eq 1 ]; then
+    # Exit code 1 = user error (e.g., parse failure, missing prerequisites).
+    # Check if the expected file documents this as an expected error.
+    if grep -qE '^(DETAIL|RESULT):.*\b(error|Error)\b' "$expected_file"; then
+      echo "PASS (expected error): $base_name"
+      passed=$((passed + 1))
+    else
+      echo "FAIL (ssr user error): $base_name"
+      echo "  Output: $(echo "$ssr_output" | tail -3)"
+      failed=$((failed + 1))
+    fi
+    rm -rf "$ssr_dir"
+    continue
+  elif [ "$ssr_rc" -eq 3 ]; then
+    # Exit code 3 = internal error (generate/solve/aggregate crashed).
+    echo "FAIL (ssr internal error): $base_name"
+    echo "  Output: $(echo "$ssr_output" | tail -5)"
+    failed=$((failed + 1))
+    rm -rf "$ssr_dir"
+    continue
+  fi
+
+  # Compare summary lines.
+  expected_summary=$(extract_summary "$expected_file")
+  actual_summary=$(echo "$ssr_output" | grep -E '^(DETAIL|RESULT):' || true)
+
+  if [ "$expected_summary" = "$actual_summary" ]; then
+    echo "PASS: $base_name"
+    passed=$((passed + 1))
+  else
+    echo "FAIL: $base_name"
+    echo "  Expected: $expected_summary"
+    echo "  Got:      $actual_summary"
+    failed=$((failed + 1))
+  fi
+
+  rm -rf "$ssr_dir"
+done
+
+echo ""
+echo "SSR test summary: $passed passed, $failed failed, $skipped skipped"
+[ "$failed" -eq 0 ]
diff --git a/docs/design/SplitSolveAggregate.md b/docs/design/SplitSolveAggregate.md
new file mode 100644
index 0000000000..e87012ee80
--- /dev/null
+++ b/docs/design/SplitSolveAggregate.md
@@ -0,0 +1,269 @@
+# Design: Split-Solve-Aggregate Results for Cloud-Based SMT Solving
+
+## Motivation
+
+Strata's verification pipeline is bottlenecked by SMT solving, which can take
+seconds to minutes per query. For large programs, the total wall-clock time is
+dominated by sequential solver invocations. Cloud-based solving enables massive
+parallelism — all queries can be dispatched simultaneously — but requires
+decoupling the pipeline into three phases:
+
+1. **Generate** — run the Strata pipeline up to SMT file creation
+2. **Solve** — dispatch SMT queries to cloud solvers (external to Strata)
+3. **Aggregate Results** — read solver results and produce the final verification report
+
+The generation phase (parse, transform, symbolic eval, SMT encoding) can itself
+be expensive, so the aggregate results phase must **not** re-run the pipeline.
+Instead, the generate phase embeds all metadata needed for result aggregation
+directly in the `.smt2` files.
+
+## Design
+
+### Key Decision: Manifest-Free Result Aggregation
+
+Rather than emitting a separate `manifest.json` file alongside the `.smt2`
+files, all obligation metadata is embedded directly in each `.smt2` file using
+standard SMT-LIB `set-info` directives. This eliminates a separate serialization
+format, keeps each `.smt2` file self-contained, and avoids synchronization issues
+between manifest and SMT files.
+
+### Phase 1: Generate (`--no-solve`)
+
+When `--no-solve --vc-directory <dir>` is used, Strata runs the full pipeline
+(parse, transform, symbolic eval, SMT encoding) and writes `.smt2` files to the
+VC directory. Each `.smt2` file includes `set-info` directives that capture the
+obligation metadata the aggregate results phase needs.
+
+#### Embedded `set-info` Directives
+
+| Directive | Description |
+|-----------|-------------|
+| `(set-info :strata-smt-metadata-version "<N>")` | Schema version for the SMT metadata format. The aggregate results phase warns if it encounters an unrecognized version. Currently `"1"`. |
+| `(set-info :file "<path>")` | Source file path for the obligation. |
+| `(set-info :start N)` | Start offset of the source location range. |
+| `(set-info :stop N)` | End offset of the source location range. |
+| `(set-info :final-message "<msg>")` | Obligation label/message (e.g., `"assert_precondition_0"`). |
+| `(set-info :property "<type>")` | Property type: `"assert"`, `"cover"`, `"divisionByZero"`, `"arithmeticOverflow"`. |
+| `(set-info :resolved-sat "<verdict>")` | Evaluator-resolved satisfiability result (`"sat"`, `"unsat"`, `"unknown"`). Present only when the evaluator already decided this check. |
+| `(set-info :resolved-val "<verdict>")` | Evaluator-resolved validity result. Present only when the evaluator already decided this check. |
+| `(set-info :sat-message "<msg>")` | Presence indicates a satisfiability check was requested. |
+| `(set-info :unsat-message "<msg>")` | Presence indicates a validity check was requested. |
+
+These directives are emitted by `encodeCore` in `Verifier.lean` at the end of
+the SMT encoding, after the `check-sat` commands. They are comments from the
+solver's perspective (solvers ignore unknown `set-info` keys) but are parsed by
+the aggregate results phase.
+
+#### Evaluator-Resolved Obligations
+
+Some obligations are trivially resolved by the evaluator (e.g., `assert true`
+→ valid). Generating `.smt2` files for these is optional — the evaluator may
+skip SMT encoding entirely when the result is already known. When `.smt2` files
+*are* generated for such obligations, the `resolved-sat` / `resolved-val`
+directives record the evaluator's verdict. The aggregate results phase uses
+these stored results directly instead of relying on the solver output.
+
+For obligations that are resolved without generating an `.smt2` file, the
+generate phase records the result internally and includes it in the final report
+during the same run. These results do not participate in the solve/aggregate
+workflow (there is nothing to solve or aggregate).
+
+### Phase 2: Solve (external)
+
+The user runs each `.smt2` file through a solver (locally, in the cloud, etc.)
+and captures the solver's stdout into a corresponding `.result` file:
+
+```
+vcs/
+  assert_precondition_0_0.smt2
+  assert_precondition_0_0.result    ← solver stdout
+  loop_invariant_1_1.smt2
+  loop_invariant_1_1.result
+  ...
+```
+
+The `.result` file contains exactly what the solver prints to stdout — verdict
+lines (`sat`/`unsat`/`unknown`) followed by optional model output from
+`(get-value ...)` commands. This is the same format Strata already parses.
+
+If a `.result` file is missing, the aggregate results phase treats the
+obligation as `unknown`.
+
+### Phase 3: Aggregate Results (`strata aggregate-results`)
+
+```bash
+lake exe strata aggregate-results --vc-directory ./vcs/ [--check-mode deductive] [--check-level minimal] [--sarif]
+```
+
+This command:
+1. Scans the VC directory for `.smt2` files
+2. For each `.smt2` file:
+   - Parses `set-info` directives to extract obligation metadata (`SMT2Meta`)
+   - Determines which checks were requested (satisfiability, validity)
+   - If evaluator-resolved: uses the stored verdict directly
+   - Otherwise: reads the corresponding `.result` file and parses solver output
+3. Builds a `VCResult` using `buildVCResult` (the same function used by the
+   integrated verifier), applying outcome masking
+4. Merges results by assertion (`mergeByAssertion`)
+5. Produces the final report (text or SARIF)
+
+---
+
+## Aggregate Results Algorithm
+
+```
+function aggregateResultsDirectory(vcDir, options):
+  results = []
+  for each .smt2 file in vcDir (sorted by name):
+    smt2Content = readFile(smt2File)
+    meta = parseSMT2Meta(smt2Content)  // extract set-info directives
+
+    // Determine which checks were requested
+    satisfiabilityCheck = meta.hasSatCheck || meta.resolvedSat.isSome
+    validityCheck = meta.hasValCheck || meta.resolvedVal.isSome
+
+    // Get evaluator-resolved results (if any)
+    peSat? = meta.resolvedSat.map(smtResultOfString)
+    peVal? = meta.resolvedVal.map(smtResultOfString)
+
+    // Read solver output (if .result file exists)
+    resultFile = smt2File.replaceSuffix(".smt2", ".result")
+    if resultFile.exists:
+      solverOutput = readFile(resultFile)
+      (solverSat, solverVal) = parseResultFile(solverOutput,
+        satisfiabilityCheck && peSat?.isNone,
+        validityCheck && peVal?.isNone)
+    else:
+      (solverSat, solverVal) = (unknown, unknown)
+
+    // Evaluator results take precedence over solver results
+    satResult = peSat?.getD(solverSat)
+    valResult = peVal?.getD(solverVal)
+
+    // Reconstruct obligation from metadata
+    obligation = ProofObligation(meta.label, meta.property, meta.fileRange)
+
+    // Build classified VCResult (same function as integrated verifier)
+    result = buildVCResult(obligation, satResult, valResult,
+      satisfiabilityCheck, validityCheck, phases=[], options)
+    results.push(result)
+
+  return mergeByAssertion(results)
+```
+
+---
+
+## Implementation
+
+### `buildVCResult` — Shared Classification Logic
+
+The `buildVCResult` function in `Verifier.lean` is the single source of truth
+for turning raw `(satResult, valResult)` into a classified `VCResult`. It:
+
+1. Applies phase validation (`adjustForPhases`) — demotes unvalidated sat
+   results to unknown
+2. Builds the solver log
+3. Constructs the raw `VCOutcome`
+4. Applies `maskOutcome` based on which checks were requested
+5. Returns the final `VCResult`
+
+Both the integrated verifier (`getObligationResult`) and the aggregate results
+path (`aggregateFromSMT2`) call this function, ensuring consistent
+classification.
+
+### `AggregateResults.lean` — Aggregate Results Module
+
+- `parseSMT2Meta`: Parses `set-info` directives from `.smt2` file content into
+  an `SMT2Meta` structure.
+- `parseResultFile`: Parses a `.result` file's verdict lines into
+  `(satResult, valResult)`, respecting which checks were requested.
+- `aggregateFromSMT2`: Combines parsed metadata and solver output into a
+  `VCResult`.
+- `aggregateResultsDirectory`: Orchestrates the full aggregation over a
+  directory.
+
+### `StrataMain.lean` — CLI Command
+
+The `aggregateResultsCommand` accepts:
+- `--vc-directory` (required) — directory containing `.smt2` and `.result` files
+- `--check-mode` — verification mode (deductive, bugFinding, etc.)
+- `--check-level` — check level (minimal, minimalVerbose, full)
+- `--sarif` — emit SARIF output
+- `--verbose` / `--quiet` — output verbosity
+
+### `Verifier.lean` — Metadata Emission
+
+`encodeCore` is extended with `property`, `resolvedSat`, and `resolvedVal`
+parameters. These are threaded through `dischargeObligation` →
+`getObligationResult` → `verifySingleEnv`. The evaluator-resolved results
+(`peSatResult?`, `peValResult?`) are passed from `verifySingleEnv` where they
+are already computed.
+
+### Helper Scripts
+
+- `Scripts/ssr_py.sh` — End-to-end solve/aggregate workflow for Python files
+  (generate → solve → aggregate results) with parallel solving via `xargs -P`.
+
+- `StrataTest/Languages/Python/run_py_ssr_test.sh` — Integration test that
+  validates aggregation output matches direct verification for all Python test
+  files.
+
+---
+
+## Design Decisions
+
+**Why embed metadata in `.smt2` files instead of a separate manifest?**
+A separate manifest introduces synchronization concerns (manifest and `.smt2`
+files can get out of sync), requires a custom JSON schema with serialization/
+deserialization code, and makes each `.smt2` file dependent on an external file
+for interpretation. Embedding metadata via `set-info` keeps each file
+self-contained, uses a standard SMT-LIB mechanism, and is ignored by solvers.
+
+**Why not re-run the pipeline during aggregate results?**
+The symbolic evaluation step (path explosion, expression simplification) can be
+expensive for large programs. The embedded metadata avoids re-running it.
+
+**Why allow `checkMode`/`checkLevel` override in aggregate results?**
+These only affect how outcomes are classified and displayed (pass/fail/warning).
+The underlying SMT results are mode-independent. This lets users re-classify
+results without re-solving — e.g., switch from deductive to bug-finding mode.
+
+**Why pass empty `phases` in aggregate results?**
+The aggregate results path calls `buildVCResult` with `phases = []` because
+phase validation (which demotes sat results to unknown for unvalidated
+abstractions) cannot be reconstructed from the `.smt2` metadata alone. This is
+acceptable because the current phase validators are all stubs that return
+`false`. When real validators are implemented, this will need revisiting.
+
+---
+
+## Risks and Mitigations
+
+| Risk | Impact | Mitigation |
+|------|--------|------------|
+| `set-info` schema changes between generate and aggregate results | Aggregate results misinterprets metadata | `strata-smt-metadata-version` directive checked at aggregate time; warns on mismatch. New directives must be additive (backwards compatible) or bump the version. |
+| Phase validators get real implementations | Aggregate results cannot apply phase validation | Meta-test in `VCOutcomeTests.lean` asserts validators are stubs; extend `set-info` metadata when real validators land. |
+| SMT file naming collisions | Two obligations produce the same filename | Already handled: counter suffix (`_{N}`) ensures uniqueness |
+| Solver produces unexpected output format | Result parsing fails | Reuse existing verdict parsing; report clear errors for unparseable results |
+| User changes source between generate and aggregate results | Source locations in `set-info` are stale | Document that generate and aggregate results must use the same source |
+| Missing `.result` files | Obligations classified as unknown | Graceful degradation: treat missing results as `unknown` rather than failing |
+
+---
+
+## Future Extensions
+
+- **Source hash validation:** Embed a hash of the input file in `set-info`.
+  The aggregate results phase can warn if the source has changed.
+- **Incremental re-solving:** If only some obligations change after a source
+  edit, re-generate only the affected SMT files and reuse cached results for
+  unchanged obligations.
+- **Rich model display:** Currently the aggregate results path does not
+  reconstruct solver models (variable mappings are not embedded). A future
+  extension could embed variable map metadata to enable model display during
+  result aggregation.
+- **Phase validation serialization:** When validators get real implementations,
+  embed phase validation decisions in `set-info` directives so the aggregate
+  results phase can apply them.
+- **Parallel local solving:** Use the directory listing to drive parallel local
+  solver invocations (multiple cvc5 processes), as a simpler alternative to
+  cloud solving.