diff --git a/clang/include/clang/Frontend/FrontendOptions.h b/clang/include/clang/Frontend/FrontendOptions.h
index 0f81ff3a7e..29244682db 100644
--- a/clang/include/clang/Frontend/FrontendOptions.h
+++ b/clang/include/clang/Frontend/FrontendOptions.h
@@ -525,6 +525,10 @@ class FrontendOptions {
   /// (in the format produced by -fdump-record-layouts).
   std::string OverrideRecordLayoutsFile;
 
+  /// Where CppVerify writes the contracts this file verifies and those it
+  /// assumes from other files, for cpp-verify --check-contracts.
+  std::string VerifyContractsOut;
+
   /// 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 d81b16ca14..9fe881f6d1 100644
--- a/clang/include/clang/Options/Options.td
+++ b/clang/include/clang/Options/Options.td
@@ -2531,6 +2531,12 @@ defm verify_contracts : BoolFOption<"verify-contracts",
 // default once contracts are enabled, and -fno-verify turns compilation into a
 // syntax/semantics-only "light check". It implies -fverify-contracts (handled in
 // the driver) because it is meaningless without the contract language.
+def fverify_contracts_out_EQ : Joined<["-"], "fverify-contracts-out=">,
+  Group<f_clang_Group>, Visibility<[ClangOption, CC1Option]>,
+  MetaVarName<"<file>">,
+  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 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 20452cf44b..f83b6f58af 100644
--- a/clang/lib/CodeGen/CodeGenAction.cpp
+++ b/clang/lib/CodeGen/CodeGenAction.cpp
@@ -244,7 +244,8 @@ 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);
+    VerifyFuture =
+        verify::startCppVerifyAsync(C, CI.getFrontendOpts().VerifyContractsOut);
 
   {
     llvm::TimeTraceScope TimeScope("Frontend");
diff --git a/clang/lib/Driver/ToolChains/Clang.cpp b/clang/lib/Driver/ToolChains/Clang.cpp
index 69bf819504..116b559c6a 100644
--- a/clang/lib/Driver/ToolChains/Clang.cpp
+++ b/clang/lib/Driver/ToolChains/Clang.cpp
@@ -6698,6 +6698,7 @@ void Clang::ConstructJob(Compilation &C, const JobAction &JA,
   // -fno-verify skips the SMT step. It is meaningless without the contract
   // 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);
   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/Backend/CVC5Backend.cpp b/clang/lib/Verify/Backend/CVC5Backend.cpp
index 241bee81ca..65cc962e2b 100644
--- a/clang/lib/Verify/Backend/CVC5Backend.cpp
+++ b/clang/lib/Verify/Backend/CVC5Backend.cpp
@@ -2727,6 +2727,7 @@ CVC5VerifyBackend::verifyQuery(const ObligationModule &Module,
   // One check may not spend the whole query.
   auto checkLimits = [&] {
     CertifyLimits Limits;
+    Limits.Times = times();
     Limits.Deadline = QueryDeadline;
     const unsigned CapMs = CertifyTimeoutMs ? *CertifyTimeoutMs : TimeoutMs / 2;
     if (CapMs > 0) {
diff --git a/clang/lib/Verify/Backend/Certify.cpp b/clang/lib/Verify/Backend/Certify.cpp
index 9562568603..66a8254347 100644
--- a/clang/lib/Verify/Backend/Certify.cpp
+++ b/clang/lib/Verify/Backend/Certify.cpp
@@ -3744,6 +3744,7 @@ CertifyResult verify::certifyCounterexample(const ObligationModule &Module,
                                             const LogicExpr &Query,
                                             CandidateModel &Model,
                                             const CertifyLimits &Limits) {
+  TimeInto Checking(Limits.Times ? &Limits.Times->Certification : nullptr);
   CertifyResult Result;
   auto Run = [&] {
     Evaluator Definitions(Module, Model, Limits, View::Definitions);
diff --git a/clang/lib/Verify/Backend/Certify.h b/clang/lib/Verify/Backend/Certify.h
index 9c8a95c665..807761b552 100644
--- a/clang/lib/Verify/Backend/Certify.h
+++ b/clang/lib/Verify/Backend/Certify.h
@@ -154,6 +154,8 @@ struct CertifyLimits {
   /// Set when Deadline is the time one counterexample check may take, not
   /// the query's: the message then says so.
   std::optional<unsigned> CheckTimeoutMs;
+  /// Where the checks' time is counted, for --time-report.
+  BackendTimes *Times = nullptr;
 };
 
 /// A logical application at concrete arguments whose model value differs from
diff --git a/clang/lib/Verify/Backend/Timing.h b/clang/lib/Verify/Backend/Timing.h
new file mode 100644
index 0000000000..72e2c37b25
--- /dev/null
+++ b/clang/lib/Verify/Backend/Timing.h
@@ -0,0 +1,44 @@
+//===--- Timing.h - Where a function's verification spends its time -----===//
+#ifndef LLVM_CLANG_VERIFY_BACKEND_TIMING_H
+#define LLVM_CLANG_VERIFY_BACKEND_TIMING_H
+
+#include <atomic>
+#include <chrono>
+#include <cstdint>
+
+namespace clang {
+namespace verify {
+
+/// The time the backends of one function's verification spend, in
+/// nanoseconds: solving is the wall time in VerifyBackend::verify, induction
+/// the part of it spent on inductions, and certification the time of the
+/// counterexample checks, summed over checks that may run at once.
+struct BackendTimes {
+  std::atomic<uint64_t> Solving{0};
+  std::atomic<uint64_t> Induction{0};
+  std::atomic<uint64_t> Certification{0};
+};
+
+/// Adds the time from its construction to its destruction to a counter, if
+/// there is one.
+class TimeInto {
+  std::atomic<uint64_t> *Counter;
+  std::chrono::steady_clock::time_point Start;
+
+public:
+  explicit TimeInto(std::atomic<uint64_t> *Counter)
+      : Counter(Counter), Start(std::chrono::steady_clock::now()) {}
+  TimeInto(const TimeInto &) = delete;
+  TimeInto &operator=(const TimeInto &) = delete;
+  ~TimeInto() {
+    if (Counter)
+      Counter->fetch_add(std::chrono::duration_cast<std::chrono::nanoseconds>(
+                             std::chrono::steady_clock::now() - Start)
+                             .count());
+  }
+};
+
+} // namespace verify
+} // namespace clang
+
+#endif
diff --git a/clang/lib/Verify/Backend/VerifyBackend.cpp b/clang/lib/Verify/Backend/VerifyBackend.cpp
index c0142054db..cd7afa36e2 100644
--- a/clang/lib/Verify/Backend/VerifyBackend.cpp
+++ b/clang/lib/Verify/Backend/VerifyBackend.cpp
@@ -59,6 +59,10 @@ class BMCVerifyBackend : public VerifyBackend {
                                              /*ReuseVerifiedQueries=*/true)),
         MaxUnrollBound(UnrollBound) {}
   llvm::StringRef getName() const override { return "bmc"; }
+  void setTimes(std::shared_ptr<BackendTimes> T) override {
+    Z3->setTimes(T);
+    VerifyBackend::setTimes(std::move(T));
+  }
   std::optional<unsigned>
   queryTimeoutMs(const ObligationModule &Module) const override {
     return Z3->queryTimeoutMs(Module);
@@ -232,6 +236,11 @@ class PortfolioVerifyBackend : public VerifyBackend {
         MaxQueryNodes(Execution.MaxQueryNodes) {}
 
   llvm::StringRef getName() const override { return "portfolio"; }
+  void setTimes(std::shared_ptr<BackendTimes> T) override {
+    Z3->setTimes(T);
+    CVC5->setTimes(T);
+    VerifyBackend::setTimes(std::move(T));
+  }
   std::optional<unsigned>
   queryTimeoutMs(const ObligationModule &Module) const override {
     return Z3->queryTimeoutMs(Module);
@@ -499,6 +508,7 @@ void verify::requestInterrupt() { InterruptFlag.store(true); }
 bool verify::interruptRequested() { return InterruptFlag.load(); }
 
 VerifyResult VerifyBackend::verify(const ObligationModule &Module) {
+  TimeInto Solving(Times ? &Times->Solving : nullptr);
   VerifyResult Result = verifyDirect(Module);
   if (Module.Attempt != ModuleAttempt::Primary ||
       Result.Status != VerifyStatus::Unresolved ||
@@ -522,6 +532,7 @@ VerifyResult VerifyBackend::verify(const ObligationModule &Module) {
   }
   setDeadline(Until);
   llvm::scope_exit Restore([&] { setDeadline(Saved); });
+  TimeInto Inducting(Times ? &Times->Induction : nullptr);
   std::vector<std::string> Tried;
   for (const InductionScheme &Scheme : inductionSchemes(Module)) {
     if (Until && std::chrono::steady_clock::now() >= *Until)
@@ -614,6 +625,9 @@ VerifyResult VerifyBackend::verifyDirect(const ObligationModule &Module) {
   VerifyResult Result = verifyModule(Module);
   if (Result.BackendName.empty())
     Result.BackendName = getName().str();
+  for (VerifyResult &More : Result.MoreFailures)
+    if (More.BackendName.empty())
+      More.BackendName = Result.BackendName;
   if (!Capabilities.ProducesVerificationVerdict &&
       Result.Status != VerifyStatus::Exported &&
       Result.Status != VerifyStatus::Unresolved) {
@@ -686,6 +700,11 @@ class RaceVerifyBackend : public VerifyBackend {
         MaxQueryNodes(Execution.MaxQueryNodes) {}
 
   llvm::StringRef getName() const override { return "race"; }
+  void setTimes(std::shared_ptr<BackendTimes> T) override {
+    Z3->setTimes(T);
+    CVC5->setTimes(T);
+    VerifyBackend::setTimes(std::move(T));
+  }
   std::optional<unsigned>
   queryTimeoutMs(const ObligationModule &Module) const override {
     return Z3->queryTimeoutMs(Module);
diff --git a/clang/lib/Verify/Backend/VerifyBackend.h b/clang/lib/Verify/Backend/VerifyBackend.h
index 3a891f5f6e..2a8235e10e 100644
--- a/clang/lib/Verify/Backend/VerifyBackend.h
+++ b/clang/lib/Verify/Backend/VerifyBackend.h
@@ -3,6 +3,7 @@
 #define LLVM_CLANG_VERIFY_BACKEND_VERIFYBACKEND_H
 
 #include "Obligation.h"
+#include "Timing.h"
 #include "llvm/ADT/StringRef.h"
 #include "llvm/Support/ThreadPool.h"
 #include <chrono>
@@ -146,6 +147,9 @@ struct VerifyResult {
   std::string Message;
   std::vector<VerifyModelValue> Model;
   std::vector<VerifyTraceEvent> Trace;
+  /// The failing obligations after this one, in order, each with its own
+  /// counterexample, as many as the run's MaxFailures allows.
+  std::vector<VerifyResult> MoreFailures;
   std::string ObligationId;
   std::optional<ObligationKind> ObligationType;
   /// For a certified counterexample: the value of every free variable of the
@@ -217,6 +221,10 @@ class VerifyBackend {
     FunctionDeadline = D;
     applyDeadline(D);
   }
+  /// Counts the time this backend spends into \p T, for --time-report.
+  virtual void setTimes(std::shared_ptr<BackendTimes> T) {
+    Times = std::move(T);
+  }
   /// Stops the work in progress, from any thread: queries running end
   /// unresolved and no further one starts, until resume().
   virtual void cancel() {}
@@ -232,9 +240,11 @@ class VerifyBackend {
   /// Limits the queries that start from now on to \p D.
   virtual void
   applyDeadline(std::optional<std::chrono::steady_clock::time_point> D) {}
+  BackendTimes *times() const { return Times.get(); }
 
 private:
   std::optional<std::chrono::steady_clock::time_point> FunctionDeadline;
+  std::shared_ptr<BackendTimes> Times;
 };
 
 /// Race: Z3 and cvc5 at once, the first proof or certified counterexample
@@ -287,6 +297,9 @@ struct BackendExecutionOptions {
   /// unresolved. Interactive fallback backends can consume those unresolved
   /// obligations without spending a second whole-module timeout budget.
   bool SkipWholeModuleRetry = false;
+  /// How many failing obligations of a module are reported, each with its
+  /// own counterexample; 0 reports every one.
+  unsigned MaxFailures = 1;
   /// Solve the whole-module query once, at the full budget, and report it:
   /// no per-obligation queries, refinement fallback, or induction. For small
   /// auxiliary questions such as the vacuity checks.
diff --git a/clang/lib/Verify/Backend/Z3Encode.cpp b/clang/lib/Verify/Backend/Z3Encode.cpp
index e7774fa955..7256b8e7fc 100644
--- a/clang/lib/Verify/Backend/Z3Encode.cpp
+++ b/clang/lib/Verify/Backend/Z3Encode.cpp
@@ -1819,6 +1819,8 @@ void Z3Encoder::resume() {
 
 Z3Encoder::PassScope::PassScope(Z3Encoder &Outer, Z3Encoder &Inner)
     : Outer(Outer) {
+  // The inner pass's checks are the outer query's.
+  Inner.Times = Outer.Times;
   std::lock_guard<std::mutex> Guard(Outer.CheckLock);
   Outer.Pass = &Inner;
   if (Outer.Stopped)
@@ -2281,6 +2283,7 @@ z3::expr Z3Encoder::evaluated(const z3::model &Model, const z3::expr &E,
 }
 
 CertifyLimits Z3Encoder::checkLimits(CertifyLimits Limits) const {
+  Limits.Times = Times;
   // One check may not spend the whole query: a slow one leaves time for the
   // others and for the later stages.
   const unsigned CapMs = CertifyTimeoutMs ? *CertifyTimeoutMs : TimeoutMs / 2;
@@ -3595,8 +3598,8 @@ static VerifyResult finishZ3Result(VerifyResult Result) {
 
 std::vector<VerifyResult>
 Z3VerifyBackend::verifyObligations(const ObligationModule &Module,
-                                   bool StopAtFailure, Race *Racing,
-                                   unsigned TimeoutCapMs) {
+                                   std::optional<unsigned> ReportedFailures,
+                                   Race *Racing, unsigned TimeoutCapMs) {
   TimeoutMs =
       budget(moduleTimeoutMs(Module, SolverTimeoutMs, CollectionTimeoutMs));
   if (TimeoutCapMs != 0)
@@ -3626,13 +3629,31 @@ Z3VerifyBackend::verifyObligations(const ObligationModule &Module,
   auto IsReused = [&](size_t I) {
     return ReuseVerifiedQueries && VerifiedQueries.count(QueryHashes[I]) != 0;
   };
+  // When failures are reported, each obligation after the first failure is
+  // solved in the executions that pass every earlier one that fails, as
+  // Boogie assumes an assertion after checking it: alone, its counterexample
+  // could start where an earlier check already fails, and fixing that one
+  // would remove it. A check not settled is not assumed, so a proof past
+  // the failures rests on no check that may not hold.
+  const unsigned StopAfterFailures = ReportedFailures.value_or(0);
+  std::vector<size_t> Failing;
+  std::vector<bool> PastEarlier(Module.Obligations.size());
   if (Jobs == 1 || Module.Obligations.size() < 2) {
+    unsigned Failures = 0;
     for (size_t I = 0; I != Module.Obligations.size(); ++I) {
-      Results.push_back(verifyObligation(
-          Module, Module.Obligations[I],
-          Cache ? llvm::StringRef(CacheHashes[I]) : llvm::StringRef(),
-          Cache ? &CacheLookups[I] : nullptr, IsReused(I), Racing));
-      if (StopAtFailure && Results.back().Status == VerifyStatus::Failed)
+      PastEarlier[I] = ReportedFailures && Failures != 0;
+      Results.push_back(
+          PastEarlier[I]
+              ? verifyPastEarlier(Module, I, Failing, Racing)
+              : verifyObligation(Module, Module.Obligations[I],
+                                 Cache ? llvm::StringRef(CacheHashes[I])
+                                       : llvm::StringRef(),
+                                 Cache ? &CacheLookups[I] : nullptr,
+                                 IsReused(I), Racing));
+      if (Results.back().Status != VerifyStatus::Failed)
+        continue;
+      Failing.push_back(I);
+      if (++Failures == StopAfterFailures)
         break;
     }
   } else {
@@ -3656,10 +3677,26 @@ Z3VerifyBackend::verifyObligations(const ObligationModule &Module,
     Group.wait();
     for (std::shared_future<VerifyResult> &Future : Futures)
       Results.push_back(Future.get());
+    // A failure after the first is solved again past the earlier checks; a
+    // proof or an unresolved result stays one there.
+    unsigned Failures = 0;
+    for (size_t I = 0;
+         ReportedFailures && I != Results.size() &&
+         (StopAfterFailures == 0 || Failures < StopAfterFailures);
+         ++I) {
+      if (Failures != 0 && Results[I].Status == VerifyStatus::Failed) {
+        PastEarlier[I] = true;
+        Results[I] = verifyPastEarlier(Module, I, Failing, Racing);
+      }
+      if (Results[I].Status == VerifyStatus::Failed) {
+        Failing.push_back(I);
+        ++Failures;
+      }
+    }
   }
   if (ReuseVerifiedQueries)
     for (size_t I = 0; I != Results.size(); ++I)
-      if (Results[I].Status == VerifyStatus::Verified)
+      if (Results[I].Status == VerifyStatus::Verified && !PastEarlier[I])
         VerifiedQueries.insert(QueryHashes[I]);
   return Results;
 }
@@ -3671,7 +3708,8 @@ Z3VerifyBackend::Z3VerifyBackend(const BackendExecutionOptions &Execution,
       SolverTimeoutMs(Execution.SolverTimeoutMs),
       CollectionTimeoutMs(Execution.CollectionTimeoutMs),
       ResourceLimit(Execution.SolverResourceLimit), Jobs(Execution.Jobs),
-      Pool(Execution.Pool), MaxQueryNodes(Execution.MaxQueryNodes),
+      MaxFailures(Execution.MaxFailures), Pool(Execution.Pool),
+      MaxQueryNodes(Execution.MaxQueryNodes),
       IntegerEncoding(Execution.IntegerEncoding),
       SkipWholeModuleRetry(Execution.SkipWholeModuleRetry),
       SingleQuery(Execution.SingleQuery),
@@ -3742,6 +3780,7 @@ VerifyResult Z3VerifyBackend::solveQuery(
                                     ? std::optional<unsigned>(TimeoutMs / 2)
                                     : CertifyTimeoutMs);
     Encoder.setSearchSlice(Slice);
+    Encoder.setTimes(times());
     Encoder.setIntegerEncoding(IntegerEncoding);
     Encoder.setProfileQuantifiers(ProfileQuantifiers && Facts);
     Encoder.setSequenceFacts(Facts);
@@ -3789,6 +3828,18 @@ VerifyResult Z3VerifyBackend::solveQuery(
   return WithFacts;
 }
 
+/// \p Result as the result of obligation \p Item.
+static VerifyResult attributed(VerifyResult Result, const Obligation &Item) {
+  Result.ObligationId = Item.StableId.empty() ? Item.Id : Item.StableId;
+  Result.ObligationType = Item.Kind;
+  Result.Location = Item.Loc;
+  Result.Source = Item.Source;
+  if (Result.Status == VerifyStatus::Unresolved)
+    Result.Message = "proof obligation " + Result.ObligationId +
+                     (Result.Message.empty() ? "" : ": " + Result.Message);
+  return finishZ3Result(std::move(Result));
+}
+
 VerifyResult Z3VerifyBackend::verifyObligation(const ObligationModule &Module,
                                                const Obligation &Item,
                                                llvm::StringRef SemanticHash,
@@ -3836,14 +3887,31 @@ VerifyResult Z3VerifyBackend::verifyObligation(const ObligationModule &Module,
     }
   }
 
-  Result.ObligationId = Item.StableId.empty() ? Item.Id : Item.StableId;
-  Result.ObligationType = Item.Kind;
-  Result.Location = Item.Loc;
-  Result.Source = Item.Source;
-  if (Result.Status == VerifyStatus::Unresolved)
-    Result.Message = "proof obligation " + Result.ObligationId +
-                     (Result.Message.empty() ? "" : ": " + Result.Message);
-  return finishZ3Result(std::move(Result));
+  return attributed(std::move(Result), Item);
+}
+
+VerifyResult
+Z3VerifyBackend::verifyPastEarlier(const ObligationModule &Module, size_t I,
+                                   const std::vector<size_t> &Earlier,
+                                   Race *Racing) {
+  const Obligation &Item = Module.Obligations[I];
+  auto Query = cloneLogicExpr(Item.CounterexampleQuery.get());
+  for (size_t J : Earlier) {
+    auto Conjunction = std::make_unique<LogicExpr>(LogicExpr::And);
+    Conjunction->Sort = LogicSort::boolSort();
+    Conjunction->Loc = Query->Loc;
+    Conjunction->EndLoc = Query->EndLoc;
+    Conjunction->Source = Query->Source;
+    Conjunction->Children.push_back(std::move(Query));
+    Conjunction->Children.push_back(
+        cloneLogicExpr(Module.Obligations[J].Goal.get()));
+    Query = std::move(Conjunction);
+  }
+  return attributed(spent() ? timeSpent()
+                            : solveQuery(Module, Query.get(),
+                                         Item.TraceEventCount,
+                                         budget(TimeoutMs), Racing),
+                    Item);
 }
 
 /// Internal IDs of the obligations that one-to-one Results did not prove.
@@ -3859,6 +3927,17 @@ unprovedObligations(const ObligationModule &Module,
   return Unproved;
 }
 
+VerifyResult
+Z3VerifyBackend::withMoreFailures(std::vector<VerifyResult> &Results,
+                                  size_t First) {
+  VerifyResult Reported = std::move(Results[First]);
+  for (size_t I = First + 1; I != Results.size(); ++I)
+    if (Results[I].Status == VerifyStatus::Failed &&
+        (MaxFailures == 0 || Reported.MoreFailures.size() + 1 < MaxFailures))
+      Reported.MoreFailures.push_back(std::move(Results[I]));
+  return Reported;
+}
+
 VerifyResult Z3VerifyBackend::verifyModule(const ObligationModule &Module) {
   TimeoutMs =
       budget(moduleTimeoutMs(Module, SolverTimeoutMs, CollectionTimeoutMs));
@@ -4014,7 +4093,7 @@ Z3VerifyBackend::verifyModuleDirect(const ObligationModule &Module) {
     Group.emplace(*Pool);
     Ordered = Group->async([this, &Module, &Rivals, &WholeRace] {
       std::vector<VerifyResult> Results =
-          verifyObligations(Module, /*StopAtFailure=*/true, &Rivals);
+          verifyObligations(Module, MaxFailures, &Rivals);
       // The obligations settle the module when they prove all of it or one
       // fails, and the whole query, or its retry, is then stopped.
       if (llvm::any_of(Results,
@@ -4070,8 +4149,7 @@ Z3VerifyBackend::verifyModuleDirect(const ObligationModule &Module) {
   if (Whole.Status == VerifyStatus::Verified)
     return finishZ3Result(std::move(Whole));
   auto orderedResults = [&] {
-    return Racing ? Ordered.get()
-                  : verifyObligations(Module, /*StopAtFailure=*/true);
+    return Racing ? Ordered.get() : verifyObligations(Module, MaxFailures);
   };
 
   if (Whole.Status == VerifyStatus::Failed) {
@@ -4084,18 +4162,18 @@ Z3VerifyBackend::verifyModuleDirect(const ObligationModule &Module) {
       TimeoutMs = FullTimeout;
       UnitsCap = 0;
     });
-    std::vector<VerifyResult> Results = verifyObligations(
-        Module, /*StopAtFailure=*/true, nullptr, WholeTimeout);
+    std::vector<VerifyResult> Results =
+        verifyObligations(Module, MaxFailures, nullptr, WholeTimeout);
     bool SawUnresolved = false;
-    for (VerifyResult &Result : Results) {
-      if (Result.Status == VerifyStatus::Verified)
+    for (size_t I = 0; I != Results.size(); ++I) {
+      if (Results[I].Status == VerifyStatus::Verified)
         continue;
-      if (Result.Status == VerifyStatus::Unresolved) {
+      if (Results[I].Status == VerifyStatus::Unresolved) {
         SawUnresolved = true;
         continue;
       }
-      if (Result.Status == VerifyStatus::Failed)
-        return std::move(Result);
+      if (Results[I].Status == VerifyStatus::Failed)
+        return withMoreFailures(Results, I);
     }
     if (SawUnresolved)
       return finishZ3Result(std::move(Whole));
@@ -4122,13 +4200,16 @@ Z3VerifyBackend::verifyModuleDirect(const ObligationModule &Module) {
   std::optional<std::vector<std::string>> Unproved =
       unprovedObligations(Module, Results);
   std::optional<VerifyResult> FirstUnresolved;
-  for (VerifyResult &Result : Results) {
+  for (size_t I = 0; I != Results.size(); ++I) {
+    VerifyResult &Result = Results[I];
     if (Result.Status != VerifyStatus::Verified) {
       if (Result.Status == VerifyStatus::Unresolved) {
         if (!FirstUnresolved)
           FirstUnresolved = std::move(Result);
         continue;
       }
+      if (Result.Status == VerifyStatus::Failed)
+        return withMoreFailures(Results, I);
       return std::move(Result);
     }
   }
diff --git a/clang/lib/Verify/Backend/Z3Encode.h b/clang/lib/Verify/Backend/Z3Encode.h
index 4cdbac49bb..b64f9dd908 100644
--- a/clang/lib/Verify/Backend/Z3Encode.h
+++ b/clang/lib/Verify/Backend/Z3Encode.h
@@ -70,6 +70,7 @@ class Z3Encoder {
                             std::optional<uint64_t> TraceEventCount);
   std::chrono::steady_clock::time_point QueryStart;
   std::optional<unsigned> CertifyTimeoutMs;
+  BackendTimes *Times = nullptr;
   bool SearchSlice = false;
   bool QuantifiedQuery = false;
   z3::solver freshSolver();
@@ -295,6 +296,8 @@ class Z3Encoder {
   void setCertifyTimeoutMs(std::optional<unsigned> Ms) {
     CertifyTimeoutMs = Ms;
   }
+  /// Where the counterexample checks' time is counted.
+  void setTimes(BackendTimes *T) { Times = T; }
   /// The timeout is a slice of the query's time, for the search only: a model
   /// found is checked with the check's own time, not what is left of it.
   void setSearchSlice(bool Slice) { SearchSlice = Slice; }
@@ -333,6 +336,8 @@ class Z3VerifyBackend : public VerifyBackend {
   /// of their queries may do: the work the complete query's probe had, or 0.
   unsigned UnitsCap = 0;
   unsigned Jobs;
+  /// How many failing obligations a module reports; 0: every one.
+  unsigned MaxFailures;
   llvm::StdThreadPool *Pool;
   uint64_t MaxQueryNodes;
   MachineIntegerEncoding IntegerEncoding;
@@ -345,6 +350,10 @@ class Z3VerifyBackend : public VerifyBackend {
 
   std::optional<std::chrono::steady_clock::time_point> Deadline;
   unsigned budget(unsigned Ms) const { return withinDeadline(Ms, Deadline); }
+  /// The failure at First of the results of verifyObligations, carrying the
+  /// failures after it, as many as MaxFailures allows.
+  VerifyResult withMoreFailures(std::vector<VerifyResult> &Results,
+                                size_t First);
   /// The function's time is spent, so no further query starts.
   bool spent() const {
     return Cancellation.Cancelled ||
@@ -381,6 +390,12 @@ class Z3VerifyBackend : public VerifyBackend {
                                 llvm::StringRef SemanticHash = {},
                                 const ProofCacheLookup *Lookup = nullptr,
                                 bool Reused = false, Race *Racing = nullptr);
+  /// Obligation \p I of \p Module in the executions that pass every one of
+  /// \p Earlier, failing obligations before it. No cache holds it, since it
+  /// asks less than the obligation.
+  VerifyResult verifyPastEarlier(const ObligationModule &Module, size_t I,
+                                 const std::vector<size_t> &Earlier,
+                                 Race *Racing);
 
 public:
   explicit Z3VerifyBackend(const BackendExecutionOptions &Execution = {},
@@ -390,13 +405,15 @@ class Z3VerifyBackend : public VerifyBackend {
   BackendCapabilities getCapabilities() const override {
     return {allLogicFeatures(), true};
   }
-  /// One result per obligation in order. With StopAtFailure a serial run ends
-  /// after the first failure, since later results cannot change it. A nonzero
-  /// TimeoutCapMs bounds every query's timeout.
-  std::vector<VerifyResult> verifyObligations(const ObligationModule &Module,
-                                              bool StopAtFailure = false,
-                                              Race *Racing = nullptr,
-                                              unsigned TimeoutCapMs = 0);
+  /// One result per obligation in order, each solved alone. With
+  /// ReportedFailures, a serial run ends after that many failures (0: never),
+  /// since later results are not reported, and each obligation after the
+  /// first failure is solved in the executions that pass every earlier one
+  /// that fails. A nonzero TimeoutCapMs bounds every query's timeout.
+  std::vector<VerifyResult>
+  verifyObligations(const ObligationModule &Module,
+                    std::optional<unsigned> ReportedFailures = std::nullopt,
+                    Race *Racing = nullptr, unsigned TimeoutCapMs = 0);
   void cancel() override { Cancellation.cancel(); }
   void resume() override { Cancellation.reset(); }
   std::optional<unsigned>
diff --git a/clang/lib/Verify/Driver/CppVerifyIntegration.cpp b/clang/lib/Verify/Driver/CppVerifyIntegration.cpp
index c3c09897ab..497bcfe7c3 100644
--- a/clang/lib/Verify/Driver/CppVerifyIntegration.cpp
+++ b/clang/lib/Verify/Driver/CppVerifyIntegration.cpp
@@ -20,11 +20,13 @@ bool verify::shouldRunCppVerify(const CompilerInstance &CI) {
 }
 
 std::future<CppVerifyAsyncResult>
-verify::startCppVerifyAsync(ASTContext &Ctx) {
-  return std::async(std::launch::async, [&Ctx]() {
+verify::startCppVerifyAsync(ASTContext &Ctx, std::string ContractsOut) {
+  return std::async(std::launch::async, [&Ctx, ContractsOut]() {
     std::string Buffer;
     llvm::raw_string_ostream OS(Buffer);
-    bool Ok = verifyTranslationUnit(Ctx, OS, VerifyOptions{});
+    VerifyOptions Opts;
+    Opts.ContractsOut = ContractsOut;
+    bool Ok = verifyTranslationUnit(Ctx, OS, Opts);
     OS.flush();
     return CppVerifyAsyncResult{Ok, std::move(Buffer)};
   });
diff --git a/clang/lib/Verify/Driver/CppVerifyIntegration.h b/clang/lib/Verify/Driver/CppVerifyIntegration.h
index 6246a1b392..bfee19996e 100644
--- a/clang/lib/Verify/Driver/CppVerifyIntegration.h
+++ b/clang/lib/Verify/Driver/CppVerifyIntegration.h
@@ -19,7 +19,10 @@ 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).
-std::future<CppVerifyAsyncResult> startCppVerifyAsync(ASTContext &Ctx);
+/// With \p ContractsOut, 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 = "");
 
 /// Join \p Future, print verifier output, and report diagnostics on failure.
 bool finishCppVerify(CompilerInstance &CI, std::future<CppVerifyAsyncResult> Future);
diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp
index 8967072384..ffbcefbafa 100644
--- a/clang/lib/Verify/Driver/Verifier.cpp
+++ b/clang/lib/Verify/Driver/Verifier.cpp
@@ -13,6 +13,7 @@
 #include "../Backend/ProofCache.h"
 #include "../Backend/SpecAxioms.h"
 #include "../Backend/TaskGroup.h"
+#include "../Backend/Z3Encode.h"
 #include "../Frontend/ASTConverter.h"
 #include "../IR/VStmt.h"
 #include "../Transform/LoopUnroll.h"
@@ -37,11 +38,13 @@
 #include "llvm/Support/Error.h"
 #include "llvm/Support/FileSystem.h"
 #include "llvm/Support/FormatVariadic.h"
+#include "llvm/Support/GlobPattern.h"
 #include "llvm/Support/JSON.h"
 #include "llvm/Support/MD5.h"
 #include "llvm/Support/MathExtras.h"
 #include "llvm/Support/MemoryBuffer.h"
 #include "llvm/Support/Path.h"
+#include "llvm/Support/Process.h"
 #include "llvm/Support/Program.h"
 #include "llvm/Support/SHA256.h"
 #include "llvm/Support/ThreadPool.h"
@@ -58,6 +61,66 @@
 using namespace clang;
 using namespace verify;
 
+/// One printed result of a file of a run over several files, as verified
+/// and, for a proof that rests on contracts the file declares without a
+/// definition, as unresolved for want of one of them (the contract's
+/// description in place of ContractPlaceholder); with what each counts.
+struct CrossFileLine {
+  std::string Text;
+  std::string Demoted;
+  VerifySummary Counts;
+  VerifySummary DemotedCounts;
+  /// The keys of the contracts the proof rests on; empty for any other line.
+  std::set<std::string> Assumes;
+  /// A finding about a proof (its line), and whether it holds for the entry
+  /// state alone, which no callee contract enters.
+  std::optional<size_t> FindingOf;
+  bool FoundAtEntry = false;
+  /// A warning shown only when no file of the run defines this contract.
+  std::string UnlessDefined;
+};
+
+/// A contract a file verifies, offered to the other files.
+struct CrossFileContract {
+  std::string Name;
+  std::string File;
+  bool Established = false;
+  std::set<std::string> Assumes;
+};
+
+struct CrossFileReport {
+  std::vector<CrossFileLine> Lines;
+  /// Printed after the lines (the time report).
+  std::string Trailer;
+  bool Ok = true;
+  std::map<std::string, CrossFileContract> Defined;
+  /// The names of the contracts the lines rest on, by key.
+  std::map<std::string, std::string> Names;
+};
+
+static constexpr llvm::StringLiteral ContractPlaceholder =
+    "@@cppverify-contract@@";
+
+static void addSummary(VerifySummary &To, const VerifySummary &From) {
+  To.Verified += From.Verified;
+  To.Failed += From.Failed;
+  To.Unresolved += From.Unresolved;
+  To.BoundedSafe += From.BoundedSafe;
+  To.Trusted += From.Trusted;
+  To.Lowered += From.Lowered;
+  To.Exported += From.Exported;
+  To.Interrupted += From.Interrupted;
+  for (const auto &[Reason, Count] : From.Reasons)
+    To.Reasons[Reason] += Count;
+}
+
+struct CrossFileRun::Impl {
+  std::vector<CrossFileReport> Files;
+};
+
+CrossFileRun::CrossFileRun() : State(std::make_unique<Impl>()) {}
+CrossFileRun::~CrossFileRun() = default;
+
 namespace {
 
 /// How deep the driver unfolds inductive predicates in a function, one
@@ -1101,8 +1164,22 @@ struct VerifyDiagnostic {
   SourceRange Span;
   /// A spec function that needs no check, listed with --verbose: no verdict.
   bool Axiom = false;
+  /// What else the verifier found about the verdict, each printed as a note.
+  std::vector<std::string> Notes;
+  /// A failing obligation after the one a function's verdict reports: no
+  /// verdict of its own.
+  bool Additional = false;
+  /// In a run over several files: a warning that the contract of this
+  /// function has no definition, shown only if no file of the run has one.
+  std::string UnlessDefined;
 };
 
+static uint64_t nanosecondsSince(std::chrono::steady_clock::time_point Start) {
+  return std::chrono::duration_cast<std::chrono::nanoseconds>(
+             std::chrono::steady_clock::now() - Start)
+      .count();
+}
+
 /// The backend a lowering reports, as lower-only names it.
 static std::string backendName(BackendKind Kind) {
   return Kind == BackendKind::CVC5        ? "cvc5"
@@ -2808,6 +2885,39 @@ class Verifier {
   std::vector<VerifyDiagnostic> Diags;
   /// What --list-functions prints: each function's location and kind.
   std::vector<std::pair<SourceLocation, std::string>> Listing;
+  /// Each contracted function's contract as written, by its identity.
+  std::map<std::string, std::string> ContractTexts;
+  /// In a run over several files: the contracts declared here without a
+  /// definition, which another file may verify, by identity, with their
+  /// names; for each proof (its place in Diags), those it rests on, through
+  /// the contracts verified here; and each contract verified here, whether
+  /// this file establishes it and on which of the others it rests.
+  std::map<std::string, std::string> Externals;
+  std::map<size_t, std::set<std::string>> ExternalOf;
+  struct DefinedContract {
+    std::string Name;
+    bool Established = false;
+    std::set<std::string> Assumes;
+  };
+  std::map<std::string, DefinedContract> DefinedContracts;
+  /// Where each function is declared, by its name, for the records of
+  /// --contracts-out.
+  std::map<std::string, SourceLocation> DeclLocOf;
+  /// Where the verification of each reported function spent its time, in
+  /// nanoseconds, and of the run, for --time-report.
+  struct FunctionTime {
+    std::string Name;
+    uint64_t Total = 0;
+    uint64_t Solving = 0;
+    uint64_t Induction = 0;
+    uint64_t Certification = 0;
+    uint64_t Confirmation = 0;
+  };
+  std::vector<FunctionTime> Timings;
+  std::chrono::steady_clock::time_point RunStart =
+      std::chrono::steady_clock::now();
+  std::optional<std::chrono::steady_clock::time_point> Converted, Verified,
+      Settled;
   std::optional<LeanProject> Lean;
   /// Where each template specialization verified is instantiated, and what
   /// it is, by its function's name.
@@ -3129,10 +3239,29 @@ class Verifier {
     for (const auto &[Loc, Message] : Converter.getWarnings())
       Diags.push_back({VerifyDiagnostic::Warning, Message, Loc});
     InstantiationPoints = Converter.getInstantiationPoints();
+    ContractTexts = Converter.getContractTexts();
     // A construct the verifier does not represent costs its function alone:
     // the function is Unresolved, its first error carrying the verdict, and
     // the rest of the translation unit is verified. An error outside every
     // function stops the run.
+    // --function: the functions the run reports, by their names.
+    std::vector<llvm::GlobPattern> Patterns;
+    for (const std::string &Text : Opts.FunctionPatterns) {
+      auto Pattern = llvm::GlobPattern::create(Text);
+      if (!Pattern) {
+        Diags.push_back(
+            {VerifyDiagnostic::Error, "--function=" + Text + ": " +
+                                          llvm::toString(Pattern.takeError())});
+        return false;
+      }
+      Patterns.push_back(std::move(*Pattern));
+    }
+    auto selects = [&](llvm::StringRef Name) {
+      return Patterns.empty() ||
+             llvm::any_of(Patterns, [&](const llvm::GlobPattern &Pattern) {
+               return Pattern.match(Name);
+             });
+    };
     bool OutsideFunctions = false;
     std::map<std::string, std::string> UnsupportedConstructs;
     for (const ConversionError &Err : Converter.getErrors()) {
@@ -3143,6 +3272,7 @@ class Verifier {
         OutsideFunctions = true;
       else
         D.FunctionName = Err.FunctionName;
+      D.Hidden = !Err.Function.empty() && !selects(Err.FunctionName);
       if (!Err.Function.empty() &&
           UnsupportedConstructs.emplace(Err.Function, Err.Message).second) {
         VerifyResult R;
@@ -3168,10 +3298,38 @@ class Verifier {
           {VerifyDiagnostic::Warning, "no verifiable functions found"});
       return true;
     }
+    Converted = std::chrono::steady_clock::now();
+    // A function is selected by the name its verdicts print, which for an
+    // inductive predicate's step is the predicate's; the predicate's rule
+    // proofs are reported with it.
+    std::vector<bool> Selected(Functions.size());
+    for (size_t I = 0; I != Functions.size(); ++I) {
+      const VFunction &Fn = *Functions[I];
+      Selected[I] =
+          selects(Fn.InductiveStepOf.empty() ? Fn.Name : Fn.InductiveStepOf);
+    }
+    std::set<std::string> SelectedIdentities;
+    for (size_t I = 0; I != Functions.size(); ++I)
+      if (Selected[I])
+        SelectedIdentities.insert(Functions[I]->Identity);
+    for (size_t I = 0; I != Functions.size(); ++I)
+      Selected[I] = Selected[I] ||
+                    SelectedIdentities.count(Functions[I]->InductiveRuleOf);
+    if (!Patterns.empty() &&
+        llvm::none_of(Selected, [](bool S) { return S; }) &&
+        llvm::none_of(Converter.getErrors(), [&](const ConversionError &Err) {
+          return !Err.Function.empty() && selects(Err.FunctionName);
+        })) {
+      Diags.push_back({VerifyDiagnostic::Error,
+                       "no function matches --function=" +
+                           llvm::join(Opts.FunctionPatterns, ", --function=")});
+      return false;
+    }
     if (Opts.ListFunctions) {
-      for (const auto &Fn : Functions) {
+      for (size_t I = 0; I != Functions.size(); ++I) {
+        const auto &Fn = Functions[I];
         if (Fn->IsBuiltin || Fn->IsChoice || !Fn->InductiveStepOf.empty() ||
-            !Fn->InductiveRuleOf.empty())
+            !Fn->InductiveRuleOf.empty() || !Selected[I])
           continue;
         const char *Kind = Fn->IsConstexprSpec ? "constexpr spec"
                            : Fn->IsSpec        ? "spec"
@@ -3250,6 +3408,7 @@ class Verifier {
     Execution.MemoryLimitMB = Opts.MemoryLimitMB;
     Execution.IntegerEncoding = Opts.IntegerEncoding;
     Execution.SkipWholeModuleRetry = !Opts.LeanFallbackProjectPath.empty();
+    Execution.MaxFailures = Opts.MaxFailures;
     Execution.CVC5Path = Opts.CVC5Path;
     Execution.ProfileQuantifiers = Opts.ProfileQuantifiers;
     Execution.ProofCachePath = Opts.ProofCachePath;
@@ -3401,6 +3560,8 @@ class Verifier {
         const VFunction *Fn;
         std::string Label;
         BackendKind Kind;
+        /// The function whose verification proposed it.
+        size_t Function;
       };
       std::vector<Confirmation> Confirmations;
       /// Certified failures a fallback project shows in Lean: each one's
@@ -3420,6 +3581,13 @@ class Verifier {
       std::string Archive;
       /// Ctrl-C came before the verification ended.
       bool Interrupted = false;
+      /// Where the verification spent its time (--time-report), in
+      /// nanoseconds: the task, its backends, the notes of its failures,
+      /// and the confirmations by proof after every task.
+      std::shared_ptr<BackendTimes> Times;
+      uint64_t Task = 0;
+      uint64_t Notes = 0;
+      uint64_t Confirmed = 0;
     };
     std::vector<FunctionRun> Runs(Functions.size());
     // The source manager caches its last line lookup.
@@ -3447,7 +3615,7 @@ class Verifier {
           Run.Confirmations.push_back({Diags.size(),
                                        std::make_shared<ObligationModule>(
                                            copyObligationModule(Checked)),
-                                       R, &In, Label, Kind});
+                                       R, &In, Label, Kind, Index});
         explainUnsettled(R, In, Checked);
       };
       // What the function's verification builds is bounded by the node
@@ -3502,6 +3670,176 @@ class Verifier {
       }
       auto SmokeBackend = createVerifyBackend(BackendKind::Z3, nullptr, 0,
                                               SmokeExecution, nullptr);
+      if (Opts.TimeReport) {
+        Run.Times = std::make_shared<BackendTimes>();
+        Backend->setTimes(Run.Times);
+        if (OwnSpecBackend)
+          OwnSpecBackend->setTimes(Run.Times);
+        SmokeBackend->setTimes(Run.Times);
+      }
+      // What else a failure shows. A counterexample that passes through a
+      // loop starts from any state the loop's invariants allow, which no
+      // execution need reach; unrolling the loops looks for an execution
+      // that fails, or proves that none does.
+      auto failureNotes = [&](const VFunction &F, const VerifyResult &Failure) {
+        std::vector<std::string> Notes;
+        auto at = [&](SourceLocation Loc) {
+          const PresumedLoc Where = Ctx.getSourceManager().getPresumedLoc(Loc);
+          return Where.isValid() ? std::to_string(Where.getLine()) + ":" +
+                                       std::to_string(Where.getColumn())
+                                 : std::string("?");
+        };
+        if (F.UnmeasuredLoop.isValid())
+          Notes.push_back("the loop at " + at(F.UnmeasuredLoop) +
+                          " has no cppverify::decreases: a proof would be "
+                          "Unresolved (decreases.missing) until it has one");
+        const auto Loop = llvm::find_if(Failure.Trace, [](const auto &Event) {
+          return Event.Kind == DiagnosticTraceKind::Loop &&
+                 Event.Active.value_or(false);
+        });
+        if (Loop == Failure.Trace.end() || !isDeductiveBackend(Opts.Backend) ||
+            Failure.Reason != VerifyReason::Counterexample)
+          return Notes;
+        Notes.push_back(
+            "the counterexample's state at the loop at " +
+            (Loop->Source.isValid() ? std::to_string(Loop->Source.Line) + ":" +
+                                          std::to_string(Loop->Source.Column)
+                                    : std::string("?")) +
+            " is any state its invariants allow, not necessarily one an "
+            "execution reaches");
+        if (Opts.ConfirmBound == 0 || !Failure.ObligationType)
+          return Notes;
+        const auto UnrollStart = std::chrono::steady_clock::now();
+        llvm::scope_exit CountUnrolling(
+            [&] { Run.Notes += nanosecondsSince(UnrollStart); });
+        VFunction Bounded = cloneVFunction(F);
+        annotatePointerOrigins(Bounded);
+        if (Opts.CheckUB && !F.TotalExpressions && instrumentUBChecks(Bounded))
+          return Notes;
+        SpecInliner(FnMap, Bounded.SpecFuel).prepareFunction(Bounded);
+        // The search after a failure takes at most one query's time.
+        Z3VerifyBackend Unroller(Execution, "bmc");
+        std::optional<std::chrono::steady_clock::time_point> Until = Deadline;
+        if (Opts.SolverTimeoutMs != 0) {
+          const auto Slice = std::chrono::steady_clock::now() +
+                             std::chrono::milliseconds(Opts.SolverTimeoutMs);
+          if (!Until || Slice < *Until)
+            Until = Slice;
+        }
+        Unroller.setDeadline(Until);
+        auto iterations = [](unsigned Bound) {
+          return std::to_string(Bound) +
+                 (Bound == 1 ? " iteration" : " iterations");
+        };
+        // Unrolling keeps the function's checks, each copied into every
+        // iteration it is in, but not the loops' invariants and measures:
+        // the copies of the failed check are those of its kind at its place.
+        auto copyOfFailure = [&](const VerifyResult &Result) {
+          return Result.ObligationType == Failure.ObligationType &&
+                 Result.Source.Line == Failure.Source.Line &&
+                 Result.Source.Column == Failure.Source.Column &&
+                 Result.Source.File == Failure.Source.File;
+        };
+        bool Unrolled = false;
+        std::string Earlier;
+        for (unsigned Bound = 0; Bound <= Opts.ConfirmBound; ++Bound) {
+          VFunction Copy = LoopUnroller::unroll(Bounded, Bound);
+          Passivizer Unrolling;
+          Unrolling.setFunctionMap(InterfaceMap);
+          auto Lowered = buildObligationModule(Unrolling.run(Copy));
+          if (!Lowered) {
+            llvm::consumeError(Lowered.takeError());
+            return Notes;
+          }
+          auto Simplified = simplifyObligationModule(std::move(*Lowered));
+          if (!Simplified) {
+            llvm::consumeError(Simplified.takeError());
+            return Notes;
+          }
+          ObligationModule Module = std::move(*Simplified);
+          Module.BMCTransform = BMCTransformProvenance{Bound};
+          annotateObligationSources(Module);
+          bool Copies = false;
+          bool CopiesHold = true;
+          bool Unwound = true;
+          // Every failure is reported, so a copy, or a loop's unwinding, is
+          // solved in the executions that pass the failing checks before it:
+          // one that fails an earlier check never reaches it. What holds
+          // past another check that fails says so.
+          std::vector<VerifyResult> Results =
+              Unroller.verifyObligations(Module, /*ReportedFailures=*/0);
+          size_t Last = 0;
+          for (size_t I = 0; I != Results.size(); ++I)
+            if (Results[I].ObligationType == ObligationKind::Unwinding ||
+                copyOfFailure(Results[I]))
+              Last = I;
+          Earlier.clear();
+          for (size_t I = 0; I != Last && Earlier.empty(); ++I)
+            if (Results[I].Status == VerifyStatus::Failed &&
+                Results[I].ObligationType &&
+                Results[I].ObligationType != ObligationKind::Unwinding &&
+                !copyOfFailure(Results[I]))
+              Earlier = std::string(" (the ") +
+                        obligationKindName(*Results[I].ObligationType) +
+                        " check at " + std::to_string(Results[I].Source.Line) +
+                        ":" + std::to_string(Results[I].Source.Column) +
+                        " fails)";
+          for (VerifyResult &Result : Results) {
+            if (Result.ObligationType == ObligationKind::Unwinding) {
+              Unwound &= Result.Status == VerifyStatus::Verified;
+              continue;
+            }
+            if (!copyOfFailure(Result))
+              continue;
+            Copies = true;
+            if (Result.Status == VerifyStatus::Failed &&
+                Result.Reason == VerifyReason::Counterexample) {
+              Notes.push_back(
+                  "an execution fails this check " +
+                  (Bound == 0
+                       ? std::string("with no iteration of any loop")
+                       : "within " + iterations(Bound) + " of each loop") +
+                  (Result.Message.empty()
+                       ? std::string()
+                       : " (counterexample: " + Result.Message + ")"));
+              return Notes;
+            }
+            CopiesHold &= Result.Status == VerifyStatus::Verified;
+          }
+          Unrolled |= Copies;
+          // Unrolled once, every loop body holds a copy of each of its
+          // checks, and a check after a loop has one from no iteration on;
+          // a failure without a copy by then is of an invariant or a
+          // measure, which unrolling drops at every bound.
+          if (Bound >= 1 && !Unrolled)
+            return Notes;
+          if (!CopiesHold)
+            return Notes;
+          if (Copies && Unwound) {
+            Notes.push_back(
+                Earlier.empty()
+                    ? "no execution fails this check: every loop ends within " +
+                          iterations(Bound) +
+                          ", and unrolling proves it there; the loops' "
+                          "invariants are too weak for an unbounded proof"
+                    : "no execution fails this check without failing an "
+                      "earlier one first" +
+                          Earlier +
+                          ": those that pass the checks before it end every "
+                          "loop within " +
+                          iterations(Bound) + ", and unrolling proves it there");
+            return Notes;
+          }
+        }
+        if (Unrolled)
+          Notes.push_back("no execution fails this check within " +
+                          iterations(Opts.ConfirmBound) + " of each loop" +
+                          (Earlier.empty()
+                               ? std::string()
+                               : " without failing an earlier one first" +
+                                     Earlier));
+        return Notes;
+      };
       Passivizer P;
       P.setFunctionMap(InterfaceMap);
       auto proves = [&](PassiveProgram Smoke) {
@@ -3701,13 +4039,16 @@ class Verifier {
             Diags.push_back({VerifyDiagnostic::Trusted,
                              Fn->Name + " (contract assumed, not verified)",
                              Fn->DeclLoc, Fn->Name});
-          else if (!Fn->UnsupportedConstruct)
+          else if (!Fn->UnsupportedConstruct && Opts.ContractsOut.empty()) {
             Diags.push_back(
                 {VerifyDiagnostic::Warning,
                  Fn->Name + " has a contract but no definition, so its callers "
                             "are not verified; mark the declaration "
                             "[[cppverify::trusted]] to assume the contract",
                  Fn->DeclLoc, Fn->Name});
+            if (Opts.CrossFile)
+              Diags.back().UnlessDefined = Fn->Identity;
+          }
           if (auto Error = InterfaceErrors.find(Fn->Identity);
               Error != InterfaceErrors.end()) {
             AllOk = false;
@@ -4712,14 +5053,24 @@ class Verifier {
                   Module, *Item, *R.Assignment, LeanModules.Specs, Pending.Why);
             Run.Refutations.push_back(std::move(Pending));
           }
-          std::string Msg = "verification failed: " + Fn->Name;
-          if (!R.ObligationId.empty())
-            Msg += " [" + R.ObligationId + "]";
-          if (!R.Message.empty())
-            Msg += " (counterexample: " + R.Message + ")";
-          Msg += backendSuffix(R);
-          Diags.push_back(
-              {VerifyDiagnostic::Error, Msg, R.Location, Fn->Name, R});
+          // The failure, and those after it --max-failures reports, each
+          // with its counterexample and notes.
+          auto failure = [&](const VerifyResult &Failure) {
+            std::string Msg = "verification failed: " + Fn->Name;
+            if (!Failure.ObligationId.empty())
+              Msg += " [" + Failure.ObligationId + "]";
+            if (!Failure.Message.empty())
+              Msg += " (counterexample: " + Failure.Message + ")";
+            Msg += backendSuffix(Failure);
+            Diags.push_back({VerifyDiagnostic::Error, Msg, Failure.Location,
+                             Fn->Name, Failure});
+            Diags.back().Notes = failureNotes(*Fn, Failure);
+          };
+          failure(R);
+          for (const VerifyResult &More : R.MoreFailures) {
+            failure(More);
+            Diags.back().Additional = true;
+          }
         } else {
           const bool FallbackExported = R.Status == VerifyStatus::Unresolved &&
                                         exportLeanFallback(Module, Fn->Name, R);
@@ -4740,15 +5091,96 @@ class Verifier {
       }
       DumpStream.flush();
     };
-    if (Parallel) {
-      TaskGroup Group(*Pool);
-      for (size_t I = 0; I != Functions.size(); ++I)
-        Group.async([&verifyFunction, I] { verifyFunction(I); });
-      Group.wait();
-    } else {
+    // With --function, the executable functions run are the selected ones
+    // and, round by round, those whose contracts a verdict of the run relies
+    // on; specs, proof functions, and generated checks always run, since any
+    // verdict may rest on their facts. Every verdict reported is then the
+    // one a run of the whole file gives.
+    std::vector<bool> Scheduled(Functions.size(), true);
+    if (!Opts.FunctionPatterns.empty())
       for (size_t I = 0; I != Functions.size(); ++I)
-        verifyFunction(I);
+        Scheduled[I] =
+            Selected[I] || Functions[I]->IsSpec || Functions[I]->IsProof;
+    std::map<std::string, size_t> IndexOf;
+    for (size_t I = 0; I != Functions.size(); ++I)
+      IndexOf.emplace(Functions[I]->Identity, I);
+    std::vector<size_t> Batch;
+    for (size_t I = 0; I != Functions.size(); ++I)
+      if (Scheduled[I])
+        Batch.push_back(I);
+    // On a terminal, a line on standard error says how many functions are
+    // done; the results follow once every verdict is settled.
+    const bool ShowProgress =
+        Opts.Progress.value_or(llvm::sys::Process::StandardErrIsDisplayed()) &&
+        Opts.Diagnostics != DiagnosticFormat::Json;
+    std::mutex ProgressLock;
+    size_t Done = 0;
+    size_t Queued = Batch.size();
+    auto runFunction = [&](size_t I) {
+      const auto Start = std::chrono::steady_clock::now();
+      verifyFunction(I);
+      Runs[I].Task = nanosecondsSince(Start);
+      if (!ShowProgress)
+        return;
+      std::lock_guard<std::mutex> Lock(ProgressLock);
+      llvm::errs() << "\r\x1b[K[" << ++Done << "/" << Queued << "] "
+                   << Functions[I]->Name;
+      llvm::errs().flush();
+    };
+    while (!Batch.empty()) {
+      if (Parallel) {
+        TaskGroup Group(*Pool);
+        for (size_t I : Batch)
+          Group.async([&runFunction, I] { runFunction(I); });
+        Group.wait();
+      } else {
+        for (size_t I : Batch)
+          runFunction(I);
+      }
+      std::vector<size_t> Next;
+      auto need = [&](const std::string &Identity) {
+        auto It = IndexOf.find(Identity);
+        if (It != IndexOf.end() && !Scheduled[It->second]) {
+          Scheduled[It->second] = true;
+          Next.push_back(It->second);
+        }
+      };
+      for (size_t I : Batch) {
+        for (const auto &[Index, Identity, Callees] : Runs[I].CallDependencies)
+          for (const std::string &Callee : Callees)
+            need(Callee);
+        for (const SpecReliance &Reliance : Runs[I].ProofDependencies)
+          for (const std::string &Callee : Reliance.Callees)
+            need(Callee);
+      }
+      llvm::sort(Next);
+      Batch = std::move(Next);
+      Queued += Batch.size();
     }
+    if (ShowProgress && Done != 0)
+      llvm::errs() << "\r\x1b[K";
+    Verified = std::chrono::steady_clock::now();
+    // The report lists the functions reported, as a run of the whole file
+    // would, with the time of the confirmations below.
+    llvm::scope_exit ReportTimes([&] {
+      if (!Opts.TimeReport)
+        return;
+      for (size_t I = 0; I != Functions.size(); ++I) {
+        const FunctionRun &Run = Runs[I];
+        const VFunction &Fn = *Functions[I];
+        if (!Scheduled[I] || !Selected[I] || !Run.Times || Fn.IsBuiltin ||
+            Fn.IsChoice)
+          continue;
+        FunctionTime Time;
+        Time.Name = Fn.Name;
+        Time.Total = Run.Task + Run.Confirmed;
+        Time.Solving = Run.Times->Solving;
+        Time.Induction = Run.Times->Induction;
+        Time.Certification = Run.Times->Certification;
+        Time.Confirmation = Run.Notes + Run.Confirmed;
+        Timings.push_back(std::move(Time));
+      }
+    });
     // A function whose verification Ctrl-C cut short is reported by one
     // line. Its verdicts stay, hidden, for what they establish: a query the
     // interrupt stopped left its verdict unresolved, and a proof found
@@ -4778,6 +5210,9 @@ class Verifier {
       for (VerifyDiagnostic &D : Run.Diags) {
         if (D.FindingOf)
           *D.FindingOf += Base;
+        // What a function --function leaves out reports stays, hidden, for
+        // what it establishes.
+        D.Hidden |= !Selected[I];
         Diags.push_back(std::move(D));
       }
       AllOk &= Run.AllOk;
@@ -5007,9 +5442,18 @@ class Verifier {
     // a demoted function no longer its contract, and an inductive predicate
     // whose rule proofs are not all established has no unfolding.
     std::set<std::string> Unestablished;
-    for (const auto &Fn : Functions)
-      if (!Fn->IsSpec && !Fn->Uninterpreted && !Fn->IsTrusted)
-        Unestablished.insert(Fn->Identity);
+    for (const auto &Fn : Functions) {
+      if (Fn->IsSpec || Fn->Uninterpreted || Fn->IsTrusted)
+        continue;
+      // In a run over several files, a contract declared here without a
+      // definition holds for now: another file may verify it.
+      if (deferredContracts() && Fn->IsExternalContract &&
+          !Fn->UnsupportedConstruct && !Fn->IsProof) {
+        Externals.emplace(Fn->Identity, Fn->Name);
+        continue;
+      }
+      Unestablished.insert(Fn->Identity);
+    }
     auto settled = [&](size_t Index) { return Diags[Index].isProof(); };
     for (const auto &[Index, Identity, Callees] : CallDependencies)
       if (settled(Index))
@@ -5376,6 +5820,44 @@ class Verifier {
           Demoted = true;
         }
     }
+    // In a run over several files, each proof rests on the contracts
+    // declared here without a definition that its callees' contracts rest
+    // on, through the contracts verified here; each contract verified here
+    // is offered to the other files with what it rests on.
+    if (deferredContracts()) {
+      std::map<std::string, std::vector<size_t>> VerdictsOf;
+      for (const auto &[Index, Identity, Callees] : CallDependencies)
+        VerdictsOf[Identity].push_back(Index);
+      for (bool Changed = true; Changed;) {
+        Changed = false;
+        for (const auto &[Index, Identity, Callees] : CallDependencies) {
+          std::set<std::string> Rests;
+          for (const std::string &Callee : Callees) {
+            if (Externals.count(Callee))
+              Rests.insert(Callee);
+            for (size_t Verdict : VerdictsOf[Callee])
+              if (auto It = ExternalOf.find(Verdict); It != ExternalOf.end())
+                Rests.insert(It->second.begin(), It->second.end());
+          }
+          std::set<std::string> &Mine = ExternalOf[Index];
+          const size_t Before = Mine.size();
+          Mine.insert(Rests.begin(), Rests.end());
+          Changed |= Mine.size() != Before;
+        }
+      }
+      for (const auto &Fn : Functions) {
+        DeclLocOf.emplace(Fn->Name, Fn->DeclLoc);
+        if (Fn->IsSpec || Fn->IsProof || Fn->IsExternalContract ||
+            Fn->Uninterpreted || !ContractTexts.count(Fn->Identity))
+          continue;
+        DefinedContract &Defined = DefinedContracts[Fn->Identity];
+        Defined.Name = Fn->Name;
+        Defined.Established = !Unestablished.count(Fn->Identity);
+        for (size_t Verdict : VerdictsOf[Fn->Identity])
+          if (auto It = ExternalOf.find(Verdict); It != ExternalOf.end())
+            Defined.Assumes.insert(It->second.begin(), It->second.end());
+      }
+    }
     // Counterexamples their checks could not evaluate are confirmed by proof
     // now that it is known which contracts are established: a confirmation
     // rests only on those, and only where the spec facts its query assumes
@@ -5389,6 +5871,7 @@ class Verifier {
           Lemmas.emplace(Functions[I]->Identity, Runs[I].Contract);
       std::vector<std::optional<VerifyResult>> Outcomes(Confirmations.size());
       std::vector<char> CutShort(Confirmations.size());
+      std::vector<uint64_t> ConfirmationTimes(Confirmations.size());
       auto confirm = [&](size_t I) {
         NodeBudget::Limit NodeLimit(Opts.MaxQueryNodes);
         const FunctionRun::Confirmation &Pending = Confirmations[I];
@@ -5412,10 +5895,12 @@ class Verifier {
           CutShort[I] = true;
           return;
         }
+        const auto Start = std::chrono::steady_clock::now();
         std::unique_ptr<VerifyBackend> By = createVerifyBackend(
             Pending.Kind, nullptr, Opts.BMCUnroll, Execution, nullptr);
         Outcomes[I] = confirmCounterexample(
             Checked, Pending.Result, InterfaceMap, *Pending.Fn, Lemmas, *By);
+        ConfirmationTimes[I] = nanosecondsSince(Start);
         CutShort[I] = !Outcomes[I] && interruptRequested();
       };
       if (Parallel) {
@@ -5427,6 +5912,8 @@ class Verifier {
         for (size_t I = 0; I != Confirmations.size(); ++I)
           confirm(I);
       }
+      for (size_t I = 0; I != Confirmations.size(); ++I)
+        Runs[Confirmations[I].Function].Confirmed += ConfirmationTimes[I];
       for (size_t I = 0; I != Confirmations.size(); ++I) {
         if (CutShort[I]) {
           VerifyDiagnostic &Verdict = Diags[Confirmations[I].Index];
@@ -5636,6 +6123,14 @@ class Verifier {
       }
     }
 
+    // A run --function narrows succeeds when what it reports does.
+    if (!Opts.FunctionPatterns.empty())
+      return llvm::none_of(Diags, [](const VerifyDiagnostic &D) {
+        return !D.Hidden && (D.K == VerifyDiagnostic::Error ||
+                             D.K == VerifyDiagnostic::Unresolved ||
+                             D.K == VerifyDiagnostic::Interrupted ||
+                             D.K == VerifyDiagnostic::BoundedSafe);
+      });
     return AllOk;
   }
 
@@ -5654,6 +6149,12 @@ class Verifier {
             ? "error"
             : "note";
     Record["message"] = jsonText(D.Message);
+    if (!D.Notes.empty()) {
+      llvm::json::Array Notes;
+      for (const std::string &Note : D.Notes)
+        Notes.push_back(jsonText(Note));
+      Record["notes"] = std::move(Notes);
+    }
     if (!D.FunctionName.empty())
       Record["function"] = jsonText(D.FunctionName);
 
@@ -5853,7 +6354,7 @@ class Verifier {
   /// verdict only when it carries one, as the first error of a function the
   /// verifier does not represent does.
   static void count(const VerifyDiagnostic &D, VerifySummary &Summary) {
-    if (D.Axiom)
+    if (D.Axiom || D.Additional)
       return;
     switch (D.K) {
     case VerifyDiagnostic::Verified:
@@ -5892,6 +6393,163 @@ class Verifier {
     }
   }
 
+  /// The time the run took to settle the verdicts after verifying.
+  void settled() { Settled = std::chrono::steady_clock::now(); }
+
+  /// Where the run spent its time: converting, verifying the functions (at
+  /// once, with several jobs), and settling the verdicts; and each reported
+  /// function, the busiest first. A function's solving includes its
+  /// inductions and certification; certification is summed over checks that
+  /// may run at once.
+  void printTimeReport(llvm::raw_ostream &OS) const {
+    if (!Converted || !Verified || !Settled)
+      return;
+    auto seconds = [](uint64_t Nanoseconds) {
+      return static_cast<double>(Nanoseconds) / 1e9;
+    };
+    auto between = [&](std::chrono::steady_clock::time_point From,
+                       std::chrono::steady_clock::time_point To) {
+      return seconds(
+          std::chrono::duration_cast<std::chrono::nanoseconds>(To - From)
+              .count());
+    };
+    std::vector<const FunctionTime *> Busiest;
+    for (const FunctionTime &Time : Timings)
+      Busiest.push_back(&Time);
+    llvm::stable_sort(Busiest,
+                      [](const FunctionTime *A, const FunctionTime *B) {
+                        return A->Total > B->Total;
+                      });
+    auto lowering = [](const FunctionTime &Time) {
+      const uint64_t Rest = Time.Solving + Time.Confirmation;
+      return Time.Total > Rest ? Time.Total - Rest : 0;
+    };
+    if (Opts.Diagnostics == DiagnosticFormat::Json) {
+      llvm::json::Object Run;
+      Run["schema"] = "cppverify.time/1";
+      Run["seconds"] =
+          llvm::json::Object{{"conversion", between(RunStart, *Converted)},
+                             {"verification", between(*Converted, *Verified)},
+                             {"settling", between(*Verified, *Settled)}};
+      OS << llvm::json::Value(std::move(Run)) << "\n";
+      for (const FunctionTime *Time : Busiest) {
+        llvm::json::Object Record;
+        Record["schema"] = "cppverify.time/1";
+        Record["function"] = Time->Name;
+        Record["seconds"] =
+            llvm::json::Object{{"total", seconds(Time->Total)},
+                               {"lowering", seconds(lowering(*Time))},
+                               {"solving", seconds(Time->Solving)},
+                               {"induction", seconds(Time->Induction)},
+                               {"certification", seconds(Time->Certification)},
+                               {"confirmation", seconds(Time->Confirmation)}};
+        OS << llvm::json::Value(std::move(Record)) << "\n";
+      }
+      return;
+    }
+    OS << llvm::formatv("Time report (seconds): conversion {0:F3}, "
+                        "verification {1:F3}, settling {2:F3}\n",
+                        between(RunStart, *Converted),
+                        between(*Converted, *Verified),
+                        between(*Verified, *Settled));
+    if (Busiest.empty())
+      return;
+    OS << "     total  lowering   solving  induction  certification  "
+          "confirmation  function\n";
+    for (const FunctionTime *Time : Busiest)
+      OS << llvm::formatv("{0,10:F3}{1,10:F3}{2,10:F3}{3,11:F3}{4,15:F3}"
+                          "{5,14:F3}  {6}\n",
+                          seconds(Time->Total), seconds(lowering(*Time)),
+                          seconds(Time->Solving), seconds(Time->Induction),
+                          seconds(Time->Certification),
+                          seconds(Time->Confirmation), Time->Name);
+  }
+
+  /// Whether \p D is reported, and so counted: a hidden one is not, nor a
+  /// generated proof that holds.
+  static bool reported(const VerifyDiagnostic &D) {
+    return !D.Hidden && !(D.Quiet && (D.K == VerifyDiagnostic::Verified ||
+                                      D.K == VerifyDiagnostic::Certified ||
+                                      D.K == VerifyDiagnostic::Exported));
+  }
+
+  /// A contract declared without a definition waits for the files verified
+  /// with this one, in one run or by checkContracts.
+  bool deferredContracts() const {
+    return Opts.CrossFile || !Opts.ContractsOut.empty();
+  }
+
+  /// For checkContracts: tags each proof that rests on contracts declared
+  /// without a definition ([assumes=...]), and writes what this file
+  /// verifies and assumes to Opts.ContractsOut.
+  bool recordContracts() {
+    auto key = [&](const std::string &Identity) {
+      auto It = ContractTexts.find(Identity);
+      return Identity + "\n" + (It != ContractTexts.end() ? It->second : "");
+    };
+    const SourceManager &SM = Ctx.getSourceManager();
+    const std::string File =
+        std::string(SM.getFileEntryRefForID(SM.getMainFileID())->getName());
+    llvm::json::Array Defined;
+    for (const auto &[Identity, Contract] : DefinedContracts) {
+      llvm::json::Array Assumes;
+      for (const std::string &Assumed : Contract.Assumes)
+        Assumes.push_back(key(Assumed));
+      Defined.push_back(
+          llvm::json::Object{{"key", key(Identity)},
+                             {"name", Contract.Name},
+                             {"established", Contract.Established},
+                             {"assumes", std::move(Assumes)}});
+    }
+    llvm::json::Array Proofs;
+    for (const auto &[Index, Assumed] : ExternalOf) {
+      VerifyDiagnostic &D = Diags[Index];
+      if (Assumed.empty() || !D.isProof())
+        continue;
+      llvm::json::Array Assumes;
+      std::string Names;
+      for (const std::string &Identity : Assumed) {
+        Assumes.push_back(llvm::json::Object{{"key", key(Identity)},
+                                             {"name", Externals.at(Identity)}});
+        Names += (Names.empty() ? "" : ",") + Externals.at(Identity);
+      }
+      D.Message += " [assumes=" + Names + "]";
+      std::string Location;
+      SourceLocation Loc = D.Loc;
+      if (Loc.isInvalid())
+        if (auto It = DeclLocOf.find(D.FunctionName); It != DeclLocOf.end())
+          Loc = It->second;
+      if (const PresumedLoc Where = SM.getPresumedLoc(Loc); Where.isValid())
+        Location = std::string(Where.getFilename()) + ":" +
+                   std::to_string(Where.getLine()) + ":" +
+                   std::to_string(Where.getColumn());
+      Proofs.push_back(llvm::json::Object{{"function", D.FunctionName},
+                                          {"location", Location},
+                                          {"assumes", std::move(Assumes)}});
+    }
+    llvm::json::Object Record{{"schema", "cppverify.contracts/1"},
+                              {"file", File},
+                              {"defined", std::move(Defined)},
+                              {"proofs", std::move(Proofs)}};
+    std::error_code EC;
+    llvm::raw_fd_ostream Out(Opts.ContractsOut, EC, llvm::sys::fs::OF_Text);
+    if (EC) {
+      Diags.push_back(
+          {VerifyDiagnostic::Error,
+           "cannot write " + Opts.ContractsOut + ": " + EC.message()});
+      return false;
+    }
+    Out << llvm::json::Value(std::move(Record)) << "\n";
+    return true;
+  }
+
+  /// Whether --quiet leaves \p D out: what needs no attention.
+  bool quieted(const VerifyDiagnostic &D) const {
+    return Opts.Quiet && (D.isProof() || D.K == VerifyDiagnostic::Lowered ||
+                          D.K == VerifyDiagnostic::Exported ||
+                          D.K == VerifyDiagnostic::Trusted);
+  }
+
   void printDiagnostics(llvm::raw_ostream &OS) const {
     for (const auto &[Loc, Line] : Listing) {
       PresumedLoc PLoc = Ctx.getSourceManager().getPresumedLoc(Loc);
@@ -5901,106 +6559,174 @@ class Verifier {
       OS << Line << "\n";
     }
     for (const auto &D : Diags) {
-      if (D.Hidden)
-        continue;
-      // A generated proof is reported only if it is not a proof.
-      if (D.Quiet && (D.K == VerifyDiagnostic::Verified ||
-                      D.K == VerifyDiagnostic::Certified ||
-                      D.K == VerifyDiagnostic::Exported))
+      if (!reported(D))
         continue;
       if (Opts.Summary)
         count(D, *Opts.Summary);
-      // --quiet leaves out what needs no attention.
-      if (Opts.Quiet && (D.isProof() || D.K == VerifyDiagnostic::Lowered ||
-                         D.K == VerifyDiagnostic::Exported ||
-                         D.K == VerifyDiagnostic::Trusted))
-        continue;
-      if (Opts.Diagnostics == DiagnosticFormat::Json) {
-        printJSONDiagnostic(D, OS);
+      if (!quieted(D))
+        printDiagnostic(D, OS);
+    }
+  }
+
+  /// In a run over several files, this file's results as they wait for every
+  /// file to be verified: each reported diagnostic as printed and counted,
+  /// and a proof that rests on contracts declared here without a definition
+  /// also as unresolved for want of one, as demote() makes it, with
+  /// ContractPlaceholder for the contract.
+  CrossFileReport renderReport(bool Ok) const {
+    CrossFileReport Report;
+    Report.Ok = Ok;
+    auto key = [&](const std::string &Identity) {
+      auto It = ContractTexts.find(Identity);
+      return Identity + "\n" + (It != ContractTexts.end() ? It->second : "");
+    };
+    for (const auto &[Identity, Defined] : DefinedContracts) {
+      CrossFileContract &Contract = Report.Defined[key(Identity)];
+      Contract.Name = Defined.Name;
+      Contract.File = std::string(
+          Ctx.getSourceManager()
+              .getFileEntryRefForID(Ctx.getSourceManager().getMainFileID())
+              ->getName());
+      Contract.Established = Defined.Established;
+      for (const std::string &Assumed : Defined.Assumes)
+        Contract.Assumes.insert(key(Assumed));
+    }
+    for (const auto &[Identity, Name] : Externals)
+      Report.Names[key(Identity)] = Name;
+    std::map<size_t, size_t> LineOf;
+    for (size_t Index = 0; Index != Diags.size(); ++Index) {
+      const VerifyDiagnostic &D = Diags[Index];
+      if (!reported(D))
         continue;
+      LineOf[Index] = Report.Lines.size();
+      CrossFileLine &Line = Report.Lines.emplace_back();
+      count(D, Line.Counts);
+      llvm::raw_string_ostream Text(Line.Text);
+      if (!quieted(D))
+        printDiagnostic(D, Text);
+      if (!D.UnlessDefined.empty())
+        Line.UnlessDefined = key(D.UnlessDefined);
+      if (D.FindingOf) {
+        if (auto It = LineOf.find(*D.FindingOf); It != LineOf.end())
+          Line.FindingOf = It->second;
+        Line.FoundAtEntry = D.FoundAtEntry;
       }
-      const std::pair<SourceLocation, std::string> *Instantiation =
-          instantiationOf(D);
-      const std::string InstantiationNote =
-          Instantiation ? "in instantiation of " + Instantiation->second +
-                              " '" + D.FunctionName + "' requested here"
-                        : std::string();
-      if (D.K == VerifyDiagnostic::Error && D.Span.isValid()) {
-        DiagnosticOptions DiagOpts;
-        DiagOpts.ShowPresumedLoc = true;
-        TextDiagnostic Text(OS, Ctx.getLangOpts(), DiagOpts);
-        Text.emitDiagnostic(
-            FullSourceLoc(D.Span.getBegin(), Ctx.getSourceManager()),
-            DiagnosticsEngine::Error, D.Message,
-            CharSourceRange::getTokenRange(D.Span), {});
-        if (Instantiation)
-          Text.emitDiagnostic(
-              FullSourceLoc(Instantiation->first, Ctx.getSourceManager()),
-              DiagnosticsEngine::Note, InstantiationNote, {}, {});
+      auto Rests = ExternalOf.find(Index);
+      if (!D.isProof() || Rests == ExternalOf.end() || Rests->second.empty())
         continue;
+      for (const std::string &Assumed : Rests->second)
+        Line.Assumes.insert(key(Assumed));
+      VerifyDiagnostic Demoted = D;
+      Demoted.K = VerifyDiagnostic::Unresolved;
+      // A callee contract enters only after the entry state.
+      if (Demoted.Vacuous && !Demoted.VacuousAtEntry) {
+        Demoted.Vacuous = false;
+        if (size_t At = Demoted.Message.find(" [vacuous]");
+            At != std::string::npos)
+          Demoted.Message.erase(At, std::strlen(" [vacuous]"));
       }
-      if (D.Loc.isValid()) {
-        PresumedLoc PLoc = Ctx.getSourceManager().getPresumedLoc(D.Loc);
-        if (PLoc.isValid())
-          OS << PLoc.getFilename() << ":" << PLoc.getLine() << ":"
-             << PLoc.getColumn() << ": ";
-      }
-      switch (D.K) {
-      case VerifyDiagnostic::Lowered:
-        OS << "Lowered: " << D.Message << "\n";
-        break;
-      case VerifyDiagnostic::Verified:
-        OS << "Verified: " << D.Message << "\n";
-        break;
-      case VerifyDiagnostic::Error:
-        OS << "error: " << D.Message << "\n";
-        break;
-      case VerifyDiagnostic::Unresolved:
-        OS << "Unresolved: " << D.Message << "\n";
-        if (D.Result)
-          for (const QuantifierProfileEntry &Entry : D.Result->QuantifierProfile)
-            OS << "note: the quantifier at " << Entry.Line << ":"
-               << Entry.Column << " was instantiated " << Entry.Instances
-               << " times, up to generation " << Entry.MaxGeneration << "\n";
-        break;
-      case VerifyDiagnostic::Interrupted:
-        OS << "Interrupted: " << D.Message << "\n";
-        break;
-      case VerifyDiagnostic::BoundedSafe:
-        OS << "BoundedSafe: " << D.Message << "\n";
-        break;
-      case VerifyDiagnostic::Exported:
-        OS << "Exported: " << D.Message;
-        if (D.LeanAutomatic && D.Result)
-          OS << " (cppverify_auto proved " << D.LeanAutomatic << " of "
-             << std::set<std::string>(D.Result->LeanGoals.begin(),
-                                      D.Result->LeanGoals.end())
-                    .size()
-             << " goals)";
-        OS << "\n";
-        break;
-      case VerifyDiagnostic::Certified:
-        OS << "Certified: " << D.Message << "\n";
-        break;
-      case VerifyDiagnostic::MixedProof:
-        OS << "Proved (" << D.Result->BackendName << "): " << D.Message << "\n";
-        break;
-      case VerifyDiagnostic::Trusted:
-        OS << "Trusted: " << D.Message << "\n";
-        break;
-      case VerifyDiagnostic::Warning:
-        OS << "warning: " << D.Message << "\n";
-        break;
-      }
-      if (Instantiation) {
-        PresumedLoc PLoc =
-            Ctx.getSourceManager().getPresumedLoc(Instantiation->first);
-        if (PLoc.isValid())
-          OS << PLoc.getFilename() << ":" << PLoc.getLine() << ":"
-             << PLoc.getColumn() << ": ";
-        OS << "note: " << InstantiationNote << "\n";
-      }
+      Demoted.Message +=
+          " [reason=" + verifyReasonCode(VerifyReason::CalleeContract).str() +
+          "] (relies on " + ContractPlaceholder.str() + ")";
+      if (!Demoted.Result)
+        Demoted.Result.emplace();
+      Demoted.Result->Status = VerifyStatus::Unresolved;
+      Demoted.Result->Reason = VerifyReason::CalleeContract;
+      count(Demoted, Line.DemotedCounts);
+      llvm::raw_string_ostream DemotedText(Line.Demoted);
+      printDiagnostic(Demoted, DemotedText);
     }
+    return Report;
+  }
+
+  void printDiagnostic(const VerifyDiagnostic &D, llvm::raw_ostream &OS) const {
+    if (Opts.Diagnostics == DiagnosticFormat::Json) {
+      printJSONDiagnostic(D, OS);
+      return;
+    }
+    const std::pair<SourceLocation, std::string> *Instantiation =
+        instantiationOf(D);
+    const std::string InstantiationNote =
+        Instantiation ? "in instantiation of " + Instantiation->second + " '" +
+                            D.FunctionName + "' requested here"
+                      : std::string();
+    if (D.K == VerifyDiagnostic::Error && D.Span.isValid()) {
+      DiagnosticOptions DiagOpts;
+      DiagOpts.ShowPresumedLoc = true;
+      TextDiagnostic Text(OS, Ctx.getLangOpts(), DiagOpts);
+      Text.emitDiagnostic(
+          FullSourceLoc(D.Span.getBegin(), Ctx.getSourceManager()),
+          DiagnosticsEngine::Error, D.Message,
+          CharSourceRange::getTokenRange(D.Span), {});
+      if (Instantiation)
+        Text.emitDiagnostic(
+            FullSourceLoc(Instantiation->first, Ctx.getSourceManager()),
+            DiagnosticsEngine::Note, InstantiationNote, {}, {});
+      return;
+    }
+    if (D.Loc.isValid()) {
+      PresumedLoc PLoc = Ctx.getSourceManager().getPresumedLoc(D.Loc);
+      if (PLoc.isValid())
+        OS << PLoc.getFilename() << ":" << PLoc.getLine() << ":"
+           << PLoc.getColumn() << ": ";
+    }
+    switch (D.K) {
+    case VerifyDiagnostic::Lowered:
+      OS << "Lowered: " << D.Message << "\n";
+      break;
+    case VerifyDiagnostic::Verified:
+      OS << "Verified: " << D.Message << "\n";
+      break;
+    case VerifyDiagnostic::Error:
+      OS << "error: " << D.Message << "\n";
+      break;
+    case VerifyDiagnostic::Unresolved:
+      OS << "Unresolved: " << D.Message << "\n";
+      if (D.Result)
+        for (const QuantifierProfileEntry &Entry : D.Result->QuantifierProfile)
+          OS << "note: the quantifier at " << Entry.Line << ":" << Entry.Column
+             << " was instantiated " << Entry.Instances
+             << " times, up to generation " << Entry.MaxGeneration << "\n";
+      break;
+    case VerifyDiagnostic::Interrupted:
+      OS << "Interrupted: " << D.Message << "\n";
+      break;
+    case VerifyDiagnostic::BoundedSafe:
+      OS << "BoundedSafe: " << D.Message << "\n";
+      break;
+    case VerifyDiagnostic::Exported:
+      OS << "Exported: " << D.Message;
+      if (D.LeanAutomatic && D.Result)
+        OS << " (cppverify_auto proved " << D.LeanAutomatic << " of "
+           << std::set<std::string>(D.Result->LeanGoals.begin(),
+                                    D.Result->LeanGoals.end())
+                  .size()
+           << " goals)";
+      OS << "\n";
+      break;
+    case VerifyDiagnostic::Certified:
+      OS << "Certified: " << D.Message << "\n";
+      break;
+    case VerifyDiagnostic::MixedProof:
+      OS << "Proved (" << D.Result->BackendName << "): " << D.Message << "\n";
+      break;
+    case VerifyDiagnostic::Trusted:
+      OS << "Trusted: " << D.Message << "\n";
+      break;
+    case VerifyDiagnostic::Warning:
+      OS << "warning: " << D.Message << "\n";
+      break;
+    }
+    if (Instantiation) {
+      PresumedLoc PLoc =
+          Ctx.getSourceManager().getPresumedLoc(Instantiation->first);
+      if (PLoc.isValid())
+        OS << PLoc.getFilename() << ":" << PLoc.getLine() << ":"
+           << PLoc.getColumn() << ": ";
+      OS << "note: " << InstantiationNote << "\n";
+    }
+    for (const std::string &Note : D.Notes)
+      OS << "note: " << Note << "\n";
   }
 };
 
@@ -6010,10 +6736,238 @@ bool verify::verifyTranslationUnit(ASTContext &Ctx, llvm::raw_ostream &OS,
                                    const VerifyOptions &Opts) {
   Verifier V(Ctx, Opts, OS);
   bool Ok = V.run();
+  V.settled();
+  if (Opts.CrossFile) {
+    CrossFileReport Report = V.renderReport(Ok);
+    llvm::raw_string_ostream Trailer(Report.Trailer);
+    if (Opts.TimeReport)
+      V.printTimeReport(Trailer);
+    Opts.CrossFile->State->Files.push_back(std::move(Report));
+    return Ok;
+  }
+  if (!Opts.ContractsOut.empty())
+    Ok = V.recordContracts() && Ok;
   V.printDiagnostics(OS);
+  if (Opts.TimeReport)
+    V.printTimeReport(OS);
   return Ok;
 }
 
+/// The contracts verified in the files of a run, or in files verified apart,
+/// settled together. A contract is established by its definitions' proofs
+/// once the contracts they rest on are, starting from none, so one that rests
+/// on itself through other files is not; a contract defined in several files
+/// (inline in a header) must hold in each.
+class ContractSettlement {
+  std::map<std::string, std::vector<CrossFileContract>> Definitions;
+  std::set<std::string> Established;
+
+  static std::string identityOf(const std::string &Key) {
+    return Key.substr(0, Key.find('\n') + 1);
+  }
+
+public:
+  void define(const std::string &Key, const CrossFileContract &Contract) {
+    Definitions[Key].push_back(Contract);
+  }
+
+  void settle() {
+    for (bool Changed = true; Changed;) {
+      Changed = false;
+      for (const auto &[Key, Contracts] : Definitions)
+        if (!Established.count(Key) &&
+            llvm::all_of(Contracts, [&](const CrossFileContract &Contract) {
+              return Contract.Established &&
+                     llvm::all_of(Contract.Assumes, [&](const std::string &K) {
+                       return Established.count(K) != 0;
+                     });
+            })) {
+          Established.insert(Key);
+          Changed = true;
+        }
+    }
+  }
+
+  bool established(const std::string &Key) const {
+    return Established.count(Key) != 0;
+  }
+
+  /// Whether some file defines the function of \p Key, whatever contract its
+  /// definition is verified against.
+  bool defined(const std::string &Key) const {
+    auto It = Definitions.lower_bound(identityOf(Key));
+    return It != Definitions.end() &&
+           llvm::StringRef(It->first).starts_with(identityOf(Key));
+  }
+
+  /// What a proof that rests on the contract of \p Key, the function \p Name,
+  /// relies on, when it is not established.
+  std::string describe(const std::string &Key, const std::string &Name) const {
+    const std::string Text = "the contract of " + Name;
+    auto Defined = Definitions.find(Key);
+    if (Defined == Definitions.end()) {
+      // A definition verified against another contract does not match.
+      for (const auto &[Other, Contracts] : Definitions)
+        if (llvm::StringRef(Other).starts_with(identityOf(Key)))
+          return Text + ", which is not established: its definition in " +
+                 Contracts.front().File +
+                 " is verified against another contract";
+      return Text + " (no definition; mark it [[cppverify::trusted]] to "
+                    "assume it), which is not established";
+    }
+    for (const CrossFileContract &Contract : Defined->second)
+      if (!Contract.Established)
+        return Text + ", which its verification in " + Contract.File +
+               " does not establish";
+    return Text + ", whose proof in " + Defined->second.front().File +
+           " rests in turn on contracts not established";
+  }
+};
+
+unsigned verify::checkContracts(const std::vector<std::string> &Paths,
+                                llvm::raw_ostream &OS) {
+  struct Proof {
+    std::string Function;
+    std::string Location;
+    std::vector<std::pair<std::string, std::string>> Assumes;
+  };
+  ContractSettlement Contracts;
+  std::vector<Proof> Proofs;
+  unsigned Errors = 0;
+  auto strings = [](const llvm::json::Array *Array) {
+    std::set<std::string> Strings;
+    if (Array)
+      for (const llvm::json::Value &Value : *Array)
+        if (std::optional<llvm::StringRef> String = Value.getAsString())
+          Strings.insert(String->str());
+    return Strings;
+  };
+  for (const std::string &Path : Paths) {
+    auto Buffer = llvm::MemoryBuffer::getFile(Path);
+    if (!Buffer) {
+      OS << "error: cannot read " << Path << ": " << Buffer.getError().message()
+         << "\n";
+      ++Errors;
+      continue;
+    }
+    llvm::Expected<llvm::json::Value> Parsed =
+        llvm::json::parse((*Buffer)->getBuffer());
+    const llvm::json::Object *Record = Parsed ? Parsed->getAsObject() : nullptr;
+    if (!Record || Record->getString("schema") != "cppverify.contracts/1") {
+      if (!Parsed)
+        llvm::consumeError(Parsed.takeError());
+      OS << "error: " << Path
+         << " is not a contracts record (cppverify.contracts/1)\n";
+      ++Errors;
+      continue;
+    }
+    const std::string File =
+        Record->getString("file").value_or(llvm::StringRef(Path)).str();
+    if (const llvm::json::Array *Defined = Record->getArray("defined"))
+      for (const llvm::json::Value &Value : *Defined) {
+        const llvm::json::Object *Entry = Value.getAsObject();
+        if (!Entry || !Entry->getString("key"))
+          continue;
+        CrossFileContract Contract;
+        Contract.Name = Entry->getString("name").value_or("").str();
+        Contract.File = File;
+        Contract.Established = Entry->getBoolean("established").value_or(false);
+        Contract.Assumes = strings(Entry->getArray("assumes"));
+        Contracts.define(Entry->getString("key")->str(), Contract);
+      }
+    if (const llvm::json::Array *Rests = Record->getArray("proofs"))
+      for (const llvm::json::Value &Value : *Rests) {
+        const llvm::json::Object *Entry = Value.getAsObject();
+        if (!Entry)
+          continue;
+        Proof &P = Proofs.emplace_back();
+        P.Function = Entry->getString("function").value_or("").str();
+        P.Location = Entry->getString("location").value_or("").str();
+        if (const llvm::json::Array *Assumes = Entry->getArray("assumes"))
+          for (const llvm::json::Value &Assumed : *Assumes)
+            if (const llvm::json::Object *Contract = Assumed.getAsObject())
+              P.Assumes.emplace_back(
+                  Contract->getString("key").value_or("").str(),
+                  Contract->getString("name").value_or("").str());
+      }
+  }
+  Contracts.settle();
+  unsigned Unsettled = 0;
+  for (const Proof &P : Proofs) {
+    std::string Missing;
+    for (const auto &[Key, Name] : P.Assumes)
+      if (!Contracts.established(Key))
+        Missing +=
+            (Missing.empty() ? "" : "; ") + Contracts.describe(Key, Name);
+    if (Missing.empty())
+      continue;
+    ++Unsettled;
+    if (!P.Location.empty())
+      OS << P.Location << ": ";
+    OS << "error: the proof of " << P.Function << " relies on " << Missing
+       << "\n";
+  }
+  OS << "Contracts: " << Proofs.size()
+     << (Proofs.size() == 1 ? " proof rests" : " proofs rest")
+     << " on contracts of other files, " << Unsettled << " on one not "
+     << "established\n";
+  return Errors + Unsettled;
+}
+
+unsigned CrossFileRun::finish(llvm::raw_ostream &OS, VerifySummary *Summary) {
+  ContractSettlement Contracts;
+  for (const CrossFileReport &File : State->Files)
+    for (const auto &[Key, Contract] : File.Defined)
+      Contracts.define(Key, Contract);
+  Contracts.settle();
+  auto describe = [&](const CrossFileReport &File, const std::string &Key) {
+    auto Name = File.Names.find(Key);
+    return Contracts.describe(Key, Name != File.Names.end()
+                                       ? Name->second
+                                       : Key.substr(0, Key.find('\n')));
+  };
+  unsigned Failures = 0;
+  for (const CrossFileReport &File : State->Files) {
+    std::vector<bool> Demoted(File.Lines.size());
+    for (size_t I = 0; I != File.Lines.size(); ++I)
+      for (const std::string &Key : File.Lines[I].Assumes)
+        if (!Contracts.established(Key)) {
+          Demoted[I] = true;
+          break;
+        }
+    bool Ok = File.Ok;
+    for (size_t I = 0; I != File.Lines.size(); ++I) {
+      const CrossFileLine &Line = File.Lines[I];
+      if (!Line.UnlessDefined.empty() && Contracts.defined(Line.UnlessDefined))
+        continue;
+      // A finding rests on the facts of its query, as its proof does.
+      if (Line.FindingOf && Demoted[*Line.FindingOf] && !Line.FoundAtEntry)
+        continue;
+      if (!Demoted[I]) {
+        OS << Line.Text;
+        if (Summary)
+          addSummary(*Summary, Line.Counts);
+        continue;
+      }
+      Ok = false;
+      std::string Missing;
+      for (const std::string &Key : Line.Assumes)
+        if (!Contracts.established(Key))
+          Missing += (Missing.empty() ? "" : "; ") + describe(File, Key);
+      std::string Text = Line.Demoted;
+      for (size_t At = Text.find(ContractPlaceholder); At != std::string::npos;
+           At = Text.find(ContractPlaceholder, At + Missing.size()))
+        Text.replace(At, ContractPlaceholder.size(), Missing);
+      OS << Text;
+      if (Summary)
+        addSummary(*Summary, Line.DemotedCounts);
+    }
+    OS << File.Trailer;
+    Failures += !Ok;
+  }
+  return Failures;
+}
+
 LeanProjectReplay
 verify::replayLeanProject(const std::vector<ObligationModule> &Modules,
                           const VerifyOptions &Opts) {
diff --git a/clang/lib/Verify/Driver/Verifier.h b/clang/lib/Verify/Driver/Verifier.h
index 258d13892b..01a0477cf8 100644
--- a/clang/lib/Verify/Driver/Verifier.h
+++ b/clang/lib/Verify/Driver/Verifier.h
@@ -5,7 +5,9 @@
 #include "../Backend/VerifyBackend.h"
 #include "llvm/Support/raw_ostream.h"
 #include <map>
+#include <memory>
 #include <string>
+#include <vector>
 
 namespace clang {
 class ASTContext;
@@ -120,10 +122,66 @@ struct VerifyOptions {
   bool Verbose = false;
   /// List the functions the run would verify, and verify none.
   bool ListFunctions = false;
+  /// Report where each function's verification spent its time.
+  bool TimeReport = false;
+  /// Show which functions are done on standard error as they finish; unset,
+  /// when standard error is a terminal.
+  std::optional<bool> Progress;
+  /// How many failing obligations of a function are reported, each with its
+  /// own counterexample (Z3 only); 0 reports every one.
+  unsigned MaxFailures = 1;
+  /// Glob patterns over function names: only the functions they match are
+  /// reported. Empty: every function.
+  std::vector<std::string> FunctionPatterns;
+  /// For a failure whose counterexample passes through a loop, the most
+  /// iterations of each loop that unrolling may try to find an execution
+  /// that fails (0: do not try).
+  unsigned ConfirmBound = 10;
   /// Where the run counts the verdicts it prints, if anywhere.
   VerifySummary *Summary = nullptr;
+  /// A run over several files, which holds each file's results until every
+  /// file is verified (see CrossFileRun), or null.
+  class CrossFileRun *CrossFile = nullptr;
+  /// Where to write the contracts this file verifies and those it assumes
+  /// from other files, for checkContracts. With it, a contract declared
+  /// 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;
 };
 
+/// One run over several files. A contract that a file declares without a
+/// definition may be defined and verified in another file of the run, so a
+/// proof that rests on it waits: each file's results are kept, and once
+/// every file is verified, a proof stands where every such contract it rests
+/// on is established by its definition's verification, and is otherwise
+/// unresolved (callee.contract), as within one file.
+class CrossFileRun {
+public:
+  CrossFileRun();
+  ~CrossFileRun();
+  CrossFileRun(const CrossFileRun &) = delete;
+  CrossFileRun &operator=(const CrossFileRun &) = delete;
+
+  /// Settles the contracts the files assume against those they verify,
+  /// prints each file's results in the order the files were verified, and
+  /// counts them into \p Summary when it is given. Returns how many files
+  /// do not succeed.
+  unsigned finish(llvm::raw_ostream &OS, VerifySummary *Summary);
+
+  struct Impl;
+  std::unique_ptr<Impl> State;
+};
+
+/// The check of files verified apart (their ContractsOut records): every
+/// contract a file assumes must be established by the verification of its
+/// definition in another file. Prints each proof that rests on one that is
+/// not, and returns how many.
+unsigned checkContracts(const std::vector<std::string> &Paths,
+                        llvm::raw_ostream &OS);
+
+/// Verifies the translation unit. In a run over several files
+/// (Opts.CrossFile), the results wait for CrossFileRun::finish, and the
+/// result is the file's as far as it alone decides.
 bool verifyTranslationUnit(ASTContext &Ctx, llvm::raw_ostream &OS,
                            const VerifyOptions &Opts = VerifyOptions());
 
diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp
index f4a41723d3..7da19f9b3e 100644
--- a/clang/lib/Verify/Frontend/ASTConverter.cpp
+++ b/clang/lib/Verify/Frontend/ASTConverter.cpp
@@ -977,6 +977,38 @@ static std::string functionName(const FunctionDecl *FD,
   return Name;
 }
 
+std::string ASTConverter::contractText(const FunctionContractInfo &FCI) const {
+  std::string Text;
+  llvm::raw_string_ostream OS(Text);
+  const PrintingPolicy Policy(Ctx.getLangOpts());
+  auto clause = [&](llvm::StringRef Kind, const Expr *E) {
+    OS << Kind << '(';
+    if (E)
+      E->printPretty(OS, nullptr, Policy);
+    OS << ')';
+  };
+  for (const Expr *Pre : FCI.Preconditions)
+    clause("pre", Pre);
+  for (const Expr *Post : FCI.Postconditions)
+    clause("post", Post);
+  for (const Expr *Footprint : FCI.Modifies)
+    clause("modifies", Footprint);
+  for (const auto &[First, Second] : FCI.Aliases) {
+    clause("aliases", First);
+    clause("with", Second);
+  }
+  for (const Expr *Measure : FCI.Decreases)
+    clause("decreases", Measure);
+  if (FCI.MayDiverge.isValid())
+    OS << "decreases(*)";
+  for (const auto &[Name, Assumes] : FCI.Behaviors)
+    clause(std::string("behavior ") + (Name ? Name->getName().str() : ""),
+           Assumes);
+  for (const Expr *Check : FCI.BehaviorChecks)
+    clause("behaviors", Check);
+  return Text;
+}
+
 std::string ASTConverter::functionIdentity(const FunctionDecl *FD) {
   if (!FD)
     return {};
@@ -3263,6 +3295,7 @@ ASTConverter::convertFunction(const FunctionDecl *FD) {
   Fn->IsConstructor = Constructor != nullptr;
   Fn->Name = functionName(FD, /*Qualified=*/Method != nullptr);
   Fn->Identity = functionIdentity(FD);
+  ContractTexts[Fn->Identity] = contractText(*FCI);
   Fn->IsSpec = FCI->IsSpec;
   Fn->IsProof = FCI->IsProof;
   if (FCI->MayDiverge.isValid() && !FCI->IsSpec && !FCI->IsProof) {
@@ -3271,10 +3304,20 @@ ASTConverter::convertFunction(const FunctionDecl *FD) {
   }
   Fn->ReadsHeap = FCI->IsSpec && specReadsHeap(FD);
   Fn->DeclLoc = FD->getLocation();
-  Fn->IsTrusted = llvm::any_of(FD->redecls(), [](const FunctionDecl *D) {
-    return D->hasAttr<CppVerifyTrustedAttr>();
-  });
-  if (Fn->IsTrusted && Fn->IsSpec) {
+  // [[cppverify::trusted]] on a definition leaves its body unverified; on a
+  // declaration it says that callers which see no definition assume the
+  // contract, so a definition that only inherits it is verified.
+  const bool AnyTrusted =
+      llvm::any_of(FD->redecls(), [](const FunctionDecl *D) {
+        return D->hasAttr<CppVerifyTrustedAttr>();
+      });
+  if (const FunctionDecl *Definition = FD->getDefinition()) {
+    const auto *Trusted = Definition->getAttr<CppVerifyTrustedAttr>();
+    Fn->IsTrusted = Trusted && !Trusted->isInherited();
+  } else {
+    Fn->IsTrusted = AnyTrusted;
+  }
+  if (AnyTrusted && Fn->IsSpec) {
     error(Fn->Name + ": [[cppverify::trusted]] does not apply to a "
                      "spec function, whose definition is its "
                      "meaning");
diff --git a/clang/lib/Verify/Frontend/ASTConverter.h b/clang/lib/Verify/Frontend/ASTConverter.h
index d83dc0a171..dfc350c871 100644
--- a/clang/lib/Verify/Frontend/ASTConverter.h
+++ b/clang/lib/Verify/Frontend/ASTConverter.h
@@ -93,6 +93,7 @@ class ASTConverter {
   void nameParameters(const FunctionDecl *ContractDecl, const FunctionDecl *FD);
   unsigned BoundValueId = 0;
   std::map<const FunctionDecl *, std::string> FunctionIdentities;
+  std::map<std::string, std::string> ContractTexts;
   std::map<const FunctionDecl *, bool> SpecHeapReads;
   /// Uncontracted constexpr functions the lowered code calls or names.
   std::set<const FunctionDecl *> UsedConstexprSpecs;
@@ -175,6 +176,11 @@ class ASTConverter {
   getInstantiationPoints() const {
     return InstantiationPoints;
   }
+  /// For each contracted function, by its identity: its contract as written,
+  /// which another file's declaration of it must state the same.
+  const std::map<std::string, std::string> &getContractTexts() const {
+    return ContractTexts;
+  }
 
 private:
   /// Contract arithmetic is mathematical, as in ACSL and Verus spec code: an
@@ -472,6 +478,8 @@ class ASTConverter {
   bool calleeReturnsFreshOwned(const FunctionDecl *FD);
   VIntMode specCallIntMode(const FunctionDecl *FD) const;
   std::string functionIdentity(const FunctionDecl *FD);
+  /// The clauses of a contract as written, each kind tagged.
+  std::string contractText(const FunctionContractInfo &FCI) const;
   std::string specIdentityFromExpr(const Expr *E);
   void injectTypeInvariants(const FunctionDecl *FD, VFunction &Fn);
   std::unique_ptr<VExpr> convertTypeInvariantExpr(const Expr *E);
diff --git a/clang/test/Verify/suite/Inputs/across/include/mathx.h b/clang/test/Verify/suite/Inputs/across/include/mathx.h
new file mode 100644
index 0000000000..d688ecc585
--- /dev/null
+++ b/clang/test/Verify/suite/Inputs/across/include/mathx.h
@@ -0,0 +1,2 @@
+int clamp100(int x)
+  cppverify::post(cppverify::result >= 0 && cppverify::result <= 100);
diff --git a/clang/test/Verify/suite/Inputs/across/src/a.cpp b/clang/test/Verify/suite/Inputs/across/src/a.cpp
new file mode 100644
index 0000000000..ed53d64b88
--- /dev/null
+++ b/clang/test/Verify/suite/Inputs/across/src/a.cpp
@@ -0,0 +1,13 @@
+#include "mathx.h"
+
+int scaled(int x)
+  cppverify::post(cppverify::result >= 0 && cppverify::result <= 200)
+{
+  return 2 * clamp100(x);
+}
+
+int twice_scaled(int x)
+  cppverify::post(cppverify::result >= 0 && cppverify::result <= 400)
+{
+  return 2 * scaled(x);
+}
diff --git a/clang/test/Verify/suite/Inputs/across/src/mathx.cpp b/clang/test/Verify/suite/Inputs/across/src/mathx.cpp
new file mode 100644
index 0000000000..c00f5a85d5
--- /dev/null
+++ b/clang/test/Verify/suite/Inputs/across/src/mathx.cpp
@@ -0,0 +1,11 @@
+#include "mathx.h"
+
+// BUG is 100, or 101 for a definition that breaks its contract.
+int clamp100(int x)
+{
+  if (x < 0)
+    return 0;
+  if (x > 100)
+    return BUG;
+  return x;
+}
diff --git a/clang/test/Verify/suite/Inputs/across/src/other.cpp b/clang/test/Verify/suite/Inputs/across/src/other.cpp
new file mode 100644
index 0000000000..854852ff92
--- /dev/null
+++ b/clang/test/Verify/suite/Inputs/across/src/other.cpp
@@ -0,0 +1,10 @@
+// A declaration that states another contract than the one mathx.cpp's
+// definition is verified against.
+int clamp100(int x)
+  cppverify::post(cppverify::result >= 0 && cppverify::result <= 50);
+
+int halved(int x)
+  cppverify::post(cppverify::result >= 0 && cppverify::result <= 50)
+{
+  return clamp100(x);
+}
diff --git a/clang/test/Verify/suite/Inputs/across/src/ping.cpp b/clang/test/Verify/suite/Inputs/across/src/ping.cpp
new file mode 100644
index 0000000000..a248efe3bf
--- /dev/null
+++ b/clang/test/Verify/suite/Inputs/across/src/ping.cpp
@@ -0,0 +1,10 @@
+int pong(int n)
+  cppverify::pre(n >= 0 && n < 1000)
+  cppverify::post(cppverify::result == 0);
+
+int ping(int n)
+  cppverify::pre(n >= 0 && n < 1000)
+  cppverify::post(cppverify::result == 0)
+{
+  return n == 0 ? 0 : pong(n - 1);
+}
diff --git a/clang/test/Verify/suite/Inputs/across/src/pong.cpp b/clang/test/Verify/suite/Inputs/across/src/pong.cpp
new file mode 100644
index 0000000000..2159e5b02a
--- /dev/null
+++ b/clang/test/Verify/suite/Inputs/across/src/pong.cpp
@@ -0,0 +1,10 @@
+int ping(int n)
+  cppverify::pre(n >= 0 && n < 1000)
+  cppverify::post(cppverify::result == 0);
+
+int pong(int n)
+  cppverify::pre(n >= 0 && n < 1000)
+  cppverify::post(cppverify::result == 0)
+{
+  return n == 0 ? 0 : ping(n - 1);
+}
diff --git a/clang/test/Verify/suite/Inputs/time_report_phases.py b/clang/test/Verify/suite/Inputs/time_report_phases.py
new file mode 100644
index 0000000000..57d2ecf311
--- /dev/null
+++ b/clang/test/Verify/suite/Inputs/time_report_phases.py
@@ -0,0 +1,29 @@
+"""Reads the JSON Lines of a run with --time-report and prints, for each
+function, which phases took any time, and whether its times add up: the
+total is lowering, solving, and confirmation; induction is part of solving;
+and with one job, so is certification. Then whether the functions come
+busiest first."""
+import json
+import sys
+
+totals = []
+for line in sys.stdin:
+    record = json.loads(line)
+    if record.get("schema") != "cppverify.time/1":
+        continue
+    seconds = record["seconds"]
+    if "function" not in record:
+        print("run " + " ".join(sorted(seconds)))
+        continue
+    totals.append(seconds["total"])
+    parts = seconds["lowering"] + seconds["solving"] + seconds["confirmation"]
+    adds_up = (abs(seconds["total"] - parts) < 1e-6 and
+               seconds["lowering"] >= 0 and
+               seconds["induction"] <= seconds["solving"] and
+               seconds["certification"] <= seconds["solving"])
+    print("%s solving=%d induction=%d certification=%d confirmation=%d %s" % (
+        record["function"], seconds["solving"] > 0, seconds["induction"] > 0,
+        seconds["certification"] > 0, seconds["confirmation"] > 0,
+        "adds up" if adds_up else "does not add up: %r" % seconds))
+print("busiest first" if totals == sorted(totals, reverse=True)
+      else "not busiest first: %r" % totals)
diff --git a/clang/test/Verify/suite/Inputs/time_report_wrong.cpp b/clang/test/Verify/suite/Inputs/time_report_wrong.cpp
new file mode 100644
index 0000000000..eb9a22cb46
--- /dev/null
+++ b/clang/test/Verify/suite/Inputs/time_report_wrong.cpp
@@ -0,0 +1,14 @@
+namespace cv = cppverify;
+
+int wrong(int x)
+  cv::pre(x < 100)
+  cv::post(cv::result == x)
+{
+  return x + 1;
+}
+
+cv::spec int count(int n)
+  cv::decreases(n)
+{
+  return n <= 0 ? 0 : count(n - 1) + 1;
+}
diff --git a/clang/test/Verify/suite/confirmation_invariants.cpp b/clang/test/Verify/suite/confirmation_invariants.cpp
new file mode 100644
index 0000000000..6900c3ccc6
--- /dev/null
+++ b/clang/test/Verify/suite/confirmation_invariants.cpp
@@ -0,0 +1,34 @@
+// RUN: not %cpp-verify --jobs=4 --timeout=5000 --time-report %s -- 2>&1 | FileCheck %s
+//
+// Unrolling drops the loops' invariants and measures, so a failure of one
+// has no copy at any bound: once the loops are unrolled once and no copy
+// has appeared, the search for an execution that fails it stops, instead of
+// solving every check at every bound until its time runs out (5.8 s at
+// --timeout=5000 for this function, 30 s at the default 30000).
+
+namespace cv = cppverify;
+
+cv::spec bool valid(const int *p, int n) { return true; }
+
+// The copy is right; the first invariant's bound on i is not, and only an
+// invariant states it.
+void bounded_copy(const int *a, int *out, int n)
+  cv::pre(n >= 0 && valid(a, n) && valid(out, n))
+  cv::modifies(*out)
+  cv::post(cv::forall(i, 0, n, out[i] == a[i]))
+{
+  int i = 0;
+  while (i < n)
+    cv::invariant(0 <= i && i <= n && i <= 8)
+    cv::invariant(cv::forall(j, 0, i, out[j] == a[j]))
+    cv::decreases(n - i)
+  {
+    out[i] = a[i];
+    i = i + 1;
+  }
+}
+// CHECK: verification failed: bounded_copy {{.*}}invariant-preserved
+// CHECK: note: the counterexample's state at the loop at {{[0-9]+}}:3 is any state its invariants allow
+// CHECK-NOT: fails this check
+// CHECK: total  lowering   solving  induction  certification  confirmation  function
+// CHECK-NEXT: {{ *[0-9.]+ +[0-9.]+ +[0-9.]+ +[0-9.]+ +[0-9.]+ +0\.[0-9]+}}  bounded_copy
diff --git a/clang/test/Verify/suite/contracts_across_files.test b/clang/test/Verify/suite/contracts_across_files.test
new file mode 100644
index 0000000000..05e410f9e0
--- /dev/null
+++ b/clang/test/Verify/suite/contracts_across_files.test
@@ -0,0 +1,55 @@
+# One run over several files settles a contract that a file declares without
+# a definition against the verification of its definition in another file:
+# a proof that rests on it stands where that verification establishes it,
+# and is unresolved (callee.contract) where it does not, as within one file.
+#
+# RUN: %cpp-verify --jobs=1 %S/Inputs/across/src/a.cpp %S/Inputs/across/src/mathx.cpp \
+# RUN:   -- -I%S/Inputs/across/include -DBUG=100 2>&1 \
+# RUN:   | FileCheck %s --check-prefix=RIGHT --implicit-check-not=warning:
+# RUN: not %cpp-verify --jobs=1 %S/Inputs/across/src/a.cpp %S/Inputs/across/src/mathx.cpp \
+# RUN:   -- -I%S/Inputs/across/include -DBUG=101 2>&1 \
+# RUN:   | FileCheck %s --check-prefix=WRONG --implicit-check-not=warning:
+# RUN: not %cpp-verify --jobs=1 %S/Inputs/across/src/mathx.cpp %S/Inputs/across/src/a.cpp \
+# RUN:   -- -I%S/Inputs/across/include -DBUG=101 2>&1 \
+# RUN:   | FileCheck %s --check-prefix=ORDER
+# RUN: not %cpp-verify --jobs=1 --diagnostics-format=json %S/Inputs/across/src/a.cpp \
+# RUN:   %S/Inputs/across/src/mathx.cpp -- -I%S/Inputs/across/include -DBUG=101 \
+# RUN:   2>/dev/null | FileCheck %s --check-prefix=JSON
+# RUN: not %cpp-verify --jobs=1 %S/Inputs/across/src/a.cpp -- -I%S/Inputs/across/include \
+# RUN:   2>&1 | FileCheck %s --check-prefix=ALONE
+# RUN: not %cpp-verify --jobs=1 %S/Inputs/across/src/other.cpp %S/Inputs/across/src/mathx.cpp \
+# RUN:   -- -I%S/Inputs/across/include -DBUG=100 2>&1 \
+# RUN:   | FileCheck %s --check-prefix=OTHER --implicit-check-not=warning:
+# RUN: not %cpp-verify --jobs=1 %S/Inputs/across/src/ping.cpp %S/Inputs/across/src/pong.cpp \
+# RUN:   -- 2>&1 | FileCheck %s --check-prefix=CYCLE
+
+RIGHT: Verified: scaled [backend=z3]
+RIGHT-NEXT: Verified: twice_scaled [backend=z3]
+RIGHT-NEXT: Verified: clamp100 [backend=z3]
+RIGHT-NEXT: Summary: 3 verified
+
+WRONG: Unresolved: scaled [backend=z3] [reason=callee.contract] (relies on the contract of clamp100, which its verification in {{.*}}mathx.cpp does not establish)
+WRONG-NEXT: Unresolved: twice_scaled [backend=z3] [reason=callee.contract] (relies on the contract of clamp100, which its verification in {{.*}}mathx.cpp does not establish)
+WRONG-NEXT: mathx.h:2:42: error: verification failed: clamp100 [{{.*}}::postcondition@2:42] (counterexample: {{.*}}result [ssa=__result_1] [type=i32] = 101
+WRONG: Summary: 1 failed, 2 unresolved (callee.contract 2)
+
+The files are printed in the order they are given, settled together.
+ORDER: mathx.h:2:42: error: verification failed: clamp100
+ORDER: Unresolved: scaled [backend=z3] [reason=callee.contract] (relies on the contract of clamp100, which its verification in {{.*}}mathx.cpp does not establish)
+ORDER: Summary: 1 failed, 2 unresolved (callee.contract 2)
+
+JSON: {"backend":"z3","function":"scaled","message":"scaled [backend=z3] [reason=callee.contract] (relies on the contract of clamp100, which its verification in {{.*}}mathx.cpp does not establish)","reason":"callee.contract",{{.*}}"status":"unresolved"}
+JSON: "function":"clamp100","message":"verification failed: clamp100
+
+A file alone is as before: the contract has no definition.
+ALONE: mathx.h:1:5: warning: clamp100 has a contract but no definition, so its callers are not verified; mark the declaration {{\[\[cppverify::trusted\]\]}} to assume the contract
+ALONE-NEXT: Unresolved: scaled [backend=z3] [reason=callee.contract] (relies on the contract of clamp100 (no definition; mark it {{\[\[cppverify::trusted\]\]}} to assume it), which is not established)
+ALONE-NEXT: Unresolved: twice_scaled [backend=z3] [reason=callee.contract] (relies on the contract of scaled, which is not established)
+
+A declaration that states another contract is not the definition's.
+OTHER: Unresolved: halved [backend=z3] [reason=callee.contract] (relies on the contract of clamp100, which is not established: its definition in {{.*}}mathx.cpp is verified against another contract)
+OTHER-NEXT: Verified: clamp100 [backend=z3]
+
+Contracts whose proofs rest on each other through files establish nothing.
+CYCLE: Unresolved: ping [backend=z3] [reason=callee.contract] (relies on the contract of pong, whose proof in {{.*}}pong.cpp rests in turn on contracts not established)
+CYCLE-NEXT: Unresolved: pong [backend=z3] [reason=callee.contract] (relies on the contract of ping, whose proof in {{.*}}ping.cpp rests in turn on contracts not established)
diff --git a/clang/test/Verify/suite/contracts_link_check.test b/clang/test/Verify/suite/contracts_link_check.test
new file mode 100644
index 0000000000..db269ac4ee
--- /dev/null
+++ b/clang/test/Verify/suite/contracts_link_check.test
@@ -0,0 +1,61 @@
+# Files verified apart (separate cpp-verify runs, or clang++ compiling each
+# object) record the contracts they verify and those they assume from other
+# files; --check-contracts settles them together, as one run over the files
+# does, and fails for each proof whose assumed contract is not established.
+#
+# RUN: rm -rf %t && mkdir -p %t
+# RUN: %cpp-verify --jobs=1 --contracts-out=%t/a.json %S/Inputs/across/src/a.cpp \
+# RUN:   -- -I%S/Inputs/across/include 2>&1 | FileCheck %s --check-prefix=APART --implicit-check-not=warning:
+# RUN: not %cpp-verify --jobs=1 --contracts-out=%t/wrong.json %S/Inputs/across/src/mathx.cpp \
+# RUN:   -- -I%S/Inputs/across/include -DBUG=101 > /dev/null 2>&1
+# RUN: %cpp-verify --jobs=1 --contracts-out=%t/right.json %S/Inputs/across/src/mathx.cpp \
+# RUN:   -- -I%S/Inputs/across/include -DBUG=100 > /dev/null 2>&1
+# RUN: not %cpp-verify --check-contracts %t/a.json %t/wrong.json 2>&1 \
+# RUN:   | FileCheck %s --check-prefix=WRONG
+# RUN: %cpp-verify --check-contracts %t/a.json %t/right.json 2>&1 \
+# RUN:   | FileCheck %s --check-prefix=RIGHT
+# RUN: not %cpp-verify --check-contracts %t/a.json 2>&1 \
+# RUN:   | FileCheck %s --check-prefix=MISSING
+#
+# Through the compiler, each object's record beside it.
+# RUN: %clang -std=c++17 -fverify-contracts -fverify-contracts-out=%t/a.o.cppverify \
+# RUN:   -c %S/Inputs/across/src/a.cpp -o %t/a.o -I%S/Inputs/across/include 2>&1 \
+# RUN:   | FileCheck %s --check-prefix=APART
+# RUN: %clang -std=c++17 -fverify-contracts -fverify-contracts-out=%t/m.o.cppverify \
+# RUN:   -c %S/Inputs/across/src/mathx.cpp -o %t/m.o -I%S/Inputs/across/include -DBUG=100
+# RUN: %cpp-verify --check-contracts %t/a.o.cppverify %t/m.o.cppverify 2>&1 \
+# RUN:   | FileCheck %s --check-prefix=RIGHT
+# RUN: not %clang -std=c++17 -fverify-contracts -fverify-contracts-out=%t/w.o.cppverify \
+# RUN:   -c %S/Inputs/across/src/mathx.cpp -o %t/w.o -I%S/Inputs/across/include -DBUG=101 > /dev/null 2>&1
+# RUN: not %cpp-verify --check-contracts %t/a.o.cppverify %t/w.o.cppverify 2>&1 \
+# RUN:   | FileCheck %s --check-prefix=WRONG
+#
+# Contracts whose proofs rest on each other establish nothing.
+# RUN: %cpp-verify --jobs=1 --contracts-out=%t/ping.json %S/Inputs/across/src/ping.cpp -- > /dev/null 2>&1
+# RUN: %cpp-verify --jobs=1 --contracts-out=%t/pong.json %S/Inputs/across/src/pong.cpp -- > /dev/null 2>&1
+# RUN: not %cpp-verify --check-contracts %t/ping.json %t/pong.json 2>&1 \
+# RUN:   | FileCheck %s --check-prefix=CYCLE
+#
+# RUN: not %cpp-verify --check-contracts %S/Inputs/across/src/a.cpp 2>&1 \
+# RUN:   | FileCheck %s --check-prefix=NOT-RECORD
+# RUN: not %cpp-verify --contracts-out=%t/both.json %S/Inputs/across/src/a.cpp \
+# RUN:   %S/Inputs/across/src/mathx.cpp -- 2>&1 | FileCheck %s --check-prefix=SEVERAL
+
+A proof that rests on a contract of another file says so.
+APART: Verified: scaled [backend=z3] [assumes=clamp100]
+APART-NEXT: Verified: twice_scaled [backend=z3] [assumes=clamp100]
+
+WRONG: a.cpp:3:5: error: the proof of scaled relies on the contract of clamp100, which its verification in {{.*}}mathx.cpp does not establish
+WRONG-NEXT: a.cpp:9:5: error: the proof of twice_scaled relies on the contract of clamp100, which its verification in {{.*}}mathx.cpp does not establish
+WRONG-NEXT: Contracts: 2 proofs rest on contracts of other files, 2 on one not established
+
+RIGHT: Contracts: 2 proofs rest on contracts of other files, 0 on one not established
+
+MISSING: a.cpp:3:5: error: the proof of scaled relies on the contract of clamp100 (no definition; mark it {{\[\[cppverify::trusted\]\]}} to assume it), which is not established
+
+CYCLE: ping.cpp:5:5: error: the proof of ping relies on the contract of pong, whose proof in {{.*}}pong.cpp rests in turn on contracts not established
+CYCLE-NEXT: pong.cpp:5:5: error: the proof of pong relies on the contract of ping, whose proof in {{.*}}ping.cpp rests in turn on contracts not established
+
+NOT-RECORD: error: {{.*}}a.cpp is not a contracts record (cppverify.contracts/1)
+
+SEVERAL: error: --contracts-out records one file; a run over several files settles their contracts itself
diff --git a/clang/test/Verify/suite/function_filter.cpp b/clang/test/Verify/suite/function_filter.cpp
new file mode 100644
index 0000000000..91da544d7e
--- /dev/null
+++ b/clang/test/Verify/suite/function_filter.cpp
@@ -0,0 +1,150 @@
+// RUN: not %cpp-verify --jobs=1 %s -- 2>&1 | FileCheck %s --check-prefix=ALL
+// RUN: not %cpp-verify --jobs=1 --function=uses_wrong %s -- 2>&1 | FileCheck %s --check-prefix=ONE --implicit-check-not=Verified --implicit-check-not=error:
+// RUN: %cpp-verify --jobs=1 --function='add_*' %s -- 2>&1 | FileCheck %s --check-prefix=GLOB --implicit-check-not=uses_ --implicit-check-not=error:
+// RUN: rm -f %t.cpv
+// RUN: not %cpp-verify --jobs=1 --function=uses_wrong --obligation-out=%t.cpv %s -- > /dev/null 2>&1
+// RUN: not %cpp-verify --obligation-in=%t.cpv 2>&1 | FileCheck %s --check-prefix=RAN --implicit-check-not=add_two
+// RUN: %cpp-verify --jobs=1 --function=uses_add %s -- 2>&1 | FileCheck %s --check-prefix=CALLEE --implicit-check-not=Verified
+// RUN: not %cpp-verify --jobs=1 --function=uses_bad %s -- 2>&1 | FileCheck %s --check-prefix=SPEC --implicit-check-not=error:
+// RUN: %cpp-verify --jobs=1 --function=reach %s -- 2>&1 | FileCheck %s --check-prefix=PREDICATE --implicit-check-not=Verified
+// RUN: not %cpp-verify --jobs=1 --function=climbs %s -- 2>&1 | FileCheck %s --check-prefix=STEP
+// RUN: not %cpp-verify --jobs=1 --solver-rlimit=1 --function=reach %s -- 2>&1 | FileCheck %s --check-prefix=RULES
+// RUN: not %cpp-verify --jobs=1 --function=nothing %s -- 2>&1 | FileCheck %s --check-prefix=NONE
+// RUN: %cpp-verify --list-functions --function='add_*' %s -- 2>&1 | FileCheck %s --check-prefix=LIST --implicit-check-not=uses_
+//
+// --function reports only the functions whose names match: a glob pattern,
+// repeatable. What their verdicts rely on is verified too, so each verdict
+// is the one a run of the whole file gives; what they do not rely on is not
+// verified at all.
+
+namespace cv = cppverify;
+
+int add_one(int x)
+  cv::pre(x < 100)
+  cv::post(cv::result == x + 1)
+{
+  return x + 1;
+}
+
+int add_two(int x)
+  cv::pre(x < 100)
+  cv::post(cv::result == x + 2)
+{
+  return x + 2;
+}
+
+int wrong(int x)
+  cv::pre(x < 100)
+  cv::post(cv::result == x)
+{
+  return x + 1;
+}
+
+int uses_wrong(int x)
+  cv::pre(x < 50)
+  cv::post(cv::result == x + 1)
+{
+  int y = wrong(x);
+  return y + 1;
+}
+
+int uses_add(int x)
+  cv::pre(x < 50)
+  cv::post(cv::result == x + 2)
+{
+  int y = add_one(x);
+  return y + 1;
+}
+
+// A spec whose termination fails has no definition, whoever is selected.
+cv::spec int bad(int n)
+  cv::decreases(n)
+{
+  return n > 100 ? 0 : bad(n + 1);
+}
+
+int uses_bad(int x)
+  cv::post(bad(x) == bad(x) + 0)
+{
+  return x;
+}
+
+int jumps(int x)
+  cv::post(true)
+{
+  goto done;
+done:
+  return x;
+}
+
+cv::spec bool edge(int a, int b) { return b == a + 1; }
+
+cv::spec bool reach(int a, int b)
+  cv::inductive
+{
+  return a == b || cv::exists(c, edge(a, c) && reach(c, b));
+}
+
+// Its postcondition is false at a == b; the induction that refutes it is
+// a generated function.
+cv::spec bool climbs(int a, int b)
+  cv::inductive
+  cv::post(!cv::result || a < b)
+{
+  return a == b || cv::exists(c, edge(a, c) && climbs(c, b));
+}
+
+// ALL: Verified: add_one [backend=z3]
+// ALL: Verified: add_two [backend=z3]
+// ALL: error: verification failed: wrong
+// ALL: Unresolved: uses_wrong [backend=z3] [reason=callee.contract] (relies on the contract of wrong, which is not established)
+// ALL: Verified: uses_add [backend=z3]
+// ALL: error: spec decreases failed: bad
+// ALL: Unresolved: uses_bad [backend=z3] [reason=spec.termination]
+// ALL: Verified: inductive predicate: reach
+// ALL: Verified: inductive predicate: climbs
+// ALL: Unresolved: spec post: climbs [reason=spec.post]
+// ALL: error: spec post by induction failed: climbs
+// ALL: Summary: 5 verified, 3 failed, 4 unresolved (callee.contract 1, construct.unsupported 1, spec.post 1, spec.termination 1)
+
+// The same verdict, alone: wrong is verified, and its failure demotes it.
+// ONE: Unresolved: uses_wrong [backend=z3] [reason=callee.contract] (relies on the contract of wrong, which is not established)
+// ONE-NEXT: Summary: 1 unresolved (callee.contract 1)
+
+// GLOB: Verified: add_one [backend=z3]
+// GLOB-NEXT: Verified: add_two [backend=z3]
+// GLOB-NEXT: Summary: 2 verified
+
+// Only uses_wrong and what it relies on were verified.
+// RAN-DAG: wrong
+// RAN-DAG: uses_wrong
+
+// A callee that verifies is verified, so its caller is.
+// CALLEE: Verified: uses_add [backend=z3]
+// CALLEE-NEXT: Summary: 1 verified
+
+// SPEC: Unresolved: uses_bad [backend=z3] [reason=spec.termination] (relies on the definition of bad, whose termination is not established)
+// SPEC-NEXT: Summary: 1 unresolved (spec.termination 1)
+
+// An inductive predicate is reported with its rules.
+// PREDICATE: Verified: inductive predicate: reach
+// PREDICATE-NEXT: Summary: 1 verified
+
+// Its step and rule proofs are reported with it when they do not hold.
+// RULES: Unresolved: inductive predicate: reach [reason=spec.inductive] (its rules are not established: monotonicity, case analysis, introduction)
+// RULES-NEXT: function_filter.cpp:[[#]]:3: Unresolved: spec decreases unresolved: reach
+// RULES-NEXT: function_filter.cpp:[[#]]:3: Unresolved: reach (monotonicity)
+// RULES-NEXT: function_filter.cpp:[[#]]:3: Unresolved: reach (case analysis)
+// RULES-NEXT: function_filter.cpp:[[#]]:3: Unresolved: reach (introduction)
+// RULES-NEXT: Summary: 5 unresolved ({{.*}}spec.inductive 1)
+
+// The induction of a generated function is reported with its predicate.
+// STEP: Verified: inductive predicate: climbs
+// STEP-NEXT: Unresolved: spec post: climbs [reason=spec.post] (relies on the postcondition of climbs.step, which is not established)
+// STEP-NEXT: function_filter.cpp:92:24: error: spec post by induction failed: climbs
+// STEP-NEXT: Summary: 1 verified, 1 failed, 1 unresolved (spec.post 1)
+
+// NONE: error: no function matches --function=nothing
+
+// LIST: function_filter.cpp:22:5: function add_one
+// LIST-NEXT: function_filter.cpp:29:5: function add_two
diff --git a/clang/test/Verify/suite/inductive_counterexamples.cpp b/clang/test/Verify/suite/inductive_counterexamples.cpp
index 4fb3d8c718..7ce2f26981 100644
--- a/clang/test/Verify/suite/inductive_counterexamples.cpp
+++ b/clang/test/Verify/suite/inductive_counterexamples.cpp
@@ -1,76 +1,241 @@
-// RUN: not %cpp-verify %s -- 2>&1 | FileCheck %s
+// RUN: not %cpp-verify --jobs=1 %s -- 2>&1 | FileCheck %s
+// RUN: not %cpp-verify --jobs=1 --confirm-bound=0 %s -- 2>&1 | FileCheck %s --check-prefix=NONE
+// RUN: not %cpp-verify --jobs=1 --diagnostics-format=json %s -- 2>/dev/null | FileCheck %s --check-prefix=JSON
+// RUN: not %cpp-verify --backend=bmc --confirm-bound=3 %s -- 2>&1 | FileCheck %s --check-prefix=OPTION
 //
-// A counterexample may need an inductive predicate to be false somewhere,
-// which no derivation height shows. Its check decides that by the least
-// fixpoint over the arguments the predicate's derivations reach, when they
-// are finitely many, or by a proved postcondition; otherwise the message
-// names the application it could not decide.
+// A counterexample that passes through a loop starts the loop's next steps
+// from any state its invariants allow, which no execution need reach. Its
+// failure says so, and unrolling each loop looks for an execution that
+// fails: one within the bound, none within it, or a proof that none fails at
+// all. A loop without a measure is named beside a failure too.
 
-#include <cppverify.h>
-using cppverify::valid;
+namespace cv = cppverify;
 
-cppverify::spec bool edge(int a, int b) { return b == a + 2 || b == 2 * a; }
-
-// Finitely many arguments: every step goes up, and none above b counts.
-cppverify::spec bool climb(int a, int b) cppverify::inductive {
-  return a == b || (a < b && cppverify::exists(c, edge(a, c) && climb(c, b)));
+int count_up(int n)
+  cv::pre(n >= 0 && n <= 5)
+  cv::post(cv::result == n)
+{
+  int c = 0;
+  while (c < n)
+    cv::decreases(n - c)
+  {
+    c = c + 1;
+  }
+  return c;
 }
 
-cppverify::proof void climb_three_four() cppverify::post(climb(3, 4)) {}
-// CHECK-DAG: error: verification failed: climb_three_four {{.*}}[reason=counterexample]
+int sum_wrong(int n)
+  cv::pre(n >= 0 && n <= 5)
+  cv::post(cv::result == n)
+{
+  int s = 0;
+  for (int i = 0; i < n; i = i + 1)
+    cv::invariant(0 <= i && i <= n && s == 2 * i)
+    cv::decreases(n - i)
+  {
+    s = s + 2;
+  }
+  return s;
+}
 
-cppverify::proof void climb_one_four() cppverify::post(climb(1, 4)) {
-  cppverify::check(climb(4, 4));
-  cppverify::check(climb(2, 4));
+int far_wrong(int n)
+  cv::pre(n >= 0 && n <= 1000)
+  cv::post(cv::result < 100)
+{
+  int c = 0;
+  while (c < n)
+    cv::invariant(0 <= c && c <= n)
+    cv::decreases(n - c)
+  {
+    c = c + 1;
+  }
+  return c;
 }
-// CHECK-DAG: Verified: climb_one_four
 
-// Defined together, with finitely many arguments.
-cppverify::spec bool ev(int n);
-cppverify::spec bool od(int n) cppverify::inductive { return n == 1 || (n > 1 && ev(n - 1)); }
-cppverify::spec bool ev(int n) cppverify::inductive { return n == 0 || (n > 0 && od(n - 1)); }
+int no_loop(int x)
+  cv::pre(x < 100)
+  cv::post(cv::result == x)
+{
+  return x + 1;
+}
 
-cppverify::proof void four_is_odd() cppverify::post(od(4)) {}
-// CHECK-DAG: error: verification failed: four_is_odd {{.*}}[reason=counterexample]
+int unmeasured(int n)
+  cv::pre(n >= 0 && n <= 5)
+  cv::post(cv::result == n + 1)
+{
+  int c = 0;
+  while (c < n)
+    cv::invariant(0 <= c && c <= n)
+  {
+    c = c + 1;
+  }
+  return c;
+}
 
-// Reading memory: a cycle that never reaches 5.
-cppverify::spec bool linked(const int *next, int n, int i, int j)
-  cppverify::inductive
-  cppverify::reads(next, n)
+// Unrolling checks the copies of the failed check, here the division in
+// each iteration, and finds the execution that divides by zero.
+int divides(int n)
+  cv::pre(n >= 0 && n <= 5)
+  cv::post(cv::result >= -5)
 {
-  return i == j || (0 <= i && i < n && linked(next, n, next[i], j));
+  int c = 0;
+  int q = 0;
+  while (c < n)
+    cv::invariant(0 <= c && c <= n)
+    cv::decreases(n - c)
+  {
+    q = 10 / (3 - c);
+    c = c + 1;
+  }
+  return q - 5;
 }
 
-void around(const int *next)
-  cppverify::pre(valid(next, 2) && next[0] == 1 && next[1] == 0)
+// Unrolling keeps no invariant, so it cannot confirm a failed one.
+int grows(int n)
+  cv::pre(n >= 0 && n <= 5)
+  cv::post(true)
 {
-  cppverify::check(linked(next, 2, 0, 5));
+  int c = 0;
+  while (c < n)
+    cv::invariant(c <= 2)
+    cv::decreases(n - c)
+  {
+    c = c + 1;
+  }
+  return c;
 }
-// CHECK-DAG: error: verification failed: around {{.*}}[reason=counterexample]
 
-// Infinitely many arguments, but a proved postcondition decides it.
-cppverify::spec bool even(int n) cppverify::inductive cppverify::post(!cppverify::result || (n >= 0 && n % 2 == 0)) {
-  return n == 0 || even(n - 2);
+// The copies of the failed check are those at its place: the check after
+// the loop fails sooner, with n == 2, but it is another check.
+int two_checks(int n)
+  cv::pre(n >= 0 && n <= 5)
+  cv::post(true)
+{
+  int c = 0;
+  while (c < n)
+    cv::invariant(0 <= c && c <= n)
+    cv::decreases(n - c)
+  {
+    cv::check(c != 4);
+    c = c + 1;
+  }
+  cv::check(c != 2);
+  return c;
 }
 
-cppverify::proof void three_is_even() cppverify::post(even(3)) {}
-// CHECK-DAG: error: verification failed: three_is_even {{.*}}[reason=counterexample]
+// And those of its kind: the failed check is the overflow of INT_MIN / -1,
+// and the division by zero at the same place fails one iteration sooner, in
+// every execution that would reach it. A copy is solved in the executions
+// that pass the failing checks before it, so none fails the overflow.
+int two_kinds(int a, int n)
+  cv::pre(n >= 0 && n <= 5)
+  cv::post(true)
+{
+  int c = 0;
+  int q = 0;
+  while (c < n)
+    cv::invariant(0 <= c && c <= n)
+    cv::decreases(n - c)
+  {
+    q = a / (1 - c);
+    c = c + 1;
+  }
+  return q;
+}
 
-// Neither: the message names the application.
-cppverify::spec bool odd(int n) cppverify::inductive { return n == 1 || odd(n - 2); }
+// The first division fails at c == k, and the second one iteration sooner
+// when m == k - 1: the execution that fails the first within 2 iterations
+// divides by zero in the second first. The one shown passes it.
+int past_failure(int k, int m, int n)
+  cv::pre(n >= 0 && n <= 5)
+  cv::pre((k == 1 && m == 0) || (k == 3 && m == 100))
+  cv::post(true)
+{
+  int c = 0;
+  int q = 0;
+  while (c < n)
+    cv::invariant(0 <= c && c <= n)
+    cv::decreases(n - c)
+  {
+    q = 100 / (k - c);
+    q = q + 100 / (m - c);
+    c = c + 1;
+  }
+  return q;
+}
 
-cppverify::proof void four_is_odd_too() cppverify::post(odd(4)) {}
-// CHECK-DAG: four_is_odd_too {{.*}}whether odd(4) holds: no derivation was found among the heights tried
+// A failure on a path that skips the loop has no loop to note.
+int skipped(int n)
+  cv::pre(n >= 0 && n <= 5)
+  cv::post(cv::result >= 0)
+{
+  int c = 0;
+  if (n > 3) {
+    while (c < n)
+      cv::invariant(0 <= c && c <= n)
+      cv::decreases(n - c)
+    {
+      c = c + 1;
+    }
+  }
+  return c - 1;
+}
 
-// A postcondition that is not established is no evidence: the
-// counterexample that used it is not reported as one. ge(-5000) holds, by a
-// derivation too tall to find, while the false postcondition says it
-// cannot.
-cppverify::spec bool ge(int n);
-cppverify::spec bool ge(int n) cppverify::inductive cppverify::post(!cppverify::result || n > -1000) {
-  return n == 20 || ge(n + 1);
+// A proof gets no notes.
+int count_up_proved(int n)
+  cv::pre(n >= 0 && n <= 5)
+  cv::post(cv::result == n)
+{
+  int c = 0;
+  while (c < n)
+    cv::invariant(0 <= c && c <= n)
+    cv::decreases(n - c)
+  {
+    c = c + 1;
+  }
+  return c;
 }
-// CHECK-DAG: error: spec post by induction failed: ge
 
-cppverify::proof void far() cppverify::post(ge(-5000)) {}
-// CHECK-DAG: Unresolved: verification unresolved: far {{.*}}[reason=spec.post] (its counterexample is checked with the postcondition of ge, which is not established)
+// CHECK:      inductive_counterexamples.cpp:16:23: error: verification failed: count_up [{{.*}}::postcondition@16:23] {{.*}}trace: loop.entry@19:3 -> loop.exit@19:3
+// CHECK-NEXT: note: the counterexample's state at the loop at 19:3 is any state its invariants allow, not necessarily one an execution reaches
+// CHECK-NEXT: note: no execution fails this check: every loop ends within 5 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof
+// CHECK-NEXT: inductive_counterexamples.cpp:29:23: error: verification failed: sum_wrong [{{.*}}::postcondition@29:23]
+// CHECK-NEXT: note: the counterexample's state at the loop at 32:3 is any state its invariants allow, not necessarily one an execution reaches
+// CHECK-NEXT: note: an execution fails this check within 1 iteration of each loop (counterexample: {{.*}}n [ssa=n_0] [type=i32] = 1{{.*}})
+// CHECK-NEXT: inductive_counterexamples.cpp:43:23: error: verification failed: far_wrong [{{.*}}::postcondition@43:23]
+// CHECK-NEXT: note: the counterexample's state at the loop at 46:3 is any state its invariants allow, not necessarily one an execution reaches
+// CHECK-NEXT: note: no execution fails this check within 10 iterations of each loop
+// CHECK-NEXT: inductive_counterexamples.cpp:57:23: error: verification failed: no_loop [{{.*}}::postcondition@57:23]
+// CHECK-NEXT: inductive_counterexamples.cpp:64:23: error: verification failed: unmeasured [{{.*}}::postcondition@64:23]
+// CHECK-NEXT: note: the loop at 67:3 has no cppverify::decreases: a proof would be Unresolved (decreases.missing) until it has one
+// CHECK-NEXT: note: the counterexample's state at the loop at 67:3 is any state its invariants allow, not necessarily one an execution reaches
+// CHECK-NEXT: note: an execution fails this check with no iteration of any loop (counterexample: {{.*}}n [ssa=n_0] [type=i32] = 0{{.*}})
+// CHECK-NEXT: inductive_counterexamples.cpp:87:7: error: verification failed: divides [{{.*}}::division-by-zero@87:7]
+// CHECK-NEXT: note: the counterexample's state at the loop at 83:3 is any state its invariants allow, not necessarily one an execution reaches
+// CHECK-NEXT: note: an execution fails this check within 4 iterations of each loop (counterexample: {{.*}}c [ssa=c_4] [type=i32] = 3{{.*}})
+// CHECK-NEXT: inductive_counterexamples.cpp:100:21: error: verification failed: grows [{{.*}}::invariant-preserved@100:21]
+// CHECK-NEXT: note: the counterexample's state at the loop at 99:3 is any state its invariants allow, not necessarily one an execution reaches
+// CHECK-NEXT: inductive_counterexamples.cpp:119:5: error: verification failed: two_checks [{{.*}}::assertion@119:5]
+// CHECK-NEXT: note: the counterexample's state at the loop at 115:3 is any state its invariants allow, not necessarily one an execution reaches
+// CHECK-NEXT: note: an execution fails this check within 5 iterations of each loop (counterexample: {{.*}}n [ssa=n_0] [type=i32] = 5{{.*}})
+// CHECK-NEXT: inductive_counterexamples.cpp:140:7: error: verification failed: two_kinds [{{.*}}::overflow@140:7]
+// CHECK-NEXT: note: the counterexample's state at the loop at 136:3 is any state its invariants allow, not necessarily one an execution reaches
+// CHECK-NEXT: note: no execution fails this check without failing an earlier one first (the division-by-zero check at 140:7 fails): those that pass the checks before it end every loop within 2 iterations, and unrolling proves it there
+// CHECK-NEXT: inductive_counterexamples.cpp:160:7: error: verification failed: past_failure [{{.*}}::division-by-zero@160:7]
+// CHECK-NEXT: note: the counterexample's state at the loop at 156:3 is any state its invariants allow, not necessarily one an execution reaches
+// CHECK-NEXT: note: an execution fails this check within 4 iterations of each loop (counterexample: {{.*}}k [ssa=k_0] [type=i32] = 3, m [ssa=m_0] [type=i32] = 100{{.*}})
+// CHECK-NEXT: inductive_counterexamples.cpp:170:23: error: verification failed: skipped [{{.*}}::postcondition@170:23]
+// CHECK-NEXT: Verified: count_up_proved [backend=z3]
+// CHECK-NEXT: Summary: 1 verified, 11 failed
+
+// Without unrolling, a failure still says where its state comes from.
+// NONE:      error: verification failed: count_up
+// NONE-NEXT: note: the counterexample's state at the loop at 19:3 is any state its invariants allow, not necessarily one an execution reaches
+// NONE-NEXT: error: verification failed: sum_wrong
+
+// JSON: "function":"count_up",{{.*}}"notes":["the counterexample's state at the loop at 19:3 is any state its invariants allow, not necessarily one an execution reaches","no execution fails this check: every loop ends within 5 iterations{{.*}}"]
+// JSON: "function":"no_loop"
+// JSON-NOT: "notes"
+// JSON: "function":"unmeasured"
+
+// OPTION: error: --confirm-bound requires source verification with --backend=z3, cvc5, portfolio, or race
diff --git a/clang/test/Verify/suite/max_failures.cpp b/clang/test/Verify/suite/max_failures.cpp
new file mode 100644
index 0000000000..ee169ceb8d
--- /dev/null
+++ b/clang/test/Verify/suite/max_failures.cpp
@@ -0,0 +1,103 @@
+// RUN: not %cpp-verify --jobs=1 %s -- 2>&1 | FileCheck %s --check-prefix=ONE
+// RUN: not %cpp-verify --jobs=1 --max-failures=2 %s -- 2>&1 | FileCheck %s --check-prefix=TWO
+// RUN: not %cpp-verify --jobs=4 --max-failures=2 %s -- 2>&1 | FileCheck %s --check-prefix=TWO
+// RUN: not %cpp-verify --jobs=1 --max-failures=0 %s -- 2>&1 | FileCheck %s --check-prefix=ALL
+// RUN: not %cpp-verify --jobs=4 --max-failures=0 %s -- 2>&1 | FileCheck %s --check-prefix=ALL
+// RUN: not %cpp-verify --jobs=1 --max-failures=0 --diagnostics-format=json %s -- 2>/dev/null | FileCheck %s --check-prefix=JSON
+// RUN: not %cpp-verify --backend=cvc5 --max-failures=2 %s -- 2>&1 | FileCheck %s --check-prefix=OPTION
+//
+// A function reports the first check that fails, in the order an execution
+// meets them; --max-failures=N reports the first N, and 0 every one, each
+// with its own counterexample. A check after the first failure is solved in
+// the executions that pass the failing checks before it, so its
+// counterexample reaches it, and a check that fails only where an earlier
+// one does is not reported. The summary still counts functions.
+
+namespace cv = cppverify;
+
+int three_bugs(int x, int y)
+  cv::pre(x < 1000 && y < 1000)
+  cv::post(cv::result > 0)
+  cv::post(cv::result < 100)
+{
+  int q = 10 / y;
+  int r = x + q;
+  return r;
+}
+
+int one_bug(int x)
+  cv::pre(x < 100)
+  cv::post(cv::result == x)
+{
+  return x + 1;
+}
+
+// The assertion fails only where the division divides by zero.
+int dependent(int x)
+  cv::pre(x < 100)
+  cv::post(true)
+{
+  int q = 100 / x;
+  cv::check(x != 0);
+  return q;
+}
+
+// Each failure has its notes: the first holds in every execution, which its
+// loop's missing invariant hides, and the second fails at once.
+int counted(int n)
+  cv::pre(n >= 0 && n <= 3)
+  cv::post(cv::result == n)
+  cv::post(cv::result == n + 1)
+{
+  int c = 0;
+  while (c < n)
+    cv::decreases(n - c)
+  {
+    c = c + 1;
+  }
+  return c;
+}
+
+// ONE:      max_failures.cpp:23:3: error: verification failed: three_bugs [{{.*}}::division-by-zero@23:3] (counterexample: {{.*}}y [ssa=y_0] [type=i32] = 0{{.*}}) [backend=z3] [reason=counterexample]
+// ONE-NEXT: max_failures.cpp:30:23: error: verification failed: one_bug [{{.*}}::postcondition@30:23]
+// ONE-NEXT: max_failures.cpp:40:3: error: verification failed: dependent [{{.*}}::division-by-zero@40:3]
+// ONE-NEXT: max_failures.cpp:49:23: error: verification failed: counted [{{.*}}::postcondition@49:23]
+// ONE-NEXT: note: the counterexample's state at the loop at 53:3 is any state its invariants allow, not necessarily one an execution reaches
+// ONE-NEXT: note: no execution fails this check: every loop ends within 3 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof
+// ONE-NEXT: Summary: 4 failed
+
+// The overflow's counterexample divides by y, which is not zero.
+// TWO:      max_failures.cpp:23:3: error: verification failed: three_bugs [{{.*}}::division-by-zero@23:3]
+// TWO-NEXT: max_failures.cpp:24:3: error: verification failed: three_bugs [{{.*}}::overflow@24:3] (counterexample: {{.*}}y [ssa=y_0] [type=i32] = {{-?[1-9][0-9]*}}) [backend=z3] [reason=counterexample]
+// TWO-NEXT: max_failures.cpp:30:23: error: verification failed: one_bug [{{.*}}::postcondition@30:23]
+// TWO-NEXT: max_failures.cpp:40:3: error: verification failed: dependent [{{.*}}::division-by-zero@40:3]
+// TWO-NEXT: max_failures.cpp:49:23: error: verification failed: counted [{{.*}}::postcondition@49:23]
+// TWO-NEXT: note: the counterexample's state at the loop at 53:3 is any state its invariants allow, not necessarily one an execution reaches
+// TWO-NEXT: note: no execution fails this check: every loop ends within 3 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof
+// TWO-NEXT: max_failures.cpp:50:23: error: verification failed: counted [{{.*}}::postcondition@50:23]
+// TWO-NEXT: note: the counterexample's state at the loop at 53:3 is any state its invariants allow, not necessarily one an execution reaches
+// TWO-NEXT: note: an execution fails this check with no iteration of any loop (counterexample: {{.*}}n [ssa=n_0] [type=i32] = 0{{.*}})
+// TWO-NEXT: Summary: 4 failed
+
+// ALL:      max_failures.cpp:23:3: error: verification failed: three_bugs [{{.*}}::division-by-zero@23:3]
+// ALL-NEXT: max_failures.cpp:24:3: error: verification failed: three_bugs [{{.*}}::overflow@24:3] (counterexample: {{.*}}y [ssa=y_0] [type=i32] = {{-?[1-9][0-9]*}})
+// ALL-NEXT: max_failures.cpp:20:23: error: verification failed: three_bugs [{{.*}}::postcondition@20:23] (counterexample: {{.*}}y [ssa=y_0] [type=i32] = {{-?[1-9][0-9]*}};
+// ALL-NEXT: max_failures.cpp:21:23: error: verification failed: three_bugs [{{.*}}::postcondition@21:23] (counterexample: {{.*}}y [ssa=y_0] [type=i32] = {{-?[1-9][0-9]*}};
+// ALL-NEXT: max_failures.cpp:30:23: error: verification failed: one_bug [{{.*}}::postcondition@30:23]
+// ALL-NEXT: max_failures.cpp:40:3: error: verification failed: dependent [{{.*}}::division-by-zero@40:3]
+// ALL-NEXT: max_failures.cpp:49:23: error: verification failed: counted [{{.*}}::postcondition@49:23]
+// ALL-NEXT: note: the counterexample's state at the loop at 53:3 is any state its invariants allow, not necessarily one an execution reaches
+// ALL-NEXT: note: no execution fails this check: every loop ends within 3 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof
+// ALL-NEXT: max_failures.cpp:50:23: error: verification failed: counted [{{.*}}::postcondition@50:23]
+// ALL-NEXT: note: the counterexample's state at the loop at 53:3 is any state its invariants allow, not necessarily one an execution reaches
+// ALL-NEXT: note: an execution fails this check with no iteration of any loop (counterexample: {{.*}}n [ssa=n_0] [type=i32] = 0{{.*}})
+// ALL-NEXT: Summary: 4 failed
+
+// JSON-COUNT-4: "function":"three_bugs"
+// JSON-NOT: "function":"three_bugs"
+// JSON: "function":"one_bug"
+// JSON-NEXT: "function":"dependent"
+// JSON-COUNT-2: "function":"counted"{{.*}}"notes":[
+// JSON-NOT: "function"
+
+// OPTION: error: --max-failures requires source verification with --backend=z3
diff --git a/clang/test/Verify/suite/time_report.cpp b/clang/test/Verify/suite/time_report.cpp
new file mode 100644
index 0000000000..b1f4ff7847
--- /dev/null
+++ b/clang/test/Verify/suite/time_report.cpp
@@ -0,0 +1,104 @@
+// RUN: not %cpp-verify --jobs=1 --timeout=1000 --time-report %s -- 2>&1 | FileCheck %s --check-prefix=TEXT
+// RUN: not %cpp-verify --jobs=1 --timeout=1000 --time-report --diagnostics-format=json %s -- 2>/dev/null \
+// RUN:   | %python %S/Inputs/time_report_phases.py | FileCheck %s --check-prefix=PHASES
+// RUN: not %cpp-verify --backend=bmc --time-report --diagnostics-format=json %S/Inputs/time_report_wrong.cpp -- 2>/dev/null \
+// RUN:   | %python %S/Inputs/time_report_phases.py | FileCheck %s --check-prefix=BMC
+// RUN: %cpp-verify --jobs=1 --time-report --function=proved %s -- 2>&1 | FileCheck %s --check-prefix=FILTER --implicit-check-not=after_loop --implicit-check-not=fibo
+// RUN: not %cpp-verify --jobs=1 --timeout=1000 --progress %s -- 2>&1 >/dev/null | FileCheck %s --check-prefix=PROGRESS
+// RUN: not %cpp-verify --jobs=1 --timeout=1000 %s -- 2>&1 >/dev/null | count 0
+// RUN: not %cpp-verify --obligation-in=%t.none --time-report 2>&1 | FileCheck %s --check-prefix=REPLAY
+//
+// --time-report says where a run and each function spent their time: the
+// lowering, the solving (with the inductions and the counterexample checks
+// within it), and the confirmations after a failure, the busiest function
+// first. --progress counts the functions done on standard error, which is
+// the default only on a terminal.
+
+namespace cv = cppverify;
+
+// Solved, with no induction and nothing to confirm.
+int proved(int x)
+  cv::pre(x < 100)
+  cv::post(cv::result == x + 1)
+{
+  return x + 1;
+}
+
+// Its failure passes through the loop, which unrolling confirms.
+int after_loop(int n)
+  cv::pre(n >= 0 && n <= 3)
+  cv::post(cv::result == n)
+{
+  int c = 0;
+  while (c < n)
+    cv::decreases(n - c)
+  {
+    c = c + 1;
+  }
+  return c;
+}
+
+cv::spec int fibo(int n)
+  cv::decreases(n)
+  cv::post(cv::result >= 0)
+{
+  if (n <= 0) return 0;
+  if (n == 1) return 1;
+  return fibo(n - 2) + fibo(n - 1);
+}
+
+// Proved by induction.
+cv::proof void grows(int n)
+  cv::pre(n >= 3)
+  cv::post(fibo(n) >= n - 1)
+{
+}
+
+cv::spec int pow2(int n)
+  cv::decreases(n)
+  cv::post(cv::result >= n + 1)
+{
+  return n <= 0 ? 1 : 2 * pow2(n - 1);
+}
+
+// Inductions are tried, and the counterexample is confirmed by a proof
+// after every function is verified.
+cv::proof void small_power(int n)
+  cv::pre(n >= 1000000000)
+  cv::post(pow2(n) < 1000)
+{
+}
+
+// TEXT:      Time report (seconds): conversion {{[0-9]+\.[0-9][0-9][0-9]}}, verification {{[0-9]+\.[0-9][0-9][0-9]}}, settling {{[0-9]+\.[0-9][0-9][0-9]}}
+// TEXT-NEXT: {{^}}     total  lowering   solving  induction  certification  confirmation  function{{$}}
+// TEXT-DAG:  {{^ +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9]}}  proved{{$}}
+// TEXT-DAG:  {{^ +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9]}}  after_loop{{$}}
+// TEXT-DAG:  {{^ +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9]}}  fibo{{$}}
+// TEXT-DAG:  {{^ +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9]}}  grows{{$}}
+// TEXT-DAG:  {{^ +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9]}}  pow2{{$}}
+// TEXT-DAG:  {{^ +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9]}}  small_power{{$}}
+// TEXT:      Summary: 4 verified, 2 failed
+
+// Which phases took time, and that the times add up.
+// PHASES:     run conversion settling verification
+// PHASES-DAG: proved solving=1 induction=0 certification=1 confirmation=0 adds up
+// PHASES-DAG: after_loop solving=1 induction=0 certification=1 confirmation=1 adds up
+// PHASES-DAG: grows solving=1 induction=1 certification=1 confirmation=0 adds up
+// PHASES-DAG: small_power solving=1 induction=1 certification=1 confirmation=1 adds up
+// PHASES-DAG: fibo solving=1 induction=0 certification=0 confirmation=0 adds up
+// PHASES:     {{^}}busiest first{{$}}
+
+// Under BMC too; a failure without a loop has nothing to confirm.
+// BMC-DAG: wrong solving=1 induction=0 certification=1 confirmation=0 adds up
+// BMC-DAG: count solving=1 induction=0 certification=0 confirmation=0 adds up
+
+// Only the functions reported are listed.
+// FILTER:      Verified: proved
+// FILTER-NEXT: Time report (seconds):
+// FILTER-NEXT: total
+// FILTER-NEXT: {{^ +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9]}}  proved{{$}}
+// FILTER-NEXT: Summary: 1 verified
+
+// PROGRESS: [1/6] proved{{.*}}[2/6] after_loop{{.*}}[6/6] small_power
+
+// REPLAY: error: --time-report requires source verification
diff --git a/clang/test/Verify/suite/time_report_backends.test b/clang/test/Verify/suite/time_report_backends.test
new file mode 100644
index 0000000000..cc2582c551
--- /dev/null
+++ b/clang/test/Verify/suite/time_report_backends.test
@@ -0,0 +1,10 @@
+# REQUIRES: cvc5
+# The solvers of every backend count their counterexample checks for
+# --time-report, through a portfolio's and a race's components too.
+# RUN: not %cpp-verify --backend=cvc5 --time-report --diagnostics-format=json %S/Inputs/time_report_wrong.cpp -- 2>/dev/null \
+# RUN:   | %python %S/Inputs/time_report_phases.py | FileCheck %s
+# RUN: not %cpp-verify --backend=portfolio --time-report --diagnostics-format=json %S/Inputs/time_report_wrong.cpp -- 2>/dev/null \
+# RUN:   | %python %S/Inputs/time_report_phases.py | FileCheck %s
+# RUN: not %cpp-verify --backend=race --time-report --diagnostics-format=json %S/Inputs/time_report_wrong.cpp -- 2>/dev/null \
+# RUN:   | %python %S/Inputs/time_report_phases.py | FileCheck %s
+# CHECK: wrong solving=1 induction=0 certification=1 confirmation=0 adds up
diff --git a/clang/test/Verify/suite/trusted_declarations.cpp b/clang/test/Verify/suite/trusted_declarations.cpp
new file mode 100644
index 0000000000..8440c5a3ce
--- /dev/null
+++ b/clang/test/Verify/suite/trusted_declarations.cpp
@@ -0,0 +1,59 @@
+// RUN: not %cpp-verify --jobs=1 %s -- 2>&1 | FileCheck %s
+// RUN: not %cpp-verify --jobs=1 %s -- -DSPEC 2>&1 | FileCheck %s --check-prefix=SPEC
+//
+// [[cppverify::trusted]] on a declaration says that callers which see no
+// definition assume the contract. A definition that only inherits the mark
+// from such a declaration is verified, so a wrong body is found; on a
+// definition itself, the mark leaves the body unverified.
+
+namespace cv = cppverify;
+
+// As a header declares it.
+[[cppverify::trusted]] int clamp100(int x)
+  cv::post(cv::result >= 0 && cv::result <= 100);
+
+int clamp100(int x)
+{
+  if (x < 0)
+    return 0;
+  if (x > 100)
+    return 101;
+  return x;
+}
+
+int scaled(int x)
+  cv::post(cv::result >= 0 && cv::result <= 200)
+{
+  return 2 * clamp100(x);
+}
+
+[[cppverify::trusted]] int halved(int x)
+  cv::pre(x >= 0)
+  cv::post(cv::result >= 0)
+{
+  return x - 1;
+}
+
+[[cppverify::trusted]] int above(int x)
+  cv::post(cv::result > x);
+
+int uses_above(int x)
+  cv::pre(x < 100)
+  cv::post(cv::result > x)
+{
+  return above(x);
+}
+
+// CHECK: trusted_declarations.cpp:13:28: error: verification failed: clamp100 [{{.*}}::postcondition@13:28] (counterexample: {{.*}}result [ssa={{.*}}] [type=i32] = 101
+// CHECK: Unresolved: scaled [backend=z3] [reason=callee.contract] (relies on the contract of clamp100, which is not established)
+// CHECK: Trusted: halved (contract assumed, not verified)
+// CHECK: Trusted: above (contract assumed, not verified)
+// CHECK: Verified: uses_above [backend=z3] [trusts=above]
+
+// A spec cannot be trusted, on any of its declarations.
+#ifdef SPEC
+[[cppverify::trusted]] cv::spec int twice(int x);
+
+cv::spec int twice(int x) { return 2 * x; }
+#endif
+// SPEC: error: twice: {{\[\[cppverify::trusted\]\]}} does not apply to a spec function, whose definition is its meaning
diff --git a/clang/tools/cpp-verify/Main.cpp b/clang/tools/cpp-verify/Main.cpp
index 040acc1148..5cb8cdb83f 100644
--- a/clang/tools/cpp-verify/Main.cpp
+++ b/clang/tools/cpp-verify/Main.cpp
@@ -287,16 +287,63 @@ static cl::opt<bool>
                      "(spec axiom)"),
             cl::cat(CppVerifyCategory));
 
+static cl::opt<unsigned> ConfirmBound(
+    "confirm-bound",
+    cl::desc("For a failure whose counterexample passes through a loop, "
+             "unroll each loop up to this many iterations to look for an "
+             "execution that fails (default 10, 0 = do not look)"),
+    cl::init(10), cl::cat(CppVerifyCategory));
+
+static cl::opt<unsigned> MaxFailures(
+    "max-failures",
+    cl::desc("Report up to this many failing checks of a function, each with "
+             "its own counterexample (default 1, 0 = all; --backend=z3)"),
+    cl::init(1), cl::cat(CppVerifyCategory));
+
+static cl::list<std::string> FunctionPatterns(
+    "function",
+    cl::desc("Report only the functions whose names match this glob pattern "
+             "(repeatable); what their verdicts rely on is verified too"),
+    cl::value_desc("pattern"), cl::cat(CppVerifyCategory));
+
 static cl::opt<bool> ListFunctions(
     "list-functions",
     cl::desc("List the functions a run would verify, with their kinds and "
              "locations, and verify none"),
     cl::cat(CppVerifyCategory));
 
+static cl::opt<std::string> ContractsOut(
+    "contracts-out",
+    cl::desc("Write the contracts the file verifies and those it assumes from "
+             "other files, for --check-contracts"),
+    cl::value_desc("file"), cl::cat(CppVerifyCategory));
+
+static cl::opt<bool> CheckContracts(
+    "check-contracts",
+    cl::desc("Check that the contracts the given records (--contracts-out, "
+             "-fverify-contracts-out) assume are established by the "
+             "verification of their definitions in others"),
+    cl::cat(CppVerifyCategory));
+
+static cl::opt<bool> TimeReport(
+    "time-report",
+    cl::desc("Report where the run and each function spent their time: "
+             "lowering, solving, induction, certification, confirmation"),
+    cl::cat(CppVerifyCategory));
+
+static cl::opt<cl::boolOrDefault> Progress(
+    "progress",
+    cl::desc("Show on standard error how many functions are done (default: "
+             "when standard error is a terminal)"),
+    cl::cat(CppVerifyCategory));
+
 namespace {
 
 static int gVerifyFailures = 0;
 static verify::VerifySummary gSummary;
+/// A run over several files settles the contracts each declares without a
+/// definition against those the others verify, before printing.
+static std::unique_ptr<verify::CrossFileRun> gCrossFile;
 
 /// One line for the run: how many verdicts of each kind it reported, the
 /// reasons of the unresolved ones, and the time it took.
@@ -448,7 +495,16 @@ class VerifyConsumer : public ASTConsumer {
       VOpts.Quiet = Quiet.getValue();
       VOpts.Verbose = Verbose.getValue();
       VOpts.ListFunctions = ListFunctions.getValue();
+      VOpts.TimeReport = TimeReport.getValue();
+      VOpts.ContractsOut = ContractsOut.getValue();
+      if (Progress != cl::boolOrDefault::BOU_UNSET)
+        VOpts.Progress = Progress == cl::boolOrDefault::BOU_TRUE;
+      VOpts.MaxFailures = MaxFailures.getValue();
+      VOpts.FunctionPatterns.assign(FunctionPatterns.begin(),
+                                    FunctionPatterns.end());
+      VOpts.ConfirmBound = ConfirmBound.getValue();
       VOpts.Summary = &gSummary;
+      VOpts.CrossFile = gCrossFile.get();
       if (!verify::verifyTranslationUnit(Ctx, llvm::outs(), VOpts))
         ++gVerifyFailures;
     }
@@ -678,6 +734,12 @@ static bool resolveOptions(bool Replay) {
             "--backend=race";
   else if (given(BMCUnroll) && !Replay && Backend != "bmc")
     Error = "--unroll requires --backend=bmc";
+  else if (given(ConfirmBound) &&
+           (Replay || Backend == "bmc" || Backend == "lean"))
+    Error = "--confirm-bound requires source verification with --backend=z3, "
+            "cvc5, portfolio, or race";
+  else if (given(MaxFailures) && (Replay || Backend != "z3"))
+    Error = "--max-failures requires source verification with --backend=z3";
   else if (given(LeanFallbackScope) && LeanFallback.empty())
     Error = "--lean-fallback-scope requires --lean-fallback";
   else if (given(LeanAutoTimeout) && LeanProject.empty() &&
@@ -699,6 +761,8 @@ static bool resolveOptions(bool Replay) {
   else if ((given(CheckUB) || given(NoCheckUB)) && Replay)
     Error = "--check-ub and --no-check-ub apply to source verification; an "
             "archive keeps the checks it was written with";
+  else if (given(TimeReport) && Replay)
+    Error = "--time-report requires source verification";
   if (Error.empty())
     return true;
   llvm::errs() << "error: " << Error << "\n";
@@ -1064,6 +1128,14 @@ int main(int argc, const char **argv) {
   CommonOptionsParser &OptionsParser = ExpectedParser.get();
   if (!resolveOptions(!ObligationIn.empty()))
     return 1;
+  if (CheckContracts)
+    return verify::checkContracts(OptionsParser.getSourcePathList(),
+                                  llvm::outs()) != 0;
+  if (!ContractsOut.empty() && OptionsParser.getSourcePathList().size() != 1) {
+    llvm::errs() << "error: --contracts-out records one file; a run over "
+                    "several files settles their contracts itself\n";
+    return 1;
+  }
   if (!ObligationIn.empty()) {
     const std::vector<std::string> &Sources = OptionsParser.getSourcePathList();
     if (Sources.size() != 1 || Sources.front() != ReplayPlaceholder) {
@@ -1134,7 +1206,13 @@ int main(int argc, const char **argv) {
   TextDiagnosticPrinter ArgumentDiagnostics(llvm::errs(), *ArgumentOptions);
   Tool.setDiagnosticConsumer(&ArgumentDiagnostics);
   VerifyActionFactory Factory(ArgumentDiagnostics);
+  // Lean exports and --list-functions have no verdicts to settle.
+  if (OptionsParser.getSourcePathList().size() > 1 && BackendOpt != "lean" &&
+      LeanFallback.empty() && !ListFunctions)
+    gCrossFile = std::make_unique<verify::CrossFileRun>();
   int RC = Tool.run(&Factory);
+  if (gCrossFile)
+    gVerifyFailures += gCrossFile->finish(llvm::outs(), &gSummary);
   if (DiagnosticsFormat == verify::DiagnosticFormat::Text && !ListFunctions)
     printSummary(Start);
   if (verify::interruptRequested())
diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md
index 0927560a31..4cb50ca1a3 100644
--- a/docs/ARCHITECTURE.md
+++ b/docs/ARCHITECTURE.md
@@ -752,6 +752,31 @@ function as possibly divergent: its proof, and the proof of every caller, is
 reported `[partial]`. Calls within an executable or proof recursion cycle
 assert the decrease of the shared measure at the call site.
 
+**Counterexamples after a loop.** A certified failure (on Z3, cvc5, the
+portfolio, or the race) whose trace has an active loop event passed through
+the loop's havoc, so its state there is any the invariants allow. The driver
+notes that (`VerifyDiagnostic::Notes`, printed as `note:` lines and JSON
+`notes`) and confirms it the way BMC verifies: a copy of the function
+prepared for unrolling (`SpecInliner::prepareFunction`, the UB checks), each
+bound from 0 to `--confirm-bound` unrolled (`LoopUnroller`), passivized
+against the interface map, and solved obligation by obligation
+(`Z3VerifyBackend::verifyObligations`) with one query timeout for all
+bounds. The copies of the failed check are the obligations of its kind at
+its source location: one per iteration for a check in a loop's body, none
+for a loop's invariant or measure, which unrolling does not keep (then
+nothing is noted). A copy that fails at bound `b` is an execution within `b`
+iterations of each loop (callees still by their contracts), and its
+counterexample is noted; copies that all hold where every loop's unwinding
+is proved hold for every execution; copies that hold short of that go on to
+the next bound; anything unresolved ends the search without a note. Every
+failure of the unrolled module is reported, so each copy, and each loop's
+unwinding, is solved past the failing obligations before it (see
+`--max-failures` below): the execution noted fails no earlier check, and a
+copy that holds there, when another check fails before it, is noted as
+holding in every execution that does not fail that check first, named by its
+kind and place. A function with an unmeasured loop (`UnmeasuredLoop`) also
+gets a note naming it on any failure.
+
 **Loop exits.** A `break` or `return` inside the body leaves from the
 inductive iteration: its path guard is recorded and the path ends. After the
 loop the continuation assumes `(¬choice ∧ ¬cond) ∨ break₁ ∨ … ∨ return₁ ∨ …`.
@@ -2447,10 +2472,33 @@ expression being converted (`ASTConverter::CurrentRange`), unless the site
 names a place of its own, such as a function for the checks made after every
 function is converted. It is printed with Clang's `TextDiagnostic`, line and
 caret included, as a compiler error is, and its JSON record carries the range.
-A text run ends with a summary line: `printDiagnostics` counts each verdict
+`--function` filters what a run reports, not what its verdicts mean. A
+function is selected by the name its verdicts print, which for an inductive
+predicate's step (`InductiveStepOf`) is the predicate's, and a selected
+predicate's rule proofs (`InductiveRuleOf`) with it. `Verifier::run`
+schedules the selected functions, every spec and proof
+function (any verdict may rest on their facts, and a confirmation by proof
+on any established lemma), and then, round by round, each executable
+function whose contract a run's verdicts call (`CallDependencies`, proof
+blocks' `Callees`), until none is new. The fixpoints then run as for the
+whole file over the verdicts there are; the diagnostics of functions not
+selected stay, hidden, for what they establish. A text run ends with a summary line: `printDiagnostics` counts each verdict
 it prints into the run's `VerifySummary` (a first error that carries a
 verdict counts, a `--verbose` spec axiom line does not), and the driver
 prints the counts of every file of the run with its time.
+`--time-report` measures where that time goes. Each function's task gives
+its backends one `BackendTimes` (`Backend/Timing.h`, `VerifyBackend::setTimes`,
+which a portfolio, a race, and BMC forward to their solvers): the wall time
+in `VerifyBackend::verify` is solving and its induction loop induction, and
+`certifyCounterexample` adds each check's time through `CertifyLimits::Times`
+(summed, so with several jobs it may exceed solving). The driver times the
+task, the unrolling of `failureNotes`, and each confirmation by proof (added
+to the function that proposed it, `Confirmation::Function`); lowering is the
+task's time outside the backends and the unrolling. The run's conversion,
+verification, and settling are the times between `Verifier`'s construction,
+the converted functions, the end of the tasks, and the report. Backends
+without a sink (the unroller, those of the confirmations by proof and of the
+`cppverify::recommends` pass) count nothing, so no time is counted twice.
 Its message names the construct as C++ does (`unsupportedConstruct` for the
 statements and expressions without a site of their own; Clang's class name
 only in parentheses for those it has no name for), and each error is raised
@@ -2494,7 +2542,39 @@ again where it is used.
    - a trusted function reports `Trusted`; an unmarked contract without a
      definition draws a warning, and every caller whose proof relies on it
      (or on any callee contract whose verification failed) is demoted to
-     `Unresolved` with reason `callee.contract`;
+     `Unresolved` with reason `callee.contract`. A function is trusted by
+     the mark on its definition, or on any declaration when it has none
+     (`ASTConverter::convertFunction`: an inherited mark does not count);
+   - in a run over several files (`VerifyOptions::CrossFile`, a
+     `CrossFileRun` the driver creates when given more than one file), an
+     unmarked contract without a definition is provisionally established
+     instead (`Verifier::Externals`). After the fixpoints below, each proof
+     records the external contracts it rests on, through the file's own
+     contracts' verdicts (`ExternalOf`), and each contract the file
+     verifies is offered with whether the file establishes it and on which
+     external contracts that rests (`DefinedContracts`), keyed by identity
+     and the contract as written (`ASTConverter::contractText`). The file's
+     results are rendered while its AST lives (`renderReport`): each line
+     as verified and, for a proof that rests on external contracts, as
+     `demote` would make it, with a placeholder for the contracts, both
+     counted for the summary. Once every file is verified,
+     `CrossFileRun::finish` establishes contracts by a least fixpoint over
+     the files (a contract once every definition of it is established in
+     its file and the external contracts that rests on are), prints each
+     file's lines with the demoted form where a contract a proof rests on is
+     not established, drops the warning of a contract some file defines and
+     the findings of a demoted proof (but those of the entry state), and
+     counts the files that do not succeed. The settlement is
+     `ContractSettlement`, shared with the check of files verified apart:
+     with `VerifyOptions::ContractsOut` (`--contracts-out`, and
+     `-fverify-contracts-out` through `startCppVerifyAsync` in the compile
+     path) a file's externals are provisional the same way, each proof that
+     rests on them gets `[assumes=f]`, and `recordContracts` writes a
+     `cppverify.contracts/1` JSON record of the contracts it verifies (key,
+     name, established, assumes) and of its proofs that rest on externals
+     (function, the location of its declaration, the contracts).
+     `checkContracts` (`--check-contracts`) reads the records, settles them,
+     and prints each proof whose assumed contract is not established;
    - `[trusts=...]` lists the trusted contracts a proof uses, closed
      transitively over verified callees (JSON `"trusts"`);
    - one fixpoint settles the reasons: a verdict relying on a spec whose
@@ -2658,6 +2738,24 @@ the whole query had refuted the function in milliseconds: model search over
 quantified heap queries depends on the solver's search order, and 16 of 40
 random seeds took the full 30 s.
 
+With `--max-failures=N` (`BackendExecutionOptions::MaxFailures`, Z3 only)
+the obligations report up to `N` failures (0: all), and the result of the
+first carries the others (`VerifyResult::MoreFailures`), which the driver
+prints after it, each with its notes, as diagnostics marked `Additional` that
+the summary does not count. `verifyObligations` given a number of failures to
+report solves each obligation after the first failure in the executions that
+pass every earlier failing one, as Boogie's subsumption assumes an assertion
+after checking it (`verifyPastEarlier`: the obligation's counterexample query
+conjoined with those obligations' goals, never cached): alone, its
+counterexample could start where an earlier check already fails, and a check
+that fails only there would be reported though fixing the earlier one fixes
+it. Checks not settled are not assumed, so nothing proved past the failures
+rests on a check that may not hold. A serial run stops after the `N`th
+failure; a parallel one solves every obligation alone and then solves each
+failure after the first again, in order. Without a number, every obligation
+is solved alone, as the portfolio's comparison of Z3's and cvc5's results
+needs.
+
 The whole query of a module without logic functions is a probe of a fixed
 amount of work, `WholeProbeUnits` (6 million) Z3 resource units, with the
 module's timeout as its bound in time, so where it stops depends neither on
diff --git a/docs/DESIGN.md b/docs/DESIGN.md
index dcff8d2b56..ea57b0106a 100644
--- a/docs/DESIGN.md
+++ b/docs/DESIGN.md
@@ -139,15 +139,32 @@ it is `Unresolved` with reason `callee.contract`.
 
 `[[cppverify::trusted]]` (a standard C++ attribute, like Verus's
 `#[verifier::external_body]`) marks a contract as assumed: on a declaration
-the contract holds at every call (whose preconditions are still checked); on
-a definition the body is compiled but not verified; on a proof function the
-postcondition is an axiom. A spec cannot be trusted, since its definition is
+the contract holds at every call that sees no definition (whose
+preconditions are still checked); on a definition the body is compiled but
+not verified; on a proof function the postcondition is an axiom. A
+definition that only inherits the mark from an earlier declaration, as
+Clang's attribute inheritance gives it, is verified (decision Q13 of the 0.2
+plan): before 0.2 the mark on a header's declaration stopped the
+verification of the definition, so a wrong body was never checked. A spec cannot be trusted, since its definition is
 its meaning. The mark is written on each function: `#pragma clang attribute`
 cannot apply it to a region. A trusted function reports `Trusted: f (contract assumed, not
 verified)`, and every verdict that relies on it, directly or through verified
 callees, carries `[trusts=f]`. A contract without a definition and without
 the mark is not assumed: a warning names it, and its callers are
-`Unresolved` with reason `callee.contract`. A trusted contract writes only
+`Unresolved` with reason `callee.contract`. In one run over several files,
+such a contract is settled across them, as Frama-C settles a property's
+status over the files of a project: a proof that rests on it, directly or
+through the file's own contracts, stands once the verification of its
+definition in another file establishes it (a contract established only
+through other files' contracts once those are, starting from none), and is
+`Unresolved` with `callee.contract` otherwise. A declaration matches a
+definition with the same function and the same contract as written. Files
+verified apart (a build verifying each object) record what they verify and
+assume (`--contracts-out`, `-fverify-contracts-out`): such a contract holds
+there for now, a proof that rests on it says so (`[assumes=f]`), and
+`cpp-verify --check-contracts` settles the records as one run does, failing
+for each proof whose assumed contract is not established, as the plan's
+link check. A trusted contract writes only
 its `cppverify::modifies` footprints; without them it writes nothing through a pointer
 or reference to const, and is taken to write the whole heap through a
 mutable one (see `cppverify::modifies` below).
@@ -1894,7 +1911,24 @@ int safe_fib(int n) cppverify::pre(...) cppverify::post(cppverify::result == fib
 - `Failed`: a counterexample that holds when every logical function is
   evaluated at its true definition. It is relative to the declared
   abstractions only: callee contracts, loop invariants, and `cppverify::modifies`
-  frames.
+  frames. A counterexample that passes through a loop starts from any state
+  the loop's invariants allow, so such a failure says so in a note, and the
+  verifier unrolls each loop up to `--confirm-bound` iterations (default 10)
+  to look for an execution that fails the same check, as G5 proposed with
+  CBMC's and Kani's unrolling: it reports that execution, or that unrolling
+  proves the check, or that none fails it within the bound. The execution
+  passes every failing check before this one, and a check that holds in the
+  executions that pass them says so and names one that fails. Unrolling keeps
+  no loop invariant and no measure, so their failures are not confirmed. The verdict stays `Failed`
+  (decision Q12 of the 0.2 plan): the claim is not proved, and the note
+  carries the difference. A failure of a function whose loop has no
+  `cppverify::decreases` names that loop too.
+- Several failures of one function (`--max-failures`): after the first,
+  a check is a failure only when an execution that passes the failing checks
+  before it fails it, as Boogie assumes an assertion once checked and Dafny
+  then reports each failing assertion. Each such failure is a bug of its
+  own: one that fails only after an earlier failure disappears with its fix,
+  and is not reported. Checks not settled are not assumed.
 - Anything else is `Unresolved` with a reason. `spec.fuel`: every
   counterexample found relies on a recursive spec beyond what refinement could
   unfold, the automatic inductions did not prove it, and no counterexample
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 fe476e306d..21970d2e8e 100644
--- a/website/source/book/part-ii/ch15-toolchain-and-flags.rst
+++ b/website/source/book/part-ii/ch15-toolchain-and-flags.rst
@@ -44,6 +44,25 @@ Other flags
   check (``Verified: spec axiom: twice``), which the default leaves out
 - ``cpp-verify --list-functions`` — list the functions a run would verify,
   with their locations and kinds, and verify none
+- ``cpp-verify --function=PATTERN`` — report only the functions whose names
+  match a glob pattern (repeatable), with the same verdicts as a whole run:
+  what they rely on is verified too, and nothing else that is executable
+- ``cpp-verify --time-report`` — after the verdicts, where the run and each
+  function spent their time (lowering, solving, induction, certification,
+  confirmation), the busiest function first; on a terminal a progress line
+  counts the functions done (``--progress`` shows it anywhere)
+- ``cpp-verify --contracts-out=FILE`` and ``clang++ -fverify-contracts-out=FILE``
+  — record the contracts a file verifies and those it assumes from other
+  files; ``cpp-verify --check-contracts RECORD...`` checks the records
+  together (see :doc:`ch17-backends-modular-calls`)
+- ``cpp-verify --confirm-bound=N`` — for a failure whose counterexample passes
+  through a loop, unroll each loop up to ``N`` iterations (default 10, ``0``
+  skips it) to find an execution that fails or prove that none does (see
+  :doc:`ch16-when-verification-fails`)
+- ``cpp-verify --max-failures=N`` — report the first ``N`` checks of a
+  function that fail (``0``: every one), each with its own counterexample,
+  instead of the first only; a check after a failure counts only when an
+  execution that passes the failing checks before it fails it
 - ``cpp-verify --backend={z3,cvc5,portfolio,race,bmc,lean}`` — verification
   engine: Z3 (the default), cvc5, both with agreement required
   (``portfolio``), both at once with the first proof or certified
diff --git a/website/source/book/part-ii/ch16-when-verification-fails.rst b/website/source/book/part-ii/ch16-when-verification-fails.rst
index 6bd6aa9d8a..4a056a2812 100644
--- a/website/source/book/part-ii/ch16-when-verification-fails.rst
+++ b/website/source/book/part-ii/ch16-when-verification-fails.rst
@@ -29,6 +29,47 @@ text, and IR dumps intentionally make the stream mixed. Malformed display bytes
 are replaced with the Unicode replacement character, so JSON output remains
 valid UTF-8.
 
+A counterexample after a loop is only as real as the loop's invariants. At
+the loop, the verifier knows what the invariants say and nothing else, so a
+loop with too weak an invariant fails a correct function:
+
+.. code-block:: cpp
+
+   namespace cv = cppverify;
+
+   int count_up(int n)
+     cv::pre(n >= 0 && n <= 5)
+     cv::post(cv::result == n)
+   {
+     int c = 0;
+     while (c < n)
+       cv::decreases(n - c)
+     {
+       c = c + 1;
+     }
+     return c;
+   }
+
+.. code-block:: text
+
+   count_up.cpp:5:23: error: verification failed: count_up [fn_...::postcondition@5:23] (counterexample: result [ssa=__result_1] [type=i32] = 1, c [ssa=c_1] [type=i32] = 0, c [ssa=c_2] [type=i32] = 1, c [ssa=c_3] [type=i32] = 1, n [ssa=n_0] [type=i32] = 0; trace: loop.entry@8:3 -> loop.exit@8:3 -> return.return@13:3 value=1) [backend=z3] [reason=counterexample]
+   note: the counterexample's state at the loop at 8:3 is any state its invariants allow, not necessarily one an execution reaches
+   note: no execution fails this check: every loop ends within 5 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof
+
+The first note says where the counterexample's state comes from; the second
+is what unrolling the loop found about the same check (``--confirm-bound``,
+10 iterations by default): here, that every execution passes it, so the
+invariant is what is missing (``cv::invariant(0 <= c && c <= n)``). When
+unrolling finds an execution that fails the check, the note gives that
+execution and the number of iterations, and the bug is in the code or the
+contract, not in the invariant. When the check fails only in executions that
+fail an earlier check first, the note names that check: fix it first.
+
+A function reports its first failing check. To see every one, each with its
+own counterexample, run ``cpp-verify --max-failures=0``: a check after a
+failure is reported only when some execution that passes the earlier failing
+checks fails it, so each line is a bug of its own.
+
 An undecided query is different from a counterexample. ``Unresolved`` with
 reason ``solver.timeout``, ``solver.resource-limit``, ``solver.memory-limit``,
 or ``solver.unknown`` means Z3 timed out, exhausted an explicit resource/query
diff --git a/website/source/book/part-ii/ch17-backends-modular-calls.rst b/website/source/book/part-ii/ch17-backends-modular-calls.rst
index e1ae4a965d..cd186a853a 100644
--- a/website/source/book/part-ii/ch17-backends-modular-calls.rst
+++ b/website/source/book/part-ii/ch17-backends-modular-calls.rst
@@ -1371,6 +1371,16 @@ are ``Unresolved`` with reason ``callee.contract``, and a warning points at
 the declaration. A forgotten definition therefore cannot silently turn into
 an axiom.
 
+Where the definition is in another file, verify the files together:
+``cpp-verify src/a.cpp src/mathx.cpp -- -Iinclude``. The run settles the
+contract a header declares against the verification of its definition, so
+``a.cpp``'s callers of ``clamp100`` are verified when ``mathx.cpp``'s body
+meets the contract, and ``Unresolved`` when it does not. A build that verifies each object
+records them instead (``-fverify-contracts-out=FILE``) and checks the
+records together at the end (``cpp-verify --check-contracts``). Mark a
+header's declaration trusted only for a definition outside the program: on
+the definition, which inherits the mark, the body is still verified.
+
 The same boundary exists in other verifiers. Verus assumes the specification
 of a function marked ``#[verifier::external_body]``. Frama-C assumes the
 contract of a function without a body when it proves the callers. CppVerify
diff --git a/website/source/language/functions-loops.rst b/website/source/language/functions-loops.rst
index 4c69734279..f82e325f61 100644
--- a/website/source/language/functions-loops.rst
+++ b/website/source/language/functions-loops.rst
@@ -89,9 +89,11 @@ outside the verified subset, or a lemma you decide to assume.
    trusted.cpp:16:39: Trusted: sq_nonnegative (contract assumed, not verified)
    Verified: sample [backend=z3] [trusts=clamp_byte,read_sensor,sq_nonnegative]
 
-- On a declaration, the contract is assumed at every call; the preconditions
-  are still checked there.
-- On a definition, the body is compiled but not verified.
+- On a declaration, the contract is assumed at every call that sees no
+  definition; the preconditions are still checked there.
+- On a definition, the body is compiled but not verified. A definition that
+  only inherits the mark from an earlier declaration (a header's, say) is
+  verified: to leave a body unverified, mark the definition itself.
 - On a proof function, the postcondition is an axiom.
 - A spec function cannot be trusted: its definition is its meaning, so there
   is nothing to assume. The attribute is an error there.
@@ -101,9 +103,8 @@ outside the verified subset, or a lemma you decide to assume.
   ``[trusts=...]`` (JSON ``"trusts"``), transitively through verified
   callees: a caller of ``sample`` carries the same three names.
 
-The mark may appear on any declaration of the function. Without it, a
-contract with no definition is neither proved nor vouched for, so it proves
-nothing:
+Without the mark, a contract with no definition is neither proved nor
+vouched for, so it proves nothing:
 
 .. code-block:: cpp
 
@@ -129,6 +130,88 @@ that contradicts the state of a call (no result can satisfy it) would make
 everything after the call hold vacuously; CppVerify reports that case with
 ``[vacuous]`` and a warning at the call (see :doc:`tooling`).
 
+Contracts across files
+----------------------
+
+Real code declares a function with its contract in a header and defines it
+in one file. Verified alone, a file that sees only the declaration has no
+definition, as above. Verified together in one run, the files settle it: a
+proof that rests on the contract stands once the verification of its
+definition establishes it, and is ``Unresolved`` with ``callee.contract``
+otherwise, as within one file.
+
+.. cppverify-example: fragment
+.. code-block:: cpp
+
+   // include/mathx.h
+   int clamp100(int x)
+     cv::post(cv::result >= 0 && cv::result <= 100);
+
+   // src/mathx.cpp
+   #include "mathx.h"
+
+   int clamp100(int x)
+   {
+     if (x < 0)
+       return 0;
+     if (x > 100)
+       return 101;
+     return x;
+   }
+
+   // src/a.cpp
+   #include "mathx.h"
+
+   int scaled(int x)
+     cv::post(cv::result >= 0 && cv::result <= 200)
+   {
+     return 2 * clamp100(x);
+   }
+
+.. code-block:: text
+
+   $ cpp-verify src/a.cpp src/mathx.cpp -- -Iinclude
+   Unresolved: scaled [backend=z3] [reason=callee.contract] (relies on the contract of clamp100, which its verification in src/mathx.cpp does not establish)
+   include/mathx.h:2:42: error: verification failed: clamp100 [fn_...::postcondition@2:42] (counterexample: result [ssa=__result_1] [type=i32] = 101, x [ssa=x_0] [type=i32] = 101; ...) [backend=z3] [reason=counterexample]
+   Summary: 1 failed, 1 unresolved (callee.contract 1) in 0.0 s
+
+With ``return 100;`` both verify, and the warning that ``clamp100`` has no
+definition is not printed. The results of each file are held until every
+file is verified, then printed in the order the files are given.
+
+- A declaration matches a definition with the same function (its mangled
+  name) and the same contract as written. A file that states another
+  contract for the function does not match: its callers are unresolved, and
+  the message says that the definition is verified against another
+  contract.
+- A contract whose proof rests on contracts of other files is established
+  only once they are. Two files whose proofs rest on each other's contracts
+  establish nothing, as proofs that rest on themselves never do.
+- A trusted declaration stays an assumption, with ``[trusts=...]`` on what
+  relies on it; only its definition, where it is verified, can find a wrong
+  contract.
+
+Files verified apart, as a build verifies each object, settle their
+contracts with a check: each file records what it verifies and what it
+assumes, and ``cpp-verify --check-contracts`` settles the records as one run
+does. A proof that rests on a contract of another file says so, as
+``[assumes=clamp100]``, and the warning that the contract has no definition
+is not printed:
+
+.. code-block:: text
+
+   $ clang++ -fverify-contracts -fverify-contracts-out=a.o.cppverify -c src/a.cpp -o a.o -Iinclude
+   Verified: scaled [backend=z3] [assumes=clamp100]
+   $ clang++ -fverify-contracts -fverify-contracts-out=mathx.o.cppverify -c src/mathx.cpp -o mathx.o -Iinclude
+   include/mathx.h:2:42: error: verification failed: clamp100 [...]
+   $ cpp-verify --check-contracts a.o.cppverify mathx.o.cppverify
+   src/a.cpp:3:5: error: the proof of scaled relies on the contract of clamp100, which its verification in src/mathx.cpp does not establish
+   Contracts: 1 proof rests on contracts of other files, 1 on one not established
+
+``cpp-verify --contracts-out=FILE`` records one file the same way. The check
+exits with a non-zero status when a proof relies on a contract not
+established: run it as a build's last step, beside the link.
+
 An uncontracted, non-recursive, loop-free ``constexpr`` definition may be
 lifted for use in contract expressions; a recursive one used with symbolic
 arguments is rejected. It is lifted where verification uses it: in a contract, a
@@ -638,6 +721,83 @@ rest of the loop, and a ``continue`` goes to the condition, where the
 invariant must first hold. ``cppverify::ghost`` code cannot leave an
 executable loop.
 
+A failure is relative to the loop's invariants: after the loop, and at the
+start of an iteration, the verifier knows only what they say, so a
+counterexample there may start from a state no execution reaches. Such a
+failure says so in a note, and the verifier then unrolls each loop, up to
+``--confirm-bound`` iterations (10 by default, ``0`` to skip), to look for an
+execution that fails the same check, with callees still by their contracts:
+
+.. code-block:: cpp
+
+   namespace cv = cppverify;
+
+   int count_up(int n)
+     cv::pre(n >= 0 && n <= 5)
+     cv::post(cv::result == n)
+   {
+     int c = 0;
+     while (c < n)
+       cv::decreases(n - c)
+     {
+       c = c + 1;
+     }
+     return c;
+   }
+
+.. code-block:: text
+
+   count_up.cpp:5:23: error: verification failed: count_up [fn_...::postcondition@5:23] (counterexample: result [ssa=__result_1] [type=i32] = 1, c [ssa=c_1] [type=i32] = 0, c [ssa=c_2] [type=i32] = 1, c [ssa=c_3] [type=i32] = 1, n [ssa=n_0] [type=i32] = 0; trace: loop.entry@8:3 -> loop.exit@8:3 -> return.return@13:3 value=1) [backend=z3] [reason=counterexample]
+   note: the counterexample's state at the loop at 8:3 is any state its invariants allow, not necessarily one an execution reaches
+   note: no execution fails this check: every loop ends within 5 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof
+
+Here the loop has no invariant, so after it ``c`` may be anything; the fix is
+``cv::invariant(0 <= c && c <= n)``. When unrolling finds an execution that
+fails the check (in any iteration's copy of it, for a check in the loop's
+body), the note says within how many iterations and gives that execution;
+when it finds neither a failure nor a proof within the bound, the note says
+that no execution fails the check within that many iterations. The execution
+a note gives passes the checks before this one that fail, since one that
+fails an earlier check never reaches it. When the check holds in every
+execution that passes them, the note says so and names an earlier check that
+fails, the one to fix first (``--max-failures=0`` reports it with its own
+counterexample, see :doc:`tooling`):
+
+.. code-block:: cpp
+
+   namespace cv = cppverify;
+
+   int divide(int a, int n)
+     cv::pre(n >= 0 && n <= 5)
+     cv::post(true)
+   {
+     int c = 0;
+     int q = 0;
+     while (c < n)
+       cv::invariant(0 <= c && c <= n)
+       cv::decreases(n - c)
+     {
+       q = a / (1 - c);
+       c = c + 1;
+     }
+     return q;
+   }
+
+.. code-block:: text
+
+   divide.cpp:13:7: error: verification failed: divide [fn_...::overflow@13:7] (counterexample: a [ssa=a_0] [type=i32] = -2147483648, c [ssa=c_1] [type=i32] = 0, c [ssa=c_2] [type=i32] = 2, n [ssa=n_0] [type=i32] = 3, q [ssa=q_1] [type=i32] = 0; trace: loop.entry@9:3 -> loop.inductive iteration@9:3 condition=true) [backend=z3] [reason=counterexample]
+   note: the counterexample's state at the loop at 9:3 is any state its invariants allow, not necessarily one an execution reaches
+   note: no execution fails this check without failing an earlier one first (the division-by-zero check at 13:7 fails): those that pass the checks before it end every loop within 2 iterations, and unrolling proves it there
+
+``INT_MIN / -1`` needs ``c == 2``, and every execution that gets there
+divides by ``1 - 1`` one iteration sooner.
+
+Unrolling keeps no invariant and no measure, so a failed invariant or
+measure gets the first note only. The verdict stays ``verification failed`` either way, since
+the claim is not proved. A failure of a function
+whose loop has no ``cppverify::decreases`` also notes that loop: with a
+proof, the function would still be ``Unresolved`` (``decreases.missing``).
+
 A range-based ``for`` loop over an array (a local array, an array member,
 a constant table) visits its elements in order. Its contract names the
 position, ``cppverify::index``, the number of elements before the current
diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst
index 5e2ccff277..4b081ebfa8 100644
--- a/website/source/language/limitations.rst
+++ b/website/source/language/limitations.rst
@@ -676,7 +676,11 @@ CppVerify does not yet ship comprehensive libc or C++ standard-library models:
 of the standard library it knows ``std::min`` and ``std::max`` of two
 integers (:doc:`functions-loops`), and any other of its functions is an
 error naming it. An uncontracted call fails closed; a contract is assumed
-only when it is marked ``[[cppverify::trusted]]``. Contracts are not saved in precompiled
+only when it is marked ``[[cppverify::trusted]]``, or, in one run over
+several files, once the verification of its definition in another of them
+establishes it, and for files verified apart once
+``cpp-verify --check-contracts`` finds it established
+(:doc:`functions-loops`). Contracts are not saved in precompiled
 headers: a function declared in a PCH has no contract for the verifier, so a
 contracted function that calls it fails closed (``call to function without a
 verification contract``).
diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst
index 12094a6595..c8e2cf5a3a 100644
--- a/website/source/language/tooling.rst
+++ b/website/source/language/tooling.rst
@@ -11,7 +11,12 @@ Standalone verifier
    cpp-verify --quiet file.cpp
    cpp-verify --verbose file.cpp
    cpp-verify --list-functions file.cpp
+   cpp-verify --function='parse_*' --function=encode file.cpp
+   cpp-verify --time-report file.cpp
    cpp-verify file.cpp -- -I include -DNDEBUG
+   cpp-verify src/a.cpp src/mathx.cpp -- -I include
+   cpp-verify --contracts-out=a.cppverify src/a.cpp -- -I include
+   cpp-verify --check-contracts a.cppverify mathx.cppverify
    cpp-verify --backend=z3 file.cpp
    cpp-verify --backend=cvc5 file.cpp
    cpp-verify --backend=portfolio file.cpp
@@ -24,6 +29,8 @@ Standalone verifier
    cpp-verify --no-check-ub file.cpp
    cpp-verify --profile-quantifiers file.cpp
    cpp-verify --timeout=20000 file.cpp
+   cpp-verify --confirm-bound=4 file.cpp
+   cpp-verify --max-failures=0 file.cpp
    cpp-verify --jobs=4 --proof-cache=.cppverify-cache file.cpp
    cpp-verify --solver-rlimit=500000 --max-query-nodes=50000 file.cpp
    cpp-verify --memory-limit=4096 file.cpp
@@ -40,6 +47,23 @@ flags of a listed neighbour. Without a database the file is compiled with those
 alone. Flags after ``--`` replace the database, and ``--extra-arg=FLAG`` adds one flag either
 way.
 
+Several files given to one run are verified one after the other and
+settled together: a contract one file declares without a definition holds
+for a proof once its definition's verification in another file establishes
+it (see :doc:`functions-loops`). Their results are printed once every file
+is verified, in the order given.
+
+Files verified apart record their contracts instead:
+``--contracts-out=FILE`` (or ``clang++ -fverify-contracts
+-fverify-contracts-out=FILE``) writes a ``cppverify.contracts/1`` record of
+the contracts the file verifies, whether it establishes each and on which
+contracts of other files that rests, and of its proofs that rest on
+contracts of other files, which say so (``[assumes=f]``).
+``cpp-verify --check-contracts RECORD...`` settles the records and prints
+each proof that relies on a contract not established, at the proof's
+function, then a line that counts them; its exit status is non-zero when
+there is one.
+
 Input files and compiler errors
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -213,6 +237,77 @@ whole output, of ``--list-functions``, and of archive replay
    summary.cpp:5:5: function add_one
    summary.cpp:12:5: function add_two
 
+``--function=PATTERN`` reports only the functions whose names match the glob
+pattern (``*``, ``?``, ``[...]``; repeatable, a function matching any is
+reported), as ``Verified`` and the other lines print the name: ``Ring::push``,
+``total<short>``; an inductive predicate is reported with the checks generated
+for it (its step's termination and induction, its rule proofs). Every verdict
+it reports is the one a run of the whole file gives: the functions whose
+contracts those verdicts rely on are verified too, round by round, and so
+are all spec and proof functions, whose facts any
+proof may use; their results are not printed, and a selected function that
+relies on a callee whose verification fails is ``Unresolved`` with
+``callee.contract`` exactly as in a whole run. An executable function no
+reported verdict relies on is not verified at all. The exit status follows
+what is reported: 0 when every reported verdict is a proof. A pattern that
+matches no function is an error. With ``--list-functions`` it narrows the
+listing.
+
+``--time-report`` adds, after a file's verdicts, where its run spent its time,
+then each function it reported, the busiest first. Here ``small_power``'s
+counterexample is confirmed by a proof after inductions are tried, ``grows``
+is proved by induction, and ``after_loop`` fails after a loop that
+unrolling then checks:
+
+.. code-block:: text
+
+   $ cpp-verify --time-report file.cpp
+   ...
+   Time report (seconds): conversion 0.001, verification 4.412, settling 0.151
+        total  lowering   solving  induction  certification  confirmation  function
+        4.559     0.001     4.408      3.917          7.577         0.150  small_power
+        1.767     0.001     1.766      0.014          3.292         0.000  grows
+        0.062     0.002     0.022      0.000          0.000         0.038  after_loop
+        0.027     0.001     0.026      0.000          0.000         0.000  fibo
+        0.026     0.001     0.025      0.000          0.000         0.000  proved
+        0.022     0.001     0.021      0.000          0.000         0.000  pow2
+   Summary: 4 verified, 2 failed in 4.6 s
+
+For the run:
+
+- **conversion**: from the parsed file to the functions the verifier
+  verifies (Clang's parsing comes before it; the summary's time covers it);
+- **verification**: verifying every function, at once with several jobs;
+- **settling**: what follows: the verdicts that rest on other functions'
+  contracts and on spec facts, confirmations by proof, Lean certification.
+
+For a function:
+
+- **total**: its verification, and the confirmations of its counterexamples
+  by proof that run after every function is verified;
+- **lowering**: preparing its checks, and passivizing and lowering them to
+  obligations;
+- **solving**: in the backends: encoding, solving, checking counterexamples,
+  inductions, and a proof's vacuity checks;
+- **induction**: the part of solving spent on automatic inductions;
+- **certification**: checking the solvers' counterexamples against the true
+  definitions, summed over the checks; with several jobs they run at once,
+  so it can exceed solving;
+- **confirmation**: unrolling the loops after a failure (``--confirm-bound``)
+  and confirming a counterexample by proof.
+
+A function's total is its lowering, solving, and confirmation. With
+``--diagnostics-format=json`` the report is records of the schema
+``cppverify.time/1``: one for the run, whose ``seconds`` has
+``conversion``, ``verification``, and ``settling``, then one per function,
+with ``function`` and the six ``seconds`` of its row. The report needs source
+verification (not ``--obligation-in``).
+
+On a terminal, a line on standard error counts the functions done as they
+finish (``[12/40] parse_header``); the results follow once every verdict is
+settled. ``--progress`` shows the line anywhere, and ``--progress=false``
+hides it.
+
 ``cpp-verify --help`` shows each time limit's default (``--timeout``,
 30000 ms).
 
@@ -955,6 +1050,55 @@ False guards are omitted; a guard the model does not determine is retained with
 JSON ``"active": null`` rather than an invented path choice. Archives preserve
 the same names, ranges, IDs, and trace data during replay.
 
+A failure may carry notes, printed after it as ``note:`` lines and in JSON as
+``notes``: a counterexample that passes through a loop starts from any state
+the loop's invariants allow, and what unrolling each loop then finds about
+the same check, within ``--confirm-bound`` iterations (default 10; ``0``
+skips it; only with the solver backends, since BMC unrolls already and Lean
+runs no solver): an execution that fails it, a proof that none does, or no
+failure within the bound. The search takes at most one query timeout. Unrolling
+drops the loops' invariants and measures, so a failure of one gets no
+search: it would find no copy of the check at any bound. A loop without
+``cppverify::decreases`` is noted too (see :doc:`functions-loops`).
+
+A function reports one failure: the first check that fails, in the order an
+execution meets them. ``--max-failures=N`` reports the first ``N``, and
+``--max-failures=0`` every one, each with its own counterexample and notes,
+as Dafny reports every failing assertion of a method (only with
+``--backend=z3``). A check after the first failure is solved in the
+executions that pass the failing checks before it, as Boogie assumes an
+assertion once it has checked it: its counterexample reaches it without
+failing an earlier check, and a check that fails only where an earlier one
+fails is not reported, since fixing that one fixes it. The summary still
+counts each function once:
+
+.. cppverify-example: flags --max-failures=0
+.. code-block:: cpp
+
+   namespace cv = cppverify;
+
+   int three_bugs(int x, int y)
+     cv::pre(x < 1000 && y < 1000)
+     cv::post(cv::result > 0)
+   {
+     int q = 10 / y;
+     int r = x + q;
+     return r;
+   }
+
+.. code-block:: text
+
+   $ cpp-verify --max-failures=0 three_bugs.cpp
+   three_bugs.cpp:7:3: error: verification failed: three_bugs [fn_...::division-by-zero@7:3] (counterexample: x [ssa=x_0] [type=i32] = 0, y [ssa=y_0] [type=i32] = 0) [backend=z3] [reason=counterexample]
+   three_bugs.cpp:8:3: error: verification failed: three_bugs [fn_...::overflow@8:3] (counterexample: q [ssa=q_1] [type=i32] = -1, x [ssa=x_0] [type=i32] = -2147483648, y [ssa=y_0] [type=i32] = -9) [backend=z3] [reason=counterexample]
+   three_bugs.cpp:5:23: error: verification failed: three_bugs [fn_...::postcondition@5:23] (counterexample: result [ssa=__result_1] [type=i32] = 0, q [ssa=q_1] [type=i32] = 0, r [ssa=r_1] [type=i32] = 0, x [ssa=x_0] [type=i32] = 0, y [ssa=y_0] [type=i32] = 11; trace: return.return@9:3 value=0) [backend=z3] [reason=counterexample]
+   Summary: 1 failed in 0.0 s
+
+Without the option only the first line is printed. The overflow's
+counterexample divides by ``y = -9``, not by zero, and the postcondition's
+returns from an execution with no undefined operation. In JSON each failure
+is a record of its own.
+
 Each non-success verification result also carries a stable reason code. Current
 codes include ``counterexample``, ``solver.timeout``, ``solver.unknown``,
 ``solver.resource-limit``, ``solver.memory-limit``, ``solver.unavailable``,
diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst
index 58d1cfe2aa..8864541b71 100644
--- a/website/source/release-notes.rst
+++ b/website/source/release-notes.rst
@@ -483,11 +483,51 @@ are errors at the statement (:doc:`language/functions-loops`).
 Running cpp-verify
 ~~~~~~~~~~~~~~~~~~
 
+**Counterexamples after a loop.** A failure whose counterexample passed
+through a loop looked like any other, though its state there came from the
+loop's invariants and no execution need reach it: the first loop most users
+write, without an invariant, failed with ``c = 0`` after ``while (c < n)``.
+Such a failure now says so in a note, and unrolling each loop then looks for
+an execution that fails the same check within ``--confirm-bound`` iterations
+(default 10): it gives that execution, or says that no execution fails the
+check (when unrolling proves it) or that none fails it within the bound. The
+execution it gives passes the failing checks before this one, and a check
+that holds in every execution that passes them is noted with an earlier
+check that fails. A failure of a function whose loop has no
+``cppverify::decreases`` names that loop too
+(:doc:`language/functions-loops`).
+
+**Contracts across files.** A contract declared in a header and defined in
+another file left every caller ``Unresolved [callee.contract]``, even when
+one run verified both files, and the warning's advice,
+``[[cppverify::trusted]]`` on the declaration, also stopped the verification
+of the definition, which inherited the mark, so a wrong body was never
+checked. Now one run over several files settles such a contract: a proof
+that rests on it stands once the verification of its definition in another
+file establishes it, and is ``Unresolved`` with ``callee.contract``
+otherwise, naming the file. Files verified apart, as a build verifies each
+object, record their contracts (``clang++ -fverify-contracts-out=FILE``,
+``cpp-verify --contracts-out=FILE``), and ``cpp-verify --check-contracts``
+settles the records the same way, failing for each proof whose assumed
+contract is not established. A definition is trusted only by a mark of its
+own, so a trusted header declaration no longer hides it
+(:doc:`language/functions-loops`).
+
+**Every failure of a function.** A function reported only its first failing
+check. ``--max-failures=N`` reports the first ``N`` (``0``: every one), each
+with its own counterexample and notes; a check after a failure is reported
+only when an execution that passes the earlier failing checks fails it, as
+Dafny reports every failing assertion (:doc:`language/tooling`).
+
 **A summary, and what to print.** A run now ends with one line that counts
 its verdicts by kind, with the reasons of the unresolved ones and the time it
 took (``Summary: 12 verified, 1 failed, 2 unresolved (spec.fuel 1,
 solver.timeout 1) in 3.2 s``). ``--quiet`` prints only what needs attention,
-``--list-functions`` lists what a run would verify without verifying it, and
+``--list-functions`` lists what a run would verify without verifying it,
+``--function=PATTERN`` reports only the functions a glob pattern matches,
+with the verdicts a whole run gives, ``--time-report`` says where the run and
+each function spent their time, a line on a terminal counts the functions
+done, and
 the ``Verified: spec axiom: f`` line of a spec that needs no check is printed
 only with ``--verbose``. ``--help`` shows the default of ``--timeout``
 (:doc:`language/tooling`).