Belenos – Lightweight Formal Model Checking for C Developers

I just released Belenos, an open-source model checker that brings formal verification within reach of any C developer – no PhD required, no specialized toolchain, no obscure DSL to learn.

The core idea

Formal verification is often seen as an academic discipline: TLA+, SPIN, Alloy, Promela… powerful tools, but with steep learning curves and ecosystems far removed from day-to-day systems programming.

Belenos takes a different approach: your model is plain C. You define your system state as a C struct, your transitions as C functions, and your correctness properties as C boolean expressions. Belenos then explores the full reachable state space and checks that nothing goes wrong.

No new language. No translation layer. Just C.

How it works

Belenos is a single-header C library (belenos.h). A model is built from five primitives:

INIT

defines the initial state

EVENT

declares a state transition (applied one at a time to each reachable state)

INVARIANT

a safety property that must hold in every reachable state

GOAL

a liveness condition that must be satisfied in at least one reachable state

PRINT

a debug function to display a state when a violation is found

The engine performs a breadth-first exploration of the state graph:

1. Start from the initial state
2. Apply all events to each known state to discover new ones
3. Check all invariants on every new state
4. Continue until no new state is reachable
5. Verify that every liveness goal has been met

If a safety invariant is violated, Belenos reports the shortest event sequence leading to the erroneous state – making diagnosis straightforward. If a liveness goal is never satisfied, it is flagged explicitly.

Additional simulation paths can be declared with FROM/TO macros to verify reachability between arbitrary non-initial states – useful to check that the system can recover from specific configurations.

Concrete example: traffic lights

The tutorial walks through a two-traffic-light system with a safety requirement: at most one light can be green or orange at any time.

A naive model (unrestricted transitions) is immediately flagged by Belenos:

Warning: one_green_or_orange_max: violated invariant
---------------------------------------
light 0: RED -- light 1: RED
>>> light_0_green
light 0: GREEN -- light 1: RED
>>> light_1_green
light 0: GREEN -- light 1: GREEN
Error: Invariant violation

Two events. Shortest path. Done.

The corrected model – with guards preventing unsafe transitions – is validated across all reachable states. A refined model adds explicit transition rules (GREEN → ORANGE → RED → GREEN only) encoded as additional invariants, plus liveness goals ensuring each light eventually turns green. All verified.

Developer experience

Models are standard C programs. For quick iteration, they can be written as self-compiling shell scripts – the first line is simultaneously a valid shell command and a C comment:

//bin/cc -xc -Wall -O2 $0 -o /tmp/model && exec /tmp/model; exit $?

A belenos wrapper script is also provided for convenience:

$ belenos --san model.c        # with ASan + UBSan enabled
$ belenos -DMAX_STATES=4096 model.c

Installation is a single script (install.sh) that drops belenos.h and the belenos script into ~/.local/. No package manager, no build system dependency.

Design philosophy

Belenos is deliberately minimal and explicit. The state space is bounded by configurable macros (MAX_STATES, MAX_EVENTS, MAX_INVARIANTS, MAX_GOALS), making it suitable for protocols, synchronization mechanisms, small automata, and safety-critical state machines where exhaustive verification is tractable.

It won’t replace industrial tools for large state spaces, but it fills a real gap: fast, embedded, zero-friction formal verification for developers who want correctness guarantees without leaving the C ecosystem.

Key technical highlights

• Header-only library – zero build system integration required
• Breadth-first state graph exploration
• Safety (invariants) + liveness (goals) verification
• Shortest counterexample path on violation
• Multi-path verification with FROM/TO
• Self-compiling C scripts for fast iteration
• Sanitizer support (ASan + UBSan) out of the box
• GPLv3 licensed

Source & documentation: codeberg.org/cdsoft/belenos.

If you work on embedded systems, real-time protocols, concurrent state machines, or safety-critical software – give it a look.

Feedback and contributions welcome.