A safety property proven for every reachable state

A traffic light controller that must never let both directions go at once.

Checks passed

Public demonstration

This is not a client result. The recorded command and check status appear below.

Recorded outcome

The safety property holds in every reachable state, not only the tested ones. The cover checks show each green and yellow phase can occur, so the checks are not running on a design that never moves.

What was checked

Problem: A controller like this can pass every test someone wrote and still have a sequence where both directions go at once. Simulation only checks the inputs that were tried.
Scope: One small state machine with two outputs. Two properties: the two directions are never both off red, and each light only takes a legal value. Four cover checks, one for each green and yellow phase.
Approach: The properties are written in the RTL under an ifdef FORMAL guard, so normal simulation ignores them. SymbiYosys runs three tasks: a bounded check, an unbounded proof by k induction (a method that proves the property for every reachable state), and the cover checks.
Evidence: The proof log reports a successful proof by k induction. The cover log names each cover statement it reached.

Scope and limits

What these checks do not establish.

The design is small, and both outputs are decoded from one state register, so the property is easy to prove. It shows the method, not a hard proof.
The run does not assume a reset, so the cover checks show each phase is reachable from some state, not the full sequence from reset.
It says nothing about results on a RISC-V core.

Reproduce and inspect

Recorded verification status

We reran this on 13 September 2026 with SymbiYosys git b1a1e98, Yosys 0.67+post, and z3 4.16.0, the solver set in the repository configuration. The safety proof passes by k induction, bounded model checking passes, and all four cover checks are reached. The logs are in the repository.

Recorded commandformal-fsm-verification

sby -f traffic.sby prove
sby -f traffic.sby bmc
sby -f traffic.sby cover

Filesrtl/traffic_light.svstate machine with properties under ifdef FORMALtraffic.sbybmc, prove, and cover tasks

Next steps

Other examples

Want this method on your design?

Share the problem in a few lines. We will discuss the scope before any confidential project material changes hands.

Discuss a verification problem