There are tools available for direct formal analysis of the system as implemented (and not “just” a model of it).
With e.g. the C bounded model checker CBMC, your model language is also C. Frama-C is another approach (Hoare-like, axiomatic logic). Klee works on LLVM IR etc.
Stronger proponents would perhaps suggest extracting the implementation from the model etc., but you don’t have to drink all the koolaid at once to get many of the benefits.
And not all your software needs to be formalized either, to get many of the benefits.
I’ved succesfully used CBMC and Klee on C code for verifying important parts of embedded safety/mission critical software on resource constrained HW (i.e. no OS, static allocation, single to double digit kilobytes of RAM etc.)
With e.g. the C bounded model checker CBMC, your model language is also C. Frama-C is another approach (Hoare-like, axiomatic logic). Klee works on LLVM IR etc.
Stronger proponents would perhaps suggest extracting the implementation from the model etc., but you don’t have to drink all the koolaid at once to get many of the benefits.
And not all your software needs to be formalized either, to get many of the benefits.
I’ved succesfully used CBMC and Klee on C code for verifying important parts of embedded safety/mission critical software on resource constrained HW (i.e. no OS, static allocation, single to double digit kilobytes of RAM etc.)
Formal methods rock!