diff --git a/clang/include/clang/Frontend/FrontendOptions.h b/clang/include/clang/Frontend/FrontendOptions.h
index 29244682db..84b9cb70c9 100644
--- a/clang/include/clang/Frontend/FrontendOptions.h
+++ b/clang/include/clang/Frontend/FrontendOptions.h
@@ -529,6 +529,24 @@ class FrontendOptions {
   /// assumes from other files, for cpp-verify --check-contracts.
   std::string VerifyContractsOut;
 
+  /// The solver CppVerify verifies a compilation with (-fverify-backend=).
+  enum class CppVerifyBackend { Z3, CVC5, Portfolio, Race, BMC };
+  CppVerifyBackend VerifyBackend = CppVerifyBackend::Z3;
+
+  /// The milliseconds each CppVerify solver query may take, cpp-verify's
+  /// default unless given; 0 disables the limit (-fverify-timeout=).
+  unsigned VerifyTimeoutMs = 30000;
+
+  /// The solver jobs CppVerify runs for this compilation (-fverify-jobs=).
+  unsigned VerifyJobs = 1;
+
+  /// Where CppVerify keeps its proofs across compilations (-fverify-cache=).
+  std::string VerifyCache;
+
+  /// Where CppVerify writes this compilation's results as JSON Lines
+  /// (-fverify-report=).
+  std::string VerifyReport;
+
   /// Auxiliary triple for CUDA/HIP/SYCL compilation.
   std::string AuxTriple;
 
diff --git a/clang/include/clang/Options/Options.td b/clang/include/clang/Options/Options.td
index 9fe881f6d1..2de6775649 100644
--- a/clang/include/clang/Options/Options.td
+++ b/clang/include/clang/Options/Options.td
@@ -2537,6 +2537,41 @@ def fverify_contracts_out_EQ : Joined<["-"], "fverify-contracts-out=">,
   HelpText<"Write the contracts CppVerify verifies in this file and those it "
            "assumes from other files, for cpp-verify --check-contracts">,
   MarshallingInfoString<FrontendOpts<"VerifyContractsOut">>;
+def fverify_backend_EQ : Joined<["-"], "fverify-backend=">,
+  Group<f_clang_Group>, Visibility<[ClangOption, CC1Option]>,
+  HelpText<"The solver CppVerify verifies with: z3 (default), cvc5, portfolio "
+           "(z3 and cvc5 must agree), race (the first decisive answer of z3 "
+           "and cvc5), or bmc">,
+  Values<"z3,cvc5,portfolio,race,bmc">,
+  NormalizedValuesScope<"FrontendOptions::CppVerifyBackend">,
+  NormalizedValues<["Z3", "CVC5", "Portfolio", "Race", "BMC"]>,
+  MarshallingInfoEnum<FrontendOpts<"VerifyBackend">, "Z3">;
+def fverify_timeout_EQ : Joined<["-"], "fverify-timeout=">,
+  Group<f_clang_Group>, Visibility<[ClangOption, CC1Option]>,
+  MetaVarName<"<ms>">,
+  HelpText<"Milliseconds each CppVerify solver query may take (default 30000; "
+           "0 disables)">,
+  MarshallingInfoInt<FrontendOpts<"VerifyTimeoutMs">, "30000">;
+def fverify_jobs_EQ : Joined<["-"], "fverify-jobs=">,
+  Group<f_clang_Group>, Visibility<[ClangOption, CC1Option]>,
+  MetaVarName<"<n>">,
+  HelpText<"Solver jobs CppVerify runs for each compilation (default 1)">,
+  MarshallingInfoInt<FrontendOpts<"VerifyJobs">, "1">;
+def fverify_cache_EQ : Joined<["-"], "fverify-cache=">,
+  Group<f_clang_Group>, Visibility<[ClangOption, CC1Option]>,
+  MetaVarName<"<dir>">,
+  HelpText<"Keep CppVerify's proofs in <dir>, shared by compilations, so that "
+           "an unchanged obligation is not solved again">,
+  MarshallingInfoString<FrontendOpts<"VerifyCache">>;
+def fverify_report : Flag<["-"], "fverify-report">, Group<f_clang_Group>,
+  Visibility<[ClangOption]>,
+  HelpText<"Write CppVerify's results as JSON Lines beside the object file, "
+           "in <object>.cppverify.json">;
+def fverify_report_EQ : Joined<["-"], "fverify-report=">,
+  Group<f_clang_Group>, Visibility<[ClangOption, CC1Option]>,
+  MetaVarName<"<file>">,
+  HelpText<"Write CppVerify's results as JSON Lines to <file>">,
+  MarshallingInfoString<FrontendOpts<"VerifyReport">>;
 def fno_verify : Flag<["-"], "fno-verify">, Group<f_clang_Group>,
   Visibility<[ClangOption, CC1Option]>,
   HelpText<"Check contract syntax and semantics but skip CppVerify SMT verification "
diff --git a/clang/lib/CodeGen/CodeGenAction.cpp b/clang/lib/CodeGen/CodeGenAction.cpp
index f83b6f58af..f18301e263 100644
--- a/clang/lib/CodeGen/CodeGenAction.cpp
+++ b/clang/lib/CodeGen/CodeGenAction.cpp
@@ -244,8 +244,7 @@ bool BackendConsumer::LinkInModules(llvm::Module *M) {
 void BackendConsumer::HandleTranslationUnit(ASTContext &C) {
   std::optional<std::future<verify::CppVerifyAsyncResult>> VerifyFuture;
   if (verify::shouldRunCppVerify(CI))
-    VerifyFuture =
-        verify::startCppVerifyAsync(C, CI.getFrontendOpts().VerifyContractsOut);
+    VerifyFuture = verify::startCppVerifyAsync(C, CI.getFrontendOpts());
 
   {
     llvm::TimeTraceScope TimeScope("Frontend");
diff --git a/clang/lib/Driver/ToolChains/Clang.cpp b/clang/lib/Driver/ToolChains/Clang.cpp
index 116b559c6a..6b52ae3a36 100644
--- a/clang/lib/Driver/ToolChains/Clang.cpp
+++ b/clang/lib/Driver/ToolChains/Clang.cpp
@@ -6699,6 +6699,24 @@ void Clang::ConstructJob(Compilation &C, const JobAction &JA,
   // language, so when neither -f/-fno-verify-contracts was given it implies
   // -fverify-contracts, yielding a syntax/semantics-only "light check".
   Args.AddLastArg(CmdArgs, options::OPT_fverify_contracts_out_EQ);
+  for (OptSpecifier Opt :
+       {options::OPT_fverify_backend_EQ, options::OPT_fverify_timeout_EQ,
+        options::OPT_fverify_jobs_EQ, options::OPT_fverify_cache_EQ})
+    Args.AddLastArg(CmdArgs, Opt);
+  // -fverify-report writes beside the object, as -ftime-trace does.
+  if (Arg *A = Args.getLastArg(options::OPT_fverify_report,
+                               options::OPT_fverify_report_EQ)) {
+    SmallString<128> Report;
+    if (A->getOption().matches(options::OPT_fverify_report_EQ))
+      Report = A->getValue();
+    else if (Output.isFilename())
+      Report = Output.getFilename();
+    else
+      Report = llvm::sys::path::stem(Input.getBaseInput());
+    if (!A->getOption().matches(options::OPT_fverify_report_EQ))
+      Report += ".cppverify.json";
+    CmdArgs.push_back(Args.MakeArgString("-fverify-report=" + Report));
+  }
   if (Args.hasArg(options::OPT_fno_verify)) {
     CmdArgs.push_back("-fno-verify");
     if (!Args.hasArg(options::OPT_fverify_contracts) &&
diff --git a/clang/lib/Verify/Driver/CppVerifyIntegration.cpp b/clang/lib/Verify/Driver/CppVerifyIntegration.cpp
index b664448748..edb42bb204 100644
--- a/clang/lib/Verify/Driver/CppVerifyIntegration.cpp
+++ b/clang/lib/Verify/Driver/CppVerifyIntegration.cpp
@@ -3,6 +3,8 @@
 #include "Verifier.h"
 #include "clang/Basic/DiagnosticFrontend.h"
 #include "clang/Frontend/CompilerInstance.h"
+#include "clang/Frontend/FrontendOptions.h"
+#include <limits>
 #include "llvm/Support/raw_ostream.h"
 #include <thread>
 
@@ -19,16 +21,48 @@ bool verify::shouldRunCppVerify(const CompilerInstance &CI) {
   return true;
 }
 
+VerifyOptions verify::compilationOptions(const FrontendOptions &Options) {
+  VerifyOptions Opts;
+  switch (Options.VerifyBackend) {
+  case FrontendOptions::CppVerifyBackend::Z3:
+    Opts.Backend = BackendKind::Z3;
+    break;
+  case FrontendOptions::CppVerifyBackend::CVC5:
+    Opts.Backend = BackendKind::CVC5;
+    break;
+  case FrontendOptions::CppVerifyBackend::Portfolio:
+    Opts.Backend = BackendKind::Portfolio;
+    break;
+  case FrontendOptions::CppVerifyBackend::Race:
+    Opts.Backend = BackendKind::Race;
+    break;
+  case FrontendOptions::CppVerifyBackend::BMC:
+    Opts.Backend = BackendKind::BMC;
+    break;
+  }
+  const unsigned Timeout = Options.VerifyTimeoutMs;
+  const unsigned Max = std::numeric_limits<unsigned>::max();
+  Opts.SolverTimeoutMs = Timeout;
+  Opts.CollectionTimeoutMs = Timeout > Max / 2 ? 0 : 2 * Timeout;
+  Opts.FunctionTimeoutMs = Timeout > Max / 10 ? 0 : 10 * Timeout;
+  Opts.Jobs = std::max(1u, Options.VerifyJobs);
+  Opts.ProofCachePath = Options.VerifyCache;
+  Opts.ReportPath = Options.VerifyReport;
+  Opts.ContractsOut = Options.VerifyContractsOut;
+  Opts.QuietWithoutFunctions = true;
+  return Opts;
+}
+
 std::future<CppVerifyAsyncResult>
-verify::startCppVerifyAsync(ASTContext &Ctx, std::string ContractsOut) {
-  return std::async(std::launch::async, [&Ctx, ContractsOut]() {
-    CppVerifyAsyncResult Result;
-    VerifyOptions Opts;
-    Opts.ContractsOut = ContractsOut;
-    Opts.Parts = &Result.Parts;
-    Result.Ok = verifyTranslationUnit(Ctx, llvm::nulls(), Opts);
-    return Result;
-  });
+verify::startCppVerifyAsync(ASTContext &Ctx, const FrontendOptions &Options) {
+  return std::async(std::launch::async,
+                    [&Ctx, Opts = compilationOptions(Options)]() mutable {
+                      CppVerifyAsyncResult Result;
+                      Opts.Parts = &Result.Parts;
+                      Result.Ok =
+                          verifyTranslationUnit(Ctx, llvm::nulls(), Opts);
+                      return Result;
+                    });
 }
 
 bool verify::finishCppVerify(CompilerInstance &CI,
diff --git a/clang/lib/Verify/Driver/CppVerifyIntegration.h b/clang/lib/Verify/Driver/CppVerifyIntegration.h
index 8d7ec4f770..d28b127e6b 100644
--- a/clang/lib/Verify/Driver/CppVerifyIntegration.h
+++ b/clang/lib/Verify/Driver/CppVerifyIntegration.h
@@ -3,6 +3,7 @@
 #define LLVM_CLANG_VERIFY_DRIVER_CPPVERIFY_INTEGRATION_H
 
 #include "DiagnosticPart.h"
+#include "Verifier.h"
 #include <future>
 #include <string>
 #include <vector>
@@ -10,6 +11,7 @@
 namespace clang {
 class ASTContext;
 class CompilerInstance;
+class FrontendOptions;
 
 namespace verify {
 
@@ -19,15 +21,23 @@ struct CppVerifyAsyncResult {
   std::vector<VerifyDiagnosticPart> Parts;
 };
 
+/// The verifier's options for a compilation with \p Options' -fverify-*
+/// options, as cpp-verify's options of the same names set them: a query
+/// timeout also scales the collection and function timeouts. A file without
+/// a function to verify says nothing.
+VerifyOptions compilationOptions(const FrontendOptions &Options);
+
 /// Returns true if CppVerify SMT should run for this compilation.
 bool shouldRunCppVerify(const CompilerInstance &CI);
 
-/// Start SMT verification on \p Ctx in a background thread. The AST must not be
-/// mutated while the future is pending (safe during codegen IR generation).
-/// With \p ContractsOut, contracts declared without a definition are assumed
-/// and recorded there with those verified, for cpp-verify --check-contracts.
+/// Start SMT verification on \p Ctx in a background thread, with the
+/// -fverify-* options of \p Options. The AST must not be mutated while the
+/// future is pending (safe during codegen IR generation). With
+/// -fverify-contracts-out, contracts declared without a definition are
+/// assumed and recorded there with those verified, for cpp-verify
+/// --check-contracts.
 std::future<CppVerifyAsyncResult>
-startCppVerifyAsync(ASTContext &Ctx, std::string ContractsOut = "");
+startCppVerifyAsync(ASTContext &Ctx, const FrontendOptions &Options);
 
 /// Join \p Future and report its results through the compiler's diagnostics:
 /// failures as errors with notes, warnings in -Wcppverify, and proofs as
diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp
index 4115824b32..2b32533561 100644
--- a/clang/lib/Verify/Driver/Verifier.cpp
+++ b/clang/lib/Verify/Driver/Verifier.cpp
@@ -3389,8 +3389,9 @@ class Verifier {
                          "obligation"});
         return false;
       }
-      Diags.push_back(
-          {VerifyDiagnostic::Warning, "no verifiable functions found"});
+      if (!Opts.QuietWithoutFunctions)
+        Diags.push_back(
+            {VerifyDiagnostic::Warning, "no verifiable functions found"});
       return true;
     }
     Converted = std::chrono::steady_clock::now();
@@ -6662,6 +6663,27 @@ class Verifier {
                           D.K == VerifyDiagnostic::Trusted);
   }
 
+  /// Writes every result the run reports to Path as a JSON Lines record, and
+  /// then the summary record; a file that cannot be written is an error.
+  bool writeReport(const std::string &Path) {
+    std::error_code EC;
+    llvm::raw_fd_ostream Report(Path, EC, llvm::sys::fs::OF_Text);
+    if (EC) {
+      Diags.push_back({VerifyDiagnostic::Error,
+                       "cannot write the report " + Path + ": " + EC.message()});
+      return false;
+    }
+    VerifySummary Summary;
+    for (const VerifyDiagnostic &D : Diags) {
+      if (!reported(D))
+        continue;
+      count(D, Summary);
+      printJSONDiagnostic(D, Report);
+    }
+    Report << llvm::json::Value(summaryRecord(Summary)) << "\n";
+    return true;
+  }
+
   void printDiagnostics(llvm::raw_ostream &OS) const {
     for (const auto &[Loc, Line] : Listing) {
       PresumedLoc PLoc = Ctx.getSourceManager().getPresumedLoc(
@@ -6995,6 +7017,24 @@ class Verifier {
 
 } // namespace
 
+llvm::json::Object verify::summaryRecord(const VerifySummary &Summary) {
+  llvm::json::Object Record;
+  Record["schema"] = SummarySchema;
+  Record["verified"] = Summary.Verified;
+  Record["failed"] = Summary.Failed;
+  Record["unresolved"] = Summary.Unresolved;
+  llvm::json::Object Reasons;
+  for (const auto &[Reason, N] : Summary.Reasons)
+    Reasons[Reason] = N;
+  Record["reasons"] = std::move(Reasons);
+  Record["bounded_safe"] = Summary.BoundedSafe;
+  Record["trusted"] = Summary.Trusted;
+  Record["lowered"] = Summary.Lowered;
+  Record["exported"] = Summary.Exported;
+  Record["interrupted"] = Summary.Interrupted;
+  return Record;
+}
+
 bool verify::verifyTranslationUnit(ASTContext &Ctx, llvm::raw_ostream &OS,
                                    const VerifyOptions &Opts) {
   Verifier V(Ctx, Opts, OS);
@@ -7010,6 +7050,8 @@ bool verify::verifyTranslationUnit(ASTContext &Ctx, llvm::raw_ostream &OS,
   }
   if (!Opts.ContractsOut.empty())
     Ok = V.recordContracts() && Ok;
+  if (!Opts.ReportPath.empty())
+    Ok = V.writeReport(Opts.ReportPath) && Ok;
   V.printDiagnostics(OS);
   if (Opts.TimeReport)
     V.printTimeReport(OS);
diff --git a/clang/lib/Verify/Driver/Verifier.h b/clang/lib/Verify/Driver/Verifier.h
index d24b01ac41..fdca629be1 100644
--- a/clang/lib/Verify/Driver/Verifier.h
+++ b/clang/lib/Verify/Driver/Verifier.h
@@ -4,6 +4,7 @@
 
 #include "../Backend/VerifyBackend.h"
 #include "DiagnosticPart.h"
+#include "llvm/Support/JSON.h"
 #include "llvm/Support/raw_ostream.h"
 #include <map>
 #include <memory>
@@ -153,6 +154,12 @@ struct VerifyOptions {
   /// without a definition holds for now, and a proof that rests on it says
   /// so ([assumes=...]): the check of the files together settles it.
   std::string ContractsOut;
+  /// Where to write the results as JSON Lines records, besides the output,
+  /// ending with the summary record.
+  std::string ReportPath;
+  /// A file with no function to verify says nothing, as in a compilation,
+  /// where most files have none.
+  bool QuietWithoutFunctions = false;
 };
 
 /// One run over several files. A contract that a file declares without a
@@ -191,6 +198,11 @@ unsigned checkContracts(const std::vector<std::string> &Paths,
 bool verifyTranslationUnit(ASTContext &Ctx, llvm::raw_ostream &OS,
                            const VerifyOptions &Opts = VerifyOptions());
 
+/// The cppverify.summary/1 record of \p Summary: the counts of the summary
+/// line, by name, without the time, so that records do not depend on the
+/// run.
+llvm::json::Object summaryRecord(const VerifySummary &Summary);
+
 /// What exporting the modules of an archive to a Lean project gives: a
 /// result for each module, in order, with the goals cppverify_auto proves of
 /// it, and what the project warns of; or why the project was not written.
diff --git a/clang/test/Verify/Inputs/no_contracts.cpp b/clang/test/Verify/Inputs/no_contracts.cpp
new file mode 100644
index 0000000000..1f76448340
--- /dev/null
+++ b/clang/test/Verify/Inputs/no_contracts.cpp
@@ -0,0 +1 @@
+int add(int a, int b) { return a + b; }
diff --git a/clang/test/Verify/compile_options.cpp b/clang/test/Verify/compile_options.cpp
new file mode 100644
index 0000000000..aaf8c5af33
--- /dev/null
+++ b/clang/test/Verify/compile_options.cpp
@@ -0,0 +1,48 @@
+// RUN: rm -rf %t && mkdir -p %t
+// RUN: %clang -### -std=c++17 -fverify-contracts -fverify-backend=cvc5 -fverify-timeout=5000 -fverify-jobs=2 -fverify-cache=%t/cache -fverify-report -c %s -o %t/x.o 2>&1 | FileCheck %s --check-prefix=DRIVER
+// RUN: %clang -### -std=c++17 -fverify-contracts -fverify-report=%t/named.json -c %s -o %t/x.o 2>&1 | FileCheck %s --check-prefix=NAMED
+// RUN: not %clang_cc1 -std=c++17 -fverify-contracts -fverify-backend=lean -emit-obj -o %t/x.o %s 2>&1 | FileCheck %s --check-prefix=BACKEND
+// RUN: not %clang_cc1 -std=c++17 -fverify-contracts -fverify-timeout=soon -emit-obj -o %t/x.o %s 2>&1 | FileCheck %s --check-prefix=TIMEOUT
+// RUN: %clang_cc1 -std=c++17 -fverify-contracts -emit-obj -o %t/plain.o %S/Inputs/no_contracts.cpp 2>&1 | count 0
+// RUN: not %clang_cc1 -std=c++17 -fverify-contracts -Rcppverify -fverify-backend=bmc -fverify-report=%t/report.json -emit-obj -o %t/x.o %s 2>&1 | FileCheck %s
+// RUN: FileCheck %s --check-prefix=REPORT < %t/report.json
+// RUN: not %clang_cc1 -std=c++17 -fverify-contracts -fverify-cache=%t/cache -emit-obj -o %t/x.o %s
+// RUN: ls %t/cache | FileCheck %s --check-prefix=CACHE
+//
+// The -fverify-* options of a compilation: the driver forwards them, naming
+// a bare -fverify-report's file after the object; the compiler rejects an
+// invalid value; a file without a function to verify says nothing; and each
+// option reaches the verifier.
+
+namespace cv = cppverify;
+
+int inc(int x)
+  cv::pre(x < 100)
+  cv::post(cv::result == x + 1)
+{
+  return x + 1;
+}
+
+int dec(int x)
+  cv::post(cv::result == x - 1)
+{
+  return x - 1;
+}
+
+// DRIVER: "-cc1"
+// DRIVER-SAME: "-fverify-backend=cvc5" "-fverify-timeout=5000" "-fverify-jobs=2" "-fverify-cache={{[^"]*}}cache" "-fverify-report={{[^"]*}}x.o.cppverify.json"
+
+// NAMED: "-fverify-report={{[^"]*}}named.json"
+// NAMED-NOT: cppverify.json
+
+// BACKEND: error: invalid value 'lean' in '-fverify-backend=lean'
+// TIMEOUT: error: invalid integral value 'soon' in '-fverify-timeout=soon'
+
+// CHECK: remark: Verified: inc [backend=bmc, bound=0]
+// CHECK: error: verification failed: dec [overflow] [backend=bmc{{.*}}]
+
+// REPORT: "function":"inc",{{.*}}"status":"verified"
+// REPORT: "function":"dec",{{.*}}"status":"failed"
+// REPORT: {"bounded_safe":0,{{.*}}"failed":1,{{.*}}"schema":"cppverify.summary/1",{{.*}}"verified":1}
+
+// CACHE: llvmcache-cppverify-
diff --git a/clang/tools/cpp-verify/Main.cpp b/clang/tools/cpp-verify/Main.cpp
index 32ee785b69..d9fc9c91de 100644
--- a/clang/tools/cpp-verify/Main.cpp
+++ b/clang/tools/cpp-verify/Main.cpp
@@ -423,24 +423,10 @@ static void printSummary(std::chrono::steady_clock::time_point Start) {
                                  : llvm::join(Parts, ", "))
                << llvm::formatv(" in {0:f1} s", Seconds) << "\n";
 }
-/// The summary as a record: the counts of the text line, by name. It has no
-/// time, so that records do not depend on the run; --time-report gives it.
+/// The summary as a record; --time-report gives the time.
 static void printSummaryRecord() {
-  llvm::json::Object Record;
-  Record["schema"] = verify::SummarySchema;
-  Record["verified"] = gSummary.Verified;
-  Record["failed"] = gSummary.Failed;
-  Record["unresolved"] = gSummary.Unresolved;
-  llvm::json::Object Reasons;
-  for (const auto &[Reason, N] : gSummary.Reasons)
-    Reasons[Reason] = N;
-  Record["reasons"] = std::move(Reasons);
-  Record["bounded_safe"] = gSummary.BoundedSafe;
-  Record["trusted"] = gSummary.Trusted;
-  Record["lowered"] = gSummary.Lowered;
-  Record["exported"] = gSummary.Exported;
-  Record["interrupted"] = gSummary.Interrupted;
-  out() << llvm::formatv("{0}\n", llvm::json::Value(std::move(Record)));
+  out() << llvm::formatv("{0}\n",
+                         llvm::json::Value(verify::summaryRecord(gSummary)));
 }
 
 static std::vector<std::string> gArguments;
diff --git a/clang/unittests/Verify/CMakeLists.txt b/clang/unittests/Verify/CMakeLists.txt
index e6ac816df0..00f27f09f4 100644
--- a/clang/unittests/Verify/CMakeLists.txt
+++ b/clang/unittests/Verify/CMakeLists.txt
@@ -6,6 +6,7 @@ endif()
 
 add_distinct_clang_unittest(VerifyTests
   CertifyTest.cpp
+  CompilationOptionsTest.cpp
   EncodingParityTest.cpp
   MachineIntegerEncodingTest.cpp
   ObligationValidationTest.cpp
diff --git a/clang/unittests/Verify/CompilationOptionsTest.cpp b/clang/unittests/Verify/CompilationOptionsTest.cpp
new file mode 100644
index 0000000000..7c6a7772a4
--- /dev/null
+++ b/clang/unittests/Verify/CompilationOptionsTest.cpp
@@ -0,0 +1,78 @@
+//===--- CompilationOptionsTest.cpp - -fverify-* options -----------------===//
+#include "../../lib/Verify/Driver/CppVerifyIntegration.h"
+#include "clang/Frontend/FrontendOptions.h"
+#include "gtest/gtest.h"
+
+using namespace clang;
+using namespace clang::verify;
+
+namespace {
+
+TEST(CompilationOptionsTest, Defaults) {
+  FrontendOptions Options;
+  VerifyOptions Opts = compilationOptions(Options);
+  VerifyOptions Tool;
+  EXPECT_EQ(Opts.Backend, BackendKind::Z3);
+  EXPECT_EQ(Opts.SolverTimeoutMs, Tool.SolverTimeoutMs);
+  EXPECT_EQ(Opts.CollectionTimeoutMs, Tool.CollectionTimeoutMs);
+  EXPECT_EQ(Opts.FunctionTimeoutMs, Tool.FunctionTimeoutMs);
+  EXPECT_EQ(Opts.Jobs, 1u);
+  EXPECT_TRUE(Opts.ProofCachePath.empty());
+  EXPECT_TRUE(Opts.ReportPath.empty());
+  EXPECT_TRUE(Opts.QuietWithoutFunctions);
+}
+
+TEST(CompilationOptionsTest, EachOption) {
+  FrontendOptions Options;
+  Options.VerifyTimeoutMs = 5000;
+  Options.VerifyJobs = 4;
+  Options.VerifyCache = "cache";
+  Options.VerifyReport = "a.o.cppverify.json";
+  Options.VerifyContractsOut = "a.o.cppverify";
+  VerifyOptions Opts = compilationOptions(Options);
+  EXPECT_EQ(Opts.SolverTimeoutMs, 5000u);
+  EXPECT_EQ(Opts.CollectionTimeoutMs, 10000u);
+  EXPECT_EQ(Opts.FunctionTimeoutMs, 50000u);
+  EXPECT_EQ(Opts.Jobs, 4u);
+  EXPECT_EQ(Opts.ProofCachePath, "cache");
+  EXPECT_EQ(Opts.ReportPath, "a.o.cppverify.json");
+  EXPECT_EQ(Opts.ContractsOut, "a.o.cppverify");
+}
+
+TEST(CompilationOptionsTest, Backends) {
+  const std::pair<FrontendOptions::CppVerifyBackend, BackendKind> Cases[] = {
+      {FrontendOptions::CppVerifyBackend::Z3, BackendKind::Z3},
+      {FrontendOptions::CppVerifyBackend::CVC5, BackendKind::CVC5},
+      {FrontendOptions::CppVerifyBackend::Portfolio, BackendKind::Portfolio},
+      {FrontendOptions::CppVerifyBackend::Race, BackendKind::Race},
+      {FrontendOptions::CppVerifyBackend::BMC, BackendKind::BMC}};
+  for (const auto &[Option, Backend] : Cases) {
+    FrontendOptions Options;
+    Options.VerifyBackend = Option;
+    EXPECT_EQ(compilationOptions(Options).Backend, Backend);
+  }
+}
+
+TEST(CompilationOptionsTest, NoTimeout) {
+  // 0 disables every time limit, as cpp-verify --timeout=0 does.
+  FrontendOptions Options;
+  Options.VerifyTimeoutMs = 0;
+  VerifyOptions Opts = compilationOptions(Options);
+  EXPECT_EQ(Opts.SolverTimeoutMs, 0u);
+  EXPECT_EQ(Opts.CollectionTimeoutMs, 0u);
+  EXPECT_EQ(Opts.FunctionTimeoutMs, 0u);
+}
+
+TEST(CompilationOptionsTest, ExtremeValues) {
+  FrontendOptions Options;
+  Options.VerifyJobs = 0;
+  Options.VerifyTimeoutMs = 4000000000u;
+  VerifyOptions Opts = compilationOptions(Options);
+  EXPECT_EQ(Opts.Jobs, 1u);
+  EXPECT_EQ(Opts.SolverTimeoutMs, 4000000000u);
+  // Too long to scale: no bound, as cpp-verify does.
+  EXPECT_EQ(Opts.CollectionTimeoutMs, 0u);
+  EXPECT_EQ(Opts.FunctionTimeoutMs, 0u);
+}
+
+} // namespace
diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md
index 7c1cd5dab9..569ec97b01 100644
--- a/docs/ARCHITECTURE.md
+++ b/docs/ARCHITECTURE.md
@@ -3357,6 +3357,8 @@ semantics.
 
 `CppVerifyIntegration` (`clang/lib/Verify/Driver/CppVerifyIntegration.cpp`) hooks **CodeGen**: when `-fverify-contracts` is on and `-fno-verify` is off, verification runs asynchronously while LLVM IR is generated. The verifier's thread collects its results as `VerifyDiagnosticPart`s (`VerifyOptions::Parts`) instead of printing them, and `finishCppVerify` reports each through the compiler's `DiagnosticsEngine` on the main thread, which the engine requires: `err_cppverify_result` for failures and unresolved results, `warn_cppverify_result` in `-Wcppverify`, `remark_cppverify_result` in `-Rcppverify` for proofs, and `note_cppverify_result` for their notes. A result without a location of its own, as a proof has none, points at its function's declaration (`VerifyDiagnostic::FunctionLoc`). So `-Werror`, `-w`, colors, `-fdiagnostics-format=sarif`, and clangd see them as Clang's own; `err_fe_cppverify_failed` is reported only when the run fails without a result of its own. Zero ghost/spec code in the object file.
 
+The `-fverify-*` options of a compilation (`-fverify-backend=`, `-fverify-timeout=`, `-fverify-jobs=`, `-fverify-cache=`, `-fverify-report=`, `-fverify-contracts-out=`) are `FrontendOptions` fields, parsed by Clang's option marshalling, so an invalid value is the compiler's error; the driver forwards them, and turns a bare `-fverify-report` into `-fverify-report=<object>.cppverify.json`, as `-ftime-trace` names its file after the object. `compilationOptions` maps them to `VerifyOptions` as `cpp-verify` maps its options of the same names (a query timeout also scales the collection and function timeouts) and sets `QuietWithoutFunctions`, so a file without a function to verify says nothing. With `ReportPath`, `verifyTranslationUnit` also writes every reported result as a `cppverify.diagnostic/2` record and then the summary record (`summaryRecord`, which `cpp-verify` prints too).
+
 ## Tooling Integration
 
 Contracts are visible to every Clang-based tool, so editors treat them as
diff --git a/website/source/book/part-ii/ch15-toolchain-and-flags.rst b/website/source/book/part-ii/ch15-toolchain-and-flags.rst
index 012a85e8ed..f852a2b8f9 100644
--- a/website/source/book/part-ii/ch15-toolchain-and-flags.rst
+++ b/website/source/book/part-ii/ch15-toolchain-and-flags.rst
@@ -34,6 +34,24 @@ is given), so a lone ``-fno-verify`` is a fast **light check**: it validates C++
 contract syntax *and* contract semantics, but not your logic — handy for editors,
 CI pre-flight, and LLM/agent loops.
 
+Verification in a build
+-----------------------
+
+The flags go to the targets whose code has contracts, as any compiler flag
+does; in CMake:
+
+.. code-block:: cmake
+
+   target_compile_options(app PRIVATE -fverify-contracts -fverify-jobs=2
+     -fverify-cache=${CMAKE_BINARY_DIR}/cppverify-cache -fverify-report)
+
+A failure stops the build and writes no object, a file without contracts
+says nothing, the proof cache spares the solver what did not change, and
+each object's results are written beside it as JSON Lines. ``-fno-verify``
+in place of ``-fverify-contracts`` keeps a development build fast. The
+reference lists every ``-fverify-*`` option
+(:doc:`../../language/tooling`, "Options of a compilation").
+
 Code that other compilers build
 -------------------------------
 
diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst
index 05036c7eff..2f6d6a3300 100644
--- a/website/source/language/tooling.rst
+++ b/website/source/language/tooling.rst
@@ -1658,6 +1658,73 @@ Before 0.2 the compiler printed the verifier's lines as text, and then the
 one error ``cppverify: verification failed``: ``-fdiagnostics-format=sarif``
 gave a document without results, and ``-w`` and ``-Werror`` changed nothing.
 
+Options of a compilation
+~~~~~~~~~~~~~~~~~~~~~~~~
+
+A compilation verifies with ``cpp-verify``'s defaults, Z3 and 30 seconds a
+query, and one solver job. These options change that for the files they are
+given to:
+
+.. list-table::
+   :header-rows: 1
+   :widths: 38 62
+
+   * - Option
+     - Meaning (the ``cpp-verify`` option)
+   * - ``-fverify-backend=z3|cvc5|portfolio|race|bmc``
+     - The solver (``--backend``). Lean projects stay with ``cpp-verify``.
+   * - ``-fverify-timeout=<ms>``
+     - Each query's time (``--timeout``, 30000 by default, ``0`` disables);
+       a query over collections gets twice it, and one function's queries
+       together ten times it, as with ``cpp-verify``.
+   * - ``-fverify-jobs=<n>``
+     - Solver jobs for each compilation (``--jobs``), 1 by default, since a
+       build compiles several files at once: ``make -j8`` with
+       ``-fverify-jobs=2`` runs up to 16.
+   * - ``-fverify-cache=<dir>``
+     - Proofs kept in ``<dir>`` (``--proof-cache``), shared by every
+       compilation that names it, so an unchanged obligation is not solved
+       again.
+   * - ``-fverify-report``, ``-fverify-report=<file>``
+     - The results as JSON Lines records (``--diagnostics-format=json``),
+       ending with the summary record, in ``<object>.cppverify.json`` beside
+       the object file, or in ``<file>``.
+   * - ``-fverify-contracts-out=<file>``
+     - The contracts the file verifies and those it assumes, for
+       ``cpp-verify --check-contracts`` (Contracts across files, in
+       :doc:`functions-loops`).
+
+An invalid value is an error of the compiler
+(``error: invalid value 'lean' in '-fverify-backend=lean'``). A file without a
+function to verify says nothing, as most files of a project have none;
+``cpp-verify`` still warns ``no verifiable functions found`` for one. Before
+0.2 a compilation always verified with the defaults, and every file without
+contracts warned.
+
+Verification in a CMake build
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Configure the build with this compiler
+(``-DCMAKE_CXX_COMPILER=/path/to/build/bin/clang++``) and give the options to
+the targets whose code has contracts:
+
+.. code-block:: cmake
+
+   option(VERIFY "Verify contracts while compiling" ON)
+   if(VERIFY)
+     target_compile_options(app PRIVATE -fverify-contracts -fverify-jobs=2
+       -fverify-cache=${CMAKE_BINARY_DIR}/cppverify-cache -fverify-report)
+   else()
+     target_compile_options(app PRIVATE -fno-verify)
+   endif()
+
+A failure is an error of the compilation, so the build stops at it and
+writes no object. ``-DVERIFY=OFF`` still checks the contracts' syntax and
+meaning (``-fno-verify``), without the solver, for fast development builds,
+and the objects are the same either way, since contracts emit no code. With
+``-fverify-report`` each object's results lie beside it, for a CI step to
+collect.
+
 Quick lookup
 ~~~~~~~~~~~~
 
diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst
index f49c3b325b..1f41fb9516 100644
--- a/website/source/release-notes.rst
+++ b/website/source/release-notes.rst
@@ -534,6 +534,17 @@ now tried by induction too, including strong induction on a variable that
 indexes memory (``[by induction on j]``); an executable function is not
 (:doc:`book/part-ii/ch13-spec-and-proof-functions`).
 
+**Verification in a build.** ``clang++ -fverify-contracts`` verified every
+file with the defaults (Z3, 30 seconds a query, one job), and each file
+without contracts warned ``no verifiable functions found``, so a build that
+gave the flag to every file printed a warning for most of them. A compilation
+now takes ``-fverify-backend=``, ``-fverify-timeout=``, ``-fverify-jobs=``,
+``-fverify-cache=`` (proofs shared by every compilation that names the
+directory), and ``-fverify-report`` (the results as JSON Lines beside each
+object, or ``-fverify-report=<file>``); a file without a function to verify
+says nothing, and the reference shows a CMake recipe, with ``-fno-verify``
+for fast development builds (:doc:`language/tooling`).
+
 **Results as records, SARIF, and annotations.** JSON records had no source
 for a verified function, a failure's range began at its caret and ended at
 the first column of its last token, compiler errors stayed text, and nothing