Home | Fault

███████████   █████████   █████  █████ █████       ███████████
░░███░░░░░░█  ███░░░░░███ ░░███  ░░███ ░░███       ░█░░░███░░░█
 ░███   █ ░  ░███    ░███  ░███   ░███  ░███       ░   ░███  ░
 ░███████    ░███████████  ░███   ░███  ░███           ░███
 ░███░░░█    ░███░░░░░███  ░███   ░███  ░███           ░███
 ░███  ░     ░███    ░███  ░███   ░███  ░███      █    ░███
 █████       █████   █████ ░░████████   ███████████    █████
 ░░░░░       ░░░░░   ░░░░░   ░░░░░░░░   ░░░░░░░░░░░    ░░░░░

Fault is a domain specific language for encoding models of systems into Satisfiability Modulo Theories (SMT). It was developed originally to apply formal verification techniques to system dynamic style models, but it can currently do much more than that.

Somethings to use Fault for:

Modeling the behavior of a state machine
Making traditional boolean logic both machine executable AND human readable
Solving program synthesis problems
Explore the limits of control logic in feedback loops.

Let's Model A Thing!

The simpliest and easiest model to write in Fault is a state machine. Here's a circuit breaker — a pattern most engineers know well:

system circuitBreaker;

component breaker = states{
    closed: sfunc{
        advance(this.open) || stay();
    },
    open: sfunc{
        advance(this.halfOpen);
    },
    halfOpen: sfunc{
        advance(this.closed) || advance(this.open);
    },
};

run {
    breaker.closed;
};

This defines a component with three states and the transitions between them. Fault will explore every possible path through the state machine and verify that the behavior matches what you expect — for example, that open is always reachable from closed, or that the breaker can never get stuck.

Although Fault has a few distinct model types, you can actually import and attach one model to another, building out more complex behaviors. For example, you can attach stocks (reservoirs of resources) and flows (rates of change) to specify exactly how and when state transitions happen. The Language Reference section walks through a full example.

But first — let's look at stocks and flows on their own, since they're useful standalone too.

Stocks and Flows: The Sandwich Problem

Let's suppose that we work at a startup with a free lunch policy. We have a certain number of employees and need a certain number of sandwiches each day. We don't want to run out of sandwiches and we don't want to have too many leftover sandwiches.

We don't need a complex model to solve this problem-- we can just get one sandwich per employee and call it a day. But this solution leaves a lot of potential edge cases that will cause our solution to fail. For example, what if some of our employees decide to take two sandwiches? What if a few decide to skip the free option and go out for lunch? What happens to the leftover sandwiches at the end of the day? Do we throw them out or do we let people eat them the following lunch, thereby gradually increasing our surplus?

At the time Fault was created there were tools to build models that simulated the outcomes of this type of system, but nothing that allowed you to formalize and check whether the algorithms we create to manage in-flows, out-flows and autoscaling would behavior correctly

If you wanted an absolute guarantee that your lunch service will never run out of sandwiches and will never have too many extras, you need to create a model that specifies how your process for doing lunch keeps those edge cases from happening.

Okay here's our model in Fault:

spec sandwich;

def supplies = stock{
    ham: 20,
};

def people = stock{
    num: 15,
};

def lunch = flow{
    sandwiches: new supplies,
    toFeed: new people,
    service: func{
        sandwiches.ham -> toFeed.num; 
    },
    prep: func{
        if sandwiches.ham < toFeed.num {
            sandwiches.ham <- (toFeed.num - sandwiches.ham);
        }
    },
};

assert supplies.ham >= 0;

run init{
    day = new lunch;
} {
    day.prep;
    day.service;
    day.prep;
    day.service;
}

Let's break this down bit by bit.

The basic parts of the spec are stocks and flows. Stocks are collections of resources, in this case sandwiches and people.

def supplies = stock{
    ham: 20,
};

def people = stock{
    num: 15,
};

Flows are functions that cause the amount of stocks to change. In our model we have two different ways our stock of sandwiches changes. First we prepare sandwiches for lunch, increasing their amount. Then we serve those sandwiches and people eat them 😃

To do this we attach an instance of the previous defined stocks to our flow with new supplies and new people.

def lunch = flow{
    sandwiches: new supplies,
    toFeed: new people,
    service: func{
        sandwiches.ham -> toFeed.num; 
    },
    prep: func{
        if sandwiches.ham < toFeed.num {
            sandwiches.ham <- (toFeed.num - sandwiches.ham);
        }
    },
};

The service function is straight forward, we deduct enough sandwiches from out stock of sandwiches to feed the number of people we have.

The prep function has a bit more logic to it. If we have leftover sandwiches we don't want to waste them. So we will only make more sandwiches if we don't have enough for everyone and we will only make the number of sandwiches we need to feed everybody.

Like most model checkers, Fault uses bounded model checking which means that Fault will only "run" the model for a fixed number of steps. It will not check an infinite amount of time.

But it also shouldn't have to! You'll see why in a minute.

The run block defines what happens at each step. Each line is one round of execution.

run init {
    day = new lunch;
} {
    day.prep;
    day.service;
    day.prep;
    day.service;
}

Here we initialize a flow with stocks attached in the init section, then list the steps Fault should execute — first prep, then service, repeated for two days. Each line is one round.

When Fault runs the model, it isn't actually evaluating any code. Instead it compiles to SMT and feeds the model into a SMT solver. The solver explores all possible branches of the behavior. If we've written asserts, the solver will try to prove our assertions wrong (more on this later)

We start off with 20 sandwiches and Fault says in the first step of the model we have two scenarios: either we have 20 sandwiches or we have 15 sandwiches.

You're probably wondering why we would have 15 sandwiches at any point in the first round. It's because the first thing we do in round 1 is prepare sandwiches for lunch that day and the way we've defined that process is as follows:

If the number of sandwiches is less than the number of people, add difference between sandwiches and people

But Fault will explore both the scenario where the conditional is true and the scenario where it is false. It doesn't evaluate the conditional, it neither knows nor cares if the conditional is true. It just creates a rule in SMT that says if the conditional IS true than the number of sandwiches should be increased by the number of people less the sandwiches we have. Since in the first round we have MORE sandwiches than people that number is -5. 20 - 5 = 15 sandwiches. The solver then dismisses that value and selects the correct value of 20 for future steps.

So the way this plays out is that state 0 of the variable sandwich_day_sandwiches_ham is 20, state 1 (the conditional is true) is 15, state 2 (the conditional is false) is 20 and state 3 is a phi value where the solver selects either the true branch or the false branch. Written this way the model checker briefly peeks into other potential futures.

What's useful about looking at all possible scenarios in the model is that it allows us to consider what the system behavior would be if safety checks happened too late, if we've created race conditions, if we don't get a response from a request ... all things that happen on real systems and sometimes cause problems.

There's one more part of our model we're going to add. We're going to tell Fault we believe it is impossible that we'll run out of sandwiches and ask it to prove us wrong.

assert supplies.ham >= 0;

Asserts allow us to focus the solvers attention on how our model affects specific properties (invariants). Our simple sandwich model doesn't have many potential states because the number of sandwiches and the number of people are both set upfront. As models grow more complex there will be scenarios where many potential values could be assigned to a variable and the solver needs to choose one and move on. In these cases running the solver again might produce a slightly different scenario. Alloy is a good example. Every run of the solver will produce a different result.

Because we've done a good job with our first model, Fault is happy to tell us it can find no specific failure case where our assert is untrue. But we don't need a model checker to tell us the 20 sandwiches is enough to feed 15 people. It would be better if we got rid of the magic numbers

def supplies = stock{
    ham,
};

def people = stock{
    num,
};

This will define both the number of sandwiches and the number of people as unknown and Fault will attempt to solve for the values that will make our assert untrue. We can also define a variable as unknown explicitly with num: unknown()

To ensure Fault encodes variables with the right type, it's a good idea to declare unknown with a type hint: num: unknown(0) or num: unknown(0.0) or num: unknown(false) This will not assign a starting value (after all the whole point is the starting value is unknown)

Now Fault tells us that -1 sandwiches and 0.125 people will create a scenario where we do not have enough sandwiches for everyone

Start model, run for 4 rounds
-----------------------------------
   Resolving variable sandwich_day_sandwiches_ham to value -1.0
   Resolving variable sandwich_day_toFeed_num to value 0.125000
   Run function sandwich_day_prep (round 1)
      sandwich_day_sandwiches_ham: -1.0 → 0.125000
   Run function sandwich_day_service (round 2)
      sandwich_day_sandwiches_ham: 0.125000 → 0.0
   Run function sandwich_day_prep (round 3)
      Variable sandwich_day_sandwiches_ham is still 0.0
   Run function sandwich_day_service (round 4)
      Variable sandwich_day_sandwiches_ham is still 0.0

That's still not super useful. So let's add a few assumptions to tell Fault to ignore negative values 😃

assume supplies.ham[0] >= 0;
assume people.num > 0;

Since we want to find a scenario where we run out of sandwiches, we tell Fault that the starting value of supplies.ham cannot be less than zero and all values of people.num must be greater than zero.

This time, Fault can find no scenario where we run out of sandwiches.

Fault Philosophically

Most languages for formal system specification are designed to prove system properties correct. But since the learning curve for writing models in these languages is so steep, when the beginner receives a positive result (no failure cases) it is almost certainly because they haven't written the model correctly. This creates a weird and frustrating experience where new users can't trust their success and can't appreciate their progresss.

Fault can be used in this way if you want, but that's not what it is built for. Fault is based on the assumption that ALL systems fail eventually. The purpose of a specification written in Fault is to explore the conditions under which the system might fail.

Let's Model A Thing! ​

Stocks and Flows: The Sandwich Problem ​

Fault Philosophically ​

Let's Model A Thing!

Stocks and Flows: The Sandwich Problem

Fault Philosophically