Event-V

Event-V is an experimental library and set of tools for modelling software systems. It is based on the methodology pioneered by Event-B, in which simple, abstract models are incrementally refined until they are detailed enough to be executed as code. The framework requires each step to prove that it is a valid implementation of the abstract model described in the previous step. In this way, a formally verified program can be produced step by step, each time only adding a small amount of complexity.

Event-V is built on Verus, a framework for formal verification of Rust programs. Unlike other popular formal verification tools like Lean, Verus emphasizes proof automation. In most cases, the proof obligations generated by Event-V can be proved automatically, which frees the programmer from the tedium of writing proofs.

The basic unit of modelling in Event-V is the machine. A machine has some static configuration (the context) and some dynamic state. The state is modified by events, which may take input and produce output.

The core of Event-V is based on a number of traits. It is possible to directly implement machines using the traits, but it is verbose. To cut down on boilerplate, Event-V provides the machine! proc macro, which generates the trait plumbing for you. Here is an example of a simple machine defined using the macro:

// The `machine!` proc macro interprets the machine definition DSL.
machine! {

machine Counter {
    // Declare the **context** struct for the machine. This contains configuration that does not
    // change through the machine's lifetime.
    context {
        max_value: nat,
    }

    // A counter with `max_value == 0` could never be incremented or decremented, which would
    // be quite boring
    valid: |context| context.max_value > 0

    // Declare the **state** struct. Unlike the context, the state can be changed by events.
    // The state takes the name of the machine, so in this case we will end up with a
    // `struct Counter { pub value: nat }`.
    state {
        value: nat,
    }

    // This machine has a single **initialization event**, which sets the counter's value to 0.
    init: |context| Counter { value: 0 }

    // Every machine has an **invariant** that determines whether it is in a valid state or not.
    // For our counter machine, the invariant is that the value does not exceed the configured
    // `max_value`. Note that because the value is declared as `nat`, it must also be non-negative,
    // but we don't have to explicitly add that in the invariant.
    invariant: |context, state| state.value <= context.max_value

    // The machine's first event increments the counter by 1. It may only fire if the current value
    // is less than the max value.
    event Increment {
        // An event's **guard** determines when it is valid for the event to fire. In this case, we
        // may only increment a counter whose value is less than the max value.
        guard: |context, state| state.value < context.max_value

        // The **action** for an event defines how the machine's state changes after the event
        // fires. In this case, the post-action state has its value incremented by 1.
        action: |context, state| Counter { value: state.value + 1 }
    }

    // The Decrement event is similar in structure to Increment, except that its guard requires
    // that the current value be greater than zero.
    event Decrement {
        guard: |context, state| state.value > 0

        // Subtracting two `nat`s produces an `int` in Verus, so we cast the result with `as nat`.
        action: |context, state| Counter { value: (state.value - 1) as nat }
    }
}

}

Any logical inconsistency in the machine definition will cause a verification failure. For example, if we omit the state.value > 0 in the guard for Decrement, we will get an error from Verus saying it couldn't prove the machine's invariant.

Related Work

Much of the terminology and trait machinery in Event-V was inspired by Lean Machines. In particular, their concept of Functional Refinement is the one implemented in Event-V.

Event-V is heavily indebted to Verus, on which it is built. Verus itself has a state_machine! macro, as well as a sophisticated tokenized_state_machine! system for verifying distributed and concurrent algorithms. Event-V seeks to complement these existing systems by:

• Formalizing refinement. The proof obligations for state machine refinement are very mechanical, but there are some subtleties that are easy to gloss over. Having to write the proof obligations out from scratch for each machine is tedious and error-prone, and Event-V seeks to automate that.
• Adding tools to debug and interact with machines. Event-V treats animation as a first-class feature, providing hooks and plumbing to make it as easy as possible to interact with state machines during development.