Add a native property-testing engine with choice-sequence shrinking

Catch3's own property engine, independent of RapidCheck, next to the
existing CheckProperty API, which stays unchanged.

Strategies (Progmasoft/Catch3/Strategy/): a Strategy<T> builds a value
from a ChoiceSource, a stream of integer choices where 0 is always the
simplest decision. Gen:: provides Integers, Booleans, Floats (ranges,
NaN and infinities on request, edge values), Characters, Strings,
Utf8Strings, Vectors, UniqueVectors, Sets, Maps, Optionals, Tuples,
Construct, Permutations, Just, SampledFrom, OneOf, Frequency, Lazy and
Recursive; every strategy has Map, Filter and FlatMap.

Shrinking: the engine records the choices of a failing trial and
shrinks them, not the value, with deletion and zeroing of blocks,
binary search per choice with a neighbour step for non-monotone
conditions, sorting and moving value between neighbours. Replaying the
shrunk choices through the same strategies means mapped, filtered,
dependent and stateful inputs all shrink, and a shrunk input still
satisfies its filters.

ForAll([options,] strategy..., body) runs the trials (size rising over
the first half), then a targeted search when the body calls Target,
then checks Cover requirements. A failure report carries the
minimized input, the notes and a replay token (PropertyOptions::Replay)
that runs exactly that input. An example database (DatabasePath or
CATCH3_PROPERTY_DATABASE) replays stored failures first and drops them
once they pass. Bodies return bool, or void with CATCH3_PROPERTY_ASSERT
and CATCH3_PROPERTY_ASSUME, which return instead of throwing; Note,
Classify, Cover and Target record into a per-thread trial record.
CATCH3_CHECK_FOR_ALL and CATCH3_REQUIRE_FOR_ALL report through Catch2
and name the property after the test case for the database.

CheckStateful runs model-based command sequences against a model and
the system under test; preconditions and state-dependent arguments are
replayed during shrinking. Relations.hpp provides Equivalent
(differential), Metamorphic, RoundTrip and Idempotent bodies.

PropertyOptions, PropertyStatus, PropertyFailure and PropertyResult
gain fields and statuses at their ends (kInsufficientCoverage,
kGaveUp); existing designated initializers and reports are unchanged.
The engine's untemplated parts are compiled in ChoiceShrinker.cpp,
PropertyEngine.cpp and Context.cpp, and every build system (Bazel,
CMake, Meson, Xmake, Premake) lists the new files and tests.

Docs: progmasoft-properties.md describes the engine,
progmasoft-roadmap.md the steps that follow (the standalone catch3
runner, mocking, per-test coverage, change-impact selection and
prioritization, mutation testing, guided test generation). The
.clang-format comment names Progmasoft C++ Style instead of Visual X#.

Verified with clang-cl 23 through CMake: ProgmasoftSelfTest passes, 57
test cases and 75,461 assertions, including the shrinking results
(1001 for x <= 1000, { 10 }, { 0, 0, 0 } through FlatMap, 102 through
a filter, { 0, 100 } for two arguments, four push(0) steps for a
queue that drops its fourth element, { 0, 0 } for a sort that loses
duplicates) and the database, replay, coverage and discard behaviour.

17 files changed, 3014 insertions, 2 deletions

diff --git a/src/Progmasoft/BUILD.bazel b/src/Progmasoft/BUILD.bazel
index 14a67bf6..b053c277 100644
--- a/src/Progmasoft/BUILD.bazel
+++ b/src/Progmasoft/BUILD.bazel
@@ -7,6 +7,9 @@ package(default_visibility = ["//visibility:public"])
 cc_library(
     name = "catch3",
     srcs = [
+        "ChoiceShrinker.cpp",
+        "Context.cpp",
+        "PropertyEngine.cpp",
         "Results.cpp",
         "Snapshot.cpp",
         "XmlWriter.cpp",
@@ -16,6 +19,7 @@ cc_library(
         "Catch3/Assertions.hpp",
         "Catch3/Detail/InvalidArgument.hpp",
         "Catch3/Detail/Sequence.hpp",
+        "Catch3/ForAll.hpp",
         "Catch3/Generator.hpp",
         "Catch3/Generators/Boolean.hpp",
         "Catch3/Generators/Element.hpp",
@@ -25,8 +29,16 @@ cc_library(
         "Catch3/Generators/Vector.hpp",
         "Catch3/Property.hpp",
         "Catch3/Random.hpp",
+        "Catch3/Relations.hpp",
         "Catch3/Results.hpp",
         "Catch3/Snapshot.hpp",
+        "Catch3/Stateful.hpp",
+        "Catch3/Strategy/ChoiceSource.hpp",
+        "Catch3/Strategy/Containers.hpp",
+        "Catch3/Strategy/Context.hpp",
+        "Catch3/Strategy/Engine.hpp",
+        "Catch3/Strategy/Numeric.hpp",
+        "Catch3/Strategy/Strategy.hpp",
         "Catch3/XmlWriter.hpp",
     ],
     copts = select({
diff --git a/src/Progmasoft/Catch3.hpp b/src/Progmasoft/Catch3.hpp
index 5fca369a..a1db1db7 100644
--- a/src/Progmasoft/Catch3.hpp
+++ b/src/Progmasoft/Catch3.hpp
@@ -6,6 +6,7 @@
 #include <catch2/catch_all.hpp>
 
 #include <Progmasoft/Catch3/Assertions.hpp>
+#include <Progmasoft/Catch3/ForAll.hpp>
 #include <Progmasoft/Catch3/Generator.hpp>
 #include <Progmasoft/Catch3/Generators/Boolean.hpp>
 #include <Progmasoft/Catch3/Generators/Element.hpp>
@@ -15,6 +16,13 @@
 #include <Progmasoft/Catch3/Generators/Vector.hpp>
 #include <Progmasoft/Catch3/Property.hpp>
 #include <Progmasoft/Catch3/Random.hpp>
+#include <Progmasoft/Catch3/Relations.hpp>
 #include <Progmasoft/Catch3/Results.hpp>
 #include <Progmasoft/Catch3/Snapshot.hpp>
+#include <Progmasoft/Catch3/Stateful.hpp>
+#include <Progmasoft/Catch3/Strategy/ChoiceSource.hpp>
+#include <Progmasoft/Catch3/Strategy/Containers.hpp>
+#include <Progmasoft/Catch3/Strategy/Context.hpp>
+#include <Progmasoft/Catch3/Strategy/Numeric.hpp>
+#include <Progmasoft/Catch3/Strategy/Strategy.hpp>
 #include <Progmasoft/Catch3/XmlWriter.hpp>
diff --git a/src/Progmasoft/Catch3/Assertions.hpp b/src/Progmasoft/Catch3/Assertions.hpp
index 668c086d..61fef04a 100644
--- a/src/Progmasoft/Catch3/Assertions.hpp
+++ b/src/Progmasoft/Catch3/Assertions.hpp
@@ -5,8 +5,14 @@
 #include <catch2/catch_message.hpp>
 #include <catch2/catch_test_macros.hpp>
 
+#include <catch2/interfaces/catch_interfaces_capture.hpp>
+
+#include <Progmasoft/Catch3/ForAll.hpp>
 #include <Progmasoft/Catch3/Property.hpp>
 #include <Progmasoft/Catch3/Snapshot.hpp>
+#include <Progmasoft/Catch3/Strategy/Context.hpp>
+
+#include <string>
 
 /// Runs a property and reports its replay seed and minimized counterexample.
 #define CATCH3_CHECK_PROPERTY( ... )                            \
@@ -25,3 +31,30 @@
         INFO( catch3SnapshotResult.Message );                               \
         CHECK( catch3SnapshotResult.Succeeded() );                          \
     } while ( false )
+
+/// Runs ForAll( [options,] strategy..., body ) under the name of the
+/// current test case, which keys the example database, and reports the
+/// result through Catch2: the minimized counterexample, its notes and its
+/// replay token on failure.
+#define CATCH3_CHECK_FOR_ALL( ... )                                          \
+    do {                                                                     \
+        const ::Progmasoft::Catch3::Detail::PropertyNameScope catch3Name(    \
+            ::Catch::getResultCapture().getCurrentTestName() + ":" +         \
+            std::to_string( __LINE__ ) );                                    \
+        const auto catch3ForAllResult =                                      \
+            ::Progmasoft::Catch3::ForAll( __VA_ARGS__ );                     \
+        INFO( catch3ForAllResult.Describe() );                               \
+        CHECK( catch3ForAllResult.Succeeded() );                             \
+    } while ( false )
+
+/// As CATCH3_CHECK_FOR_ALL, but ends the test case on failure.
+#define CATCH3_REQUIRE_FOR_ALL( ... )                                        \
+    do {                                                                     \
+        const ::Progmasoft::Catch3::Detail::PropertyNameScope catch3Name(    \
+            ::Catch::getResultCapture().getCurrentTestName() + ":" +         \
+            std::to_string( __LINE__ ) );                                    \
+        const auto catch3ForAllResult =                                      \
+            ::Progmasoft::Catch3::ForAll( __VA_ARGS__ );                     \
+        INFO( catch3ForAllResult.Describe() );                               \
+        REQUIRE( catch3ForAllResult.Succeeded() );                           \
+    } while ( false )
diff --git a/src/Progmasoft/Catch3/ForAll.hpp b/src/Progmasoft/Catch3/ForAll.hpp
new file mode 100644
index 00000000..e41bfdb6
--- /dev/null
+++ b/src/Progmasoft/Catch3/ForAll.hpp
@@ -0,0 +1,191 @@
+// Copyright (c) 2026 Progmasoft.
+// SPDX-License-Identifier: MPL-2.0 WITH AdditionRef-Progmasoft-Exception-1.1
+#pragma once
+
+#include <Progmasoft/Catch3/Property.hpp>
+#include <Progmasoft/Catch3/Strategy/Containers.hpp>
+#include <Progmasoft/Catch3/Strategy/Context.hpp>
+#include <Progmasoft/Catch3/Strategy/Engine.hpp>
+#include <Progmasoft/Catch3/Strategy/Strategy.hpp>
+#include <exception>
+#include <functional>
+#include <optional>
+#include <string>
+#include <tuple>
+#include <type_traits>
+#include <utility>
+
+namespace Progmasoft::Catch3
+{
+
+    namespace Detail
+    {
+
+        /// Runs a body on one input and turns what happened into a verdict.
+        /// A body returns bool, or void and fails through
+        /// CATCH3_PROPERTY_ASSERT; an exception from it is a failure.
+        template<typename Body, typename Tuple>
+        void
+        RunBody(Body &&body, const Tuple &values, TrialOutcome &outcome)
+        {
+            TrialRecordScope scope(outcome.Record);
+#if defined(__cpp_exceptions)
+            try
+            {
+#endif
+                using Result = decltype(std::apply(body, values));
+                if constexpr (std::is_void_v<Result>)
+                {
+                    std::apply(body, values);
+                }
+                else
+                {
+                    if (!static_cast<bool>(std::apply(body, values)))
+                    {
+                        RecordPropertyFailureMessage(
+                            "property returned false");
+                    }
+                }
+#if defined(__cpp_exceptions)
+            }
+            catch (const std::exception &exception)
+            {
+                RecordPropertyFailureMessage(
+                    std::string("property threw std::exception: ")
+                    + exception.what());
+            }
+            catch (...)
+            {
+                RecordPropertyFailureMessage(
+                    "property threw a non-standard exception");
+            }
+#endif
+            if (outcome.Record.Failure.has_value())
+            {
+                outcome.Verdict = TrialVerdict::kFailed;
+                outcome.Reason = *outcome.Record.Failure;
+            }
+            else if (outcome.Record.Discarded)
+            {
+                outcome.Verdict = TrialVerdict::kDiscarded;
+            }
+        }
+
+        /// Draws a value, catching what a strategy throws.
+        template<typename ValueType>
+        [[nodiscard]] std::optional<ValueType>
+        DrawGuarded(const Strategy<ValueType> &strategy,
+                    ChoiceSource &source,
+                    TrialOutcome &outcome)
+        {
+#if defined(__cpp_exceptions)
+            try
+            {
+#endif
+                auto value = strategy.Draw(source);
+                if (!value.has_value())
+                {
+                    outcome.Verdict = TrialVerdict::kInvalid;
+                }
+                return value;
+#if defined(__cpp_exceptions)
+            }
+            catch (const std::exception &exception)
+            {
+                outcome.Verdict = TrialVerdict::kErrored;
+                outcome.Reason = std::string("strategy threw std::exception: ")
+                                 + exception.what();
+            }
+            catch (...)
+            {
+                outcome.Verdict = TrialVerdict::kErrored;
+                outcome.Reason = "strategy threw a non-standard exception";
+            }
+            return std::nullopt;
+#endif
+        }
+
+        template<typename... ValueTypes>
+        [[nodiscard]] std::string
+        DescribeArguments(const std::tuple<ValueTypes...> &values)
+        {
+            if constexpr (sizeof...(ValueTypes) == 1)
+            {
+                return DescribeValue(std::get<0>(values));
+            }
+            else
+            {
+                return DescribeValue(values);
+            }
+        }
+
+        template<typename Body, typename... ValueTypes>
+        [[nodiscard]] PropertyResult
+        ForAllWith(const PropertyOptions &options,
+                   Body body,
+                   Strategy<ValueTypes>... strategies)
+        {
+            static_assert(sizeof...(ValueTypes) > 0,
+                          "ForAll needs at least one strategy");
+            const auto input = Gen::Tuples(std::move(strategies)...);
+            const TrialRunner runner =
+                [&](ChoiceSource &source, bool describe) -> TrialOutcome {
+                TrialOutcome outcome;
+                auto values = DrawGuarded(input, source, outcome);
+                if (!values.has_value())
+                {
+                    return outcome;
+                }
+                if (describe)
+                {
+                    outcome.Description = DescribeArguments(*values);
+                }
+                RunBody(body, std::as_const(*values), outcome);
+                return outcome;
+            };
+            return RunPropertyEngine(options, runner);
+        }
+
+        template<typename Type>
+        inline constexpr bool kIsPropertyOptions
+            = std::is_same_v<std::remove_cvref_t<Type>, PropertyOptions>;
+
+    } // namespace Detail
+
+    /// Checks that a property holds for values drawn from strategies.
+    ///
+    ///     ForAll([options,] strategy..., body)
+    ///
+    /// body receives one value per strategy, as const references. It
+    /// returns bool, or returns void and uses CATCH3_PROPERTY_ASSERT and
+    /// CATCH3_PROPERTY_ASSUME; Note, Classify, Cover and Target may be
+    /// called from it. A failure is minimized by shrinking the choices the
+    /// strategies made, and the report carries a replay token for exactly
+    /// the minimized input.
+    template<typename... Arguments>
+    [[nodiscard]] PropertyResult
+    ForAll(Arguments &&...arguments)
+    {
+        constexpr std::size_t kCount = sizeof...(Arguments);
+        static_assert(kCount >= 2, "ForAll needs strategies and a body");
+        auto all = std::forward_as_tuple(std::forward<Arguments>(arguments)...);
+        using First = std::tuple_element_t<0, std::tuple<Arguments...>>;
+        if constexpr (Detail::kIsPropertyOptions<First>)
+        {
+            return [&]<std::size_t... Index>(std::index_sequence<Index...>) {
+                return Detail::ForAllWith(std::get<0>(all),
+                                          std::get<kCount - 1U>(all),
+                                          std::get<Index + 1U>(all)...);
+            }(std::make_index_sequence<kCount - 2U>{});
+        }
+        else
+        {
+            return [&]<std::size_t... Index>(std::index_sequence<Index...>) {
+                return Detail::ForAllWith(PropertyOptions{},
+                                          std::get<kCount - 1U>(all),
+                                          std::get<Index>(all)...);
+            }(std::make_index_sequence<kCount - 1U>{});
+        }
+    }
+
+} // namespace Progmasoft::Catch3
diff --git a/src/Progmasoft/Catch3/Property.hpp b/src/Progmasoft/Catch3/Property.hpp
index 57f7ac7b..bd055148 100644
--- a/src/Progmasoft/Catch3/Property.hpp
+++ b/src/Progmasoft/Catch3/Property.hpp
@@ -31,6 +31,30 @@ namespace Progmasoft::Catch3
         /// reported failure to reproduce that single trial, including its
         /// shrinking, without rerunning the trials before it.
         std::optional<std::uint64_t> ReplayTrialSeed = std::nullopt;
+
+        // The fields below are read by ForAll and the other strategy-based
+        // checks; CheckProperty with a Generator ignores them.
+
+        /// A replay token from a failure report: runs exactly the reported,
+        /// minimized counterexample and nothing else.
+        std::optional<std::string> Replay = std::nullopt;
+        /// Trials that may be discarded, by a filter that found nothing or
+        /// by CATCH3_PROPERTY_ASSUME, per requested trial before the
+        /// property gives up.
+        std::size_t MaxDiscardRatio = 10;
+        /// Extra trials that search for a higher score after the regular
+        /// ones, when the property calls Target. 0 disables the search.
+        std::size_t TargetSteps = 500;
+        /// Directory of the example database. Failing examples are stored
+        /// there and replayed first on the next run. Empty: the directory
+        /// named by CATCH3_PROPERTY_DATABASE, or no database when that is
+        /// unset.
+        std::string DatabasePath;
+        /// Names the property in the database. The CATCH3_ macros fill it
+        /// with the test case name and the source line.
+        std::string Name;
+        /// Adds the Classify and Cover statistics to a passing report.
+        bool ShowStatistics = false;
     };
 
     enum class PropertyStatus : std::uint8_t
@@ -39,6 +63,20 @@ namespace Progmasoft::Catch3
         kFailed,
         kErrored,
         kInvalidConfiguration,
+        /// A Cover requirement was not met.
+        kInsufficientCoverage,
+        /// Too many trials were discarded to trust the result.
+        kGaveUp,
+    };
+
+    /// How often one Classify or Cover label held.
+    struct LabelStatistic final
+    {
+        std::string Label;
+        std::size_t Count = 0;
+        double Percentage = 0.0;
+        /// The percentage a Cover call requires; 0 for Classify.
+        double Required = 0.0;
     };
 
     struct PropertyFailure final
@@ -49,6 +87,11 @@ namespace Progmasoft::Catch3
         std::size_t ShrinkSteps = 0;
         std::string Counterexample;
         std::string Reason;
+        /// Replay token of the minimized counterexample; empty for
+        /// CheckProperty with a Generator, whose replay is TrialSeed.
+        std::string Replay;
+        /// What the property recorded with Note for the counterexample.
+        std::vector<std::string> Notes;
     };
 
     /// Stable, machine-readable outcome with a deterministic human-readable
@@ -59,6 +102,10 @@ namespace Progmasoft::Catch3
         std::size_t TrialsRun = 0;
         std::optional<PropertyFailure> Failure;
         std::string Error;
+        std::size_t Discarded = 0;
+        std::vector<LabelStatistic> Statistics;
+        /// Set when Statistics should be part of a passing report.
+        bool ShowStatistics = false;
 
         [[nodiscard]] bool
         Succeeded() const noexcept
@@ -74,6 +121,23 @@ namespace Progmasoft::Catch3
             {
                 case PropertyStatus::kPassed:
                     output << "property passed: " << TrialsRun << " trials";
+                    if (Discarded != 0)
+                    {
+                        output << ", " << Discarded << " discarded";
+                    }
+                    if (ShowStatistics)
+                    {
+                        DescribeStatistics(output);
+                    }
+                    return output.str();
+                case PropertyStatus::kInsufficientCoverage:
+                    output << "property coverage insufficient after "
+                           << TrialsRun << " trials: " << Error;
+                    DescribeStatistics(output);
+                    return output.str();
+                case PropertyStatus::kGaveUp:
+                    output << "property gave up after " << TrialsRun
+                           << " trials: " << Error;
                     return output.str();
                 case PropertyStatus::kInvalidConfiguration:
                     output << "invalid property configuration: " << Error;
@@ -88,7 +152,7 @@ namespace Progmasoft::Catch3
                     break;
             }
 
-            if (Failure.has_value())
+            if (Failure.has_value() && Failure->Replay.empty())
             {
                 output << "; failing trial " << Failure->Trial << ", root seed "
                        << Failure->RootSeed << ", replay seed "
@@ -99,8 +163,42 @@ namespace Progmasoft::Catch3
                        << "\nreplay: set PropertyOptions::ReplayTrialSeed to "
                        << Failure->TrialSeed;
             }
+            else if (Failure.has_value())
+            {
+                output << "; failing trial " << Failure->Trial << ", root seed "
+                       << Failure->RootSeed << ", shrink checks "
+                       << Failure->ShrinkSteps
+                       << "\ncounterexample: " << Failure->Counterexample
+                       << "\nreason: " << Failure->Reason;
+                for (const auto &note : Failure->Notes)
+                {
+                    output << "\nnote: " << note;
+                }
+                output << "\nreplay: set PropertyOptions::Replay to \""
+                       << Failure->Replay << '"';
+            }
             return output.str();
         }
+
+    private:
+        void
+        DescribeStatistics(std::ostringstream &output) const
+        {
+            for (const auto &statistic : Statistics)
+            {
+                output << "\n  " << statistic.Label << ": "
+                       << statistic.Count << " ("
+                       << static_cast<long long>(statistic.Percentage * 10.0
+                                                 + 0.5)
+                              / 10.0
+                       << "%";
+                if (statistic.Required > 0.0)
+                {
+                    output << ", required " << statistic.Required << "%";
+                }
+                output << ')';
+            }
+        }
     };
 
     namespace Detail
diff --git a/src/Progmasoft/Catch3/Relations.hpp b/src/Progmasoft/Catch3/Relations.hpp
new file mode 100644
index 00000000..d3c2ec62
--- /dev/null
+++ b/src/Progmasoft/Catch3/Relations.hpp
@@ -0,0 +1,99 @@
+// Copyright (c) 2026 Progmasoft.
+// SPDX-License-Identifier: MPL-2.0 WITH AdditionRef-Progmasoft-Exception-1.1
+#pragma once
+
+#include <Progmasoft/Catch3/ForAll.hpp>
+#include <Progmasoft/Catch3/Strategy/Context.hpp>
+#include <functional>
+#include <string>
+#include <utility>
+
+// Ready-made property bodies for the oracles that need no specification of
+// the expected result: differential, metamorphic and round-trip testing.
+// Each one is passed to ForAll in place of a hand-written body:
+//
+//     ForAll(Gen::Vectors(Gen::Integers<int>()),
+//            Equivalent(ReferenceSort, FastSort));
+
+namespace Progmasoft::Catch3
+{
+
+    /// Differential testing: the candidate must return what the reference
+    /// returns for every input. A mismatch reports both results.
+    template<typename Reference, typename Candidate>
+    [[nodiscard]] auto
+    Equivalent(Reference reference, Candidate candidate)
+    {
+        return [reference, candidate](const auto &...input) mutable {
+            const auto expected = std::invoke(reference, input...);
+            const auto actual = std::invoke(candidate, input...);
+            if (!(expected == actual))
+            {
+                Note("reference: " + Detail::DescribeValue(expected));
+                Note("candidate: " + Detail::DescribeValue(actual));
+                Detail::RecordPropertyFailureMessage(
+                    "the candidate disagrees with the reference");
+            }
+        };
+    }
+
+    /// Metamorphic testing: for every input x, relation(function(x),
+    /// function(transform(x))) must hold, for example that sorting a
+    /// shuffled list gives the same result, or that doubling a length
+    /// doubles a cost.
+    template<typename Function, typename Transform, typename Relation>
+    [[nodiscard]] auto
+    Metamorphic(Function function, Transform transform, Relation relation)
+    {
+        return [function, transform, relation](const auto &input) mutable {
+            const auto source = std::invoke(function, input);
+            const auto followUpInput = std::invoke(transform, input);
+            const auto followUp = std::invoke(function, followUpInput);
+            if (!static_cast<bool>(std::invoke(relation, source, followUp)))
+            {
+                Note("follow-up input: " + Detail::DescribeValue(followUpInput));
+                Note("source output: " + Detail::DescribeValue(source));
+                Note("follow-up output: " + Detail::DescribeValue(followUp));
+                Detail::RecordPropertyFailureMessage(
+                    "the metamorphic relation does not hold");
+            }
+        };
+    }
+
+    /// decode(encode(x)) == x for every input.
+    template<typename Encode, typename Decode>
+    [[nodiscard]] auto
+    RoundTrip(Encode encode, Decode decode)
+    {
+        return [encode, decode](const auto &input) mutable {
+            const auto encoded = std::invoke(encode, input);
+            const auto decoded = std::invoke(decode, encoded);
+            if (!(decoded == input))
+            {
+                Note("encoded: " + Detail::DescribeValue(encoded));
+                Note("decoded: " + Detail::DescribeValue(decoded));
+                Detail::RecordPropertyFailureMessage(
+                    "decoding the encoded input did not give it back");
+            }
+        };
+    }
+
+    /// function(function(x)) == function(x) for every input.
+    template<typename Function>
+    [[nodiscard]] auto
+    Idempotent(Function function)
+    {
+        return [function](const auto &input) mutable {
+            const auto once = std::invoke(function, input);
+            const auto twice = std::invoke(function, once);
+            if (!(twice == once))
+            {
+                Note("once: " + Detail::DescribeValue(once));
+                Note("twice: " + Detail::DescribeValue(twice));
+                Detail::RecordPropertyFailureMessage(
+                    "applying the function twice changed the result");
+            }
+        };
+    }
+
+} // namespace Progmasoft::Catch3
diff --git a/src/Progmasoft/Catch3/Stateful.hpp b/src/Progmasoft/Catch3/Stateful.hpp
new file mode 100644
index 00000000..6bd34caa
--- /dev/null
+++ b/src/Progmasoft/Catch3/Stateful.hpp
@@ -0,0 +1,157 @@
+// Copyright (c) 2026 Progmasoft.
+// SPDX-License-Identifier: MPL-2.0 WITH AdditionRef-Progmasoft-Exception-1.1
+#pragma once
+
+#include <Progmasoft/Catch3/ForAll.hpp>
+#include <Progmasoft/Catch3/Strategy/Containers.hpp>
+#include <functional>
+#include <optional>
+#include <string>
+#include <utility>
+#include <vector>
+
+namespace Progmasoft::Catch3
+{
+
+    /// One step of a stateful test: a description for the report and the
+    /// code that applies the step to the model and to the system under
+    /// test. It checks the system against the model with
+    /// CATCH3_PROPERTY_ASSERT.
+    template<typename Model, typename System>
+    struct Action final
+    {
+        std::string Description;
+        std::function<void(Model &, System &)> Apply;
+    };
+
+    /// A kind of step. Make builds the step from the current model, so its
+    /// arguments can depend on the state, for example by choosing a key
+    /// that the model holds. Precondition says whether the step may run in
+    /// a state; an unset precondition always holds.
+    template<typename Model, typename System>
+    struct Command final
+    {
+        std::string Name;
+        std::function<Strategy<Action<Model, System>>(const Model &)> Make;
+        std::function<bool(const Model &)> Precondition = {};
+    };
+
+    /// A command without arguments.
+    template<typename Model, typename System, typename Apply>
+    [[nodiscard]] Command<Model, System>
+    MakeCommand(std::string name, Apply apply)
+    {
+        return Command<Model, System>{
+            name,
+            [name, apply](const Model &) {
+                return Gen::Just(Action<Model, System>{ name, apply });
+            },
+        };
+    }
+
+    namespace Detail
+    {
+
+        template<typename Model, typename System>
+        [[nodiscard]] TrialOutcome
+        RunCommands(ChoiceSource &source,
+                    bool describe,
+                    const std::function<Model()> &initialModel,
+                    const std::function<System(const Model &)> &makeSystem,
+                    const std::vector<Command<Model, System>> &commands,
+                    const SizeRange &steps)
+        {
+            TrialOutcome outcome;
+            Model model = initialModel();
+            std::optional<System> system;
+            std::vector<std::string> log;
+            {
+                TrialRecordScope scope(outcome.Record);
+                system.emplace(makeSystem(model));
+            }
+            const auto addStep = [&]() -> bool {
+                // The choice names a command; when its precondition does not
+                // hold, the next commands are tried in order, so that the
+                // same choice always leads to the same command.
+                const std::size_t first = static_cast<std::size_t>(
+                    source.Draw(commands.size() - 1U));
+                const Command<Model, System> *chosen = nullptr;
+                for (std::size_t offset = 0; offset < commands.size(); ++offset)
+                {
+                    const auto &candidate
+                        = commands[(first + offset) % commands.size()];
+                    if (!candidate.Precondition || candidate.Precondition(model))
+                    {
+                        chosen = &candidate;
+                        break;
+                    }
+                }
+                if (chosen == nullptr)
+                {
+                    return false;
+                }
+                auto action = DrawGuarded(chosen->Make(model), source, outcome);
+                if (!action.has_value())
+                {
+                    return false;
+                }
+                log.push_back(action->Description);
+                RunBody(
+                    [&]() { action->Apply(model, *system); },
+                    std::tuple<>(),
+                    outcome);
+                return outcome.Verdict == TrialVerdict::kPassed;
+            };
+            (void)Detail::DrawElements(source, steps, addStep);
+            if (outcome.Verdict == TrialVerdict::kInvalid && !log.empty())
+            {
+                // A step that could not be built ends the sequence; the
+                // steps before it still ran and passed.
+                outcome.Verdict = TrialVerdict::kPassed;
+            }
+            if (de