I've found a really interesting but niche way to validate firmware, which is formal verification.

I think the easiest way to describe it is by comparing it to unit tests (in practice they compliment each other) In unit tests, we call the tested method with a set of inputs (for example, function arguments, values of global variables, etc.) and we verify the correctness of the outputs after the function call. 

Code coverage says what percentage of the function lines were executed during those tests; ideally, it should be 100%. If coverage is 100% and all results are OK, then the function is fully tested. The issue is that we tested each branch at least once, but did we test all possible branch patches?

Formal verification, on the other hand, works in a way where we define a set of inputs - each should be unique - and they should cover all possible inputs, and for each, we define the output. But what is cool is that we don't have to (and many times shouldn't) define exactly what the variable value is. 

We can just say if it's "bigger than 0," for example, and for all values that could be stored in the variable, the verification software will mathematically/magically check if the expectation is correct. This is stronger than a unit test because we test not only one value but all possible values that meet the criteria. Because we test all possible criteria, we test all possible inputs for the function.

An open-source tool called Frama-C can do that. It also has a GUI for looking at the results (Ivette). I've integrated it all into a Dockerfile, so I don't have to install anything locally (except Docker, but I use it in all my projects anyway). You can take a look here.

Let's now compare a unit test and an equivalent formal validation proof. The proof is in the comments above the function, Frama-C recognizes it and analyzes it. 

We have two branches in the code - either the soil is dry or moist - so we have two behaviors, each specifying what its requirements are and what will happen. The two lines at the end specify that for this function, we have covered all possible branches.

/*@
    requires data.pump.configured_duration_level >= WATERING_PUMP_DURATION_LEVEL_MIN;
    requires data.pump.configured_duration_level <= WATERING_PUMP_DURATION_LEVEL_MAX;
    requires GPIObits.GP1 == 0 || GPIObits.GP1 == 1;
    requires data.pump.remaining_cycle_levels > 0
        ==> data.pump.level_remaining_seconds > 0;

    assigns data.pump.remaining_cycle_levels,
        data.pump.level_remaining_seconds;

    ensures data.pump.remaining_cycle_levels > 0
        ==> data.pump.level_remaining_seconds > 0;

    behavior soil_dry:
        assumes GPIObits.GP1 == GPIO_LEVEL_HIGH;
        ensures data.pump.remaining_cycle_levels ==
            data.pump.configured_duration_level;
        ensures data.pump.level_remaining_seconds == WATERING_PUMP_STEP_DURATION_SECONDS;

    behavior soil_moist:
        assumes GPIObits.GP1 == GPIO_LEVEL_LOW;
        assigns \nothing;

    complete behaviors;
    disjoint behaviors;
*/
void watering_handle_sensor_check(void)
{
    if (GPIO_IS_HIGH(GPIO_SOIL_SENSOR_INPUT))
    {
        data.pump.remaining_cycle_levels = data.pump.configured_duration_level;
        data.pump.level_remaining_seconds = WATERING_PUMP_STEP_DURATION_SECONDS;
    }
    else
    {
        WATERING_LOG_DEBUG_HIGH("Soil check OK - moisture sufficient");
    }
}

If you want to look at the equivalent unit test for this function, here is the link.

I've done formal verification of all the business logic in the firmware (or at least that's what I think; this is the first time I've done it). You can find more proofs in the main.c and watering.c files.

There is also a graphic tool called Ivette to inspect the results. Basically, it works in a way that for each proof, it gives a dot; green means it was verified. For example:

The idea, although it looks cool, is niche because it's harder to use than unit tests; it's mostly applied in the military, aerospace, or medical sectors.