Types hold data.Nothing constrains it beyond its type.

public enum OrderStatus { Draft, Placed, Paid, Shipped, Cancelled }

public record Order(
    Guid Id, Guid CustomerId,
    IReadOnlyList<Line> Lines,
    OrderStatus Status, int Version, decimal Total, string Label);

public record Line(
    Guid Id, Guid OrderId,
    string Sku, int Qty, decimal Price);

public record Shop(
    IReadOnlyList<Order> Orders, IReadOnlyList<Customer> Customers,
    IReadOnlyList<Category> Categories)
{
    public IEnumerable<Line> Lines => Orders.SelectMany(o => o.Lines);
}

[Constraints<Shop>]
public static partial class ShopConstraints
{
    public static readonly Constraint<Shop, Guid>
        OrderIdsAreUnique = Constraints<Shop>.Unique(s => s.Orders, o => o.Id);

    public static readonly Constraint<Shop, Guid>
        LinesPointAtAnOrder = Constraints<Shop>.References(
            s => s.Lines, l => [l.OrderId], s => s.Orders.Select(o => o.Id));
    // Acyclic and NoChains have the same shape: see the relations section
}

[Constraints<Order>]
public static partial class OrderConstraints
{
    public static readonly Constraint<Order>
        TotalNeverNegative = Constraints<Order>.Always(
            o => o.Total, t => t >= 0,
            "An order total is never negative.");

    public static readonly Constraint<Order>
        MoneyIsConserved = Constraints<Order>.Always(
            o => o.Lines.Sum(l => l.Qty * l.Price) == o.Total,
            "The total is the sum of the lines.");
}

public static readonly
    StateMachine<OrderStatus, string> Lifecycle = StateMachine
        .Define<OrderStatus, string>(OrderStatus.Draft)
        .Permit("place", OrderStatus.Draft, OrderStatus.Placed)
        .Permit("pay", OrderStatus.Placed, OrderStatus.Paid)
        .Permit("ship", OrderStatus.Paid, OrderStatus.Shipped)
        .Permit("cancel", [OrderStatus.Placed, OrderStatus.Paid],
            OrderStatus.Cancelled)
        .Build();
// no edge from Cancelled to Shipped: denied

await AutoTest.For(OrderConstraints.Instance).RunAsync();   // the axes the rules declare
Lifecycle.Spec().Exhaustive();                              // every state reached, every edge taken
// Sample, ConformTo and Commutes are one more line each,
// built from the same constraints and the same machine

public record WalletState(int Checking, int Savings);

public class Wallet
{
    public WalletState State => new(_checking, _savings);
    private int _checking = 30, _savings = 10;

    public async Task MoveAsync(int amount)
    {
        await Task.Yield();
        if (amount <= 0 || amount > _checking) return;
        _checking -= amount;
        _savings += amount;
-       _savings += amount;
+       _savings += amount - 1;
    }
}

// rules are written against a state; Map says where it lives
public static readonly ConstraintSet<Wallet> WalletRules =
    ConstraintSet
    .From(("money-is-conserved",
        Constraints<WalletState>.Conserves(s => s.Checking + s.Savings)))
    .Map<Wallet>(w => w.State);
await AutoTest.For(WalletRules, () => new Wallet())
    .MutateAsync<int>("Move", (w, n) => w.MoveAsync(n), _ => Gen.Int[1, 12])
    .Steps(1, 6)
    .RunAsync();

dotnet test
# the same rules and the same line run on every change,
# human or agent.