Original developer of the C semantics in K here! I just wanted to add a pedantic clarification (since pedantry is what semantics is all about).
The semantics of the language itself is more or less complete. On top of that, a sizable portion of the standard library is given semantics directly (e.g, malloc, setjmp, stdargs, I/O including input/output to FILEs, much of printf, etc. are all formalized in the semantics). There's even basic C11 thread support. All of this runs and can be reasoned about formally. I tried to give direct semantics to the things that couldn't be (easily) written in C, because much of the standard library CAN be written in C and so it isn't so critical that it's formalized.
To round out the library you can provide provide C implementations of any missing library functions at compile time (we provide some by default), and it will KCC those just like any other code. The resulting system is pretty good at catching undefined behavior, but it is super slow.
I'm not involved with the commercial version, but they offer a trade off: don't do any semantic checking inside standard library calls in exchange for faster execution times. My understanding is that instead of chugging through the semantics of printf for every bottle of beer on the wall, they just call out to a native of printf. This makes things a lot faster, but it's possible you won't catch as many problems. In general, the commercial version is trying to make using the semantics practical instead of "academically slow", which was all I managed :)
For some nice charts and pictures, you can see the original blog post this one was inspired by: http://datagenetics.com/blog/november42014/index.html
It contains pictures for an algorithm that doesn't properly shuffle, as well as the fisher-yates shuffle.
The semantics of the language itself is more or less complete. On top of that, a sizable portion of the standard library is given semantics directly (e.g, malloc, setjmp, stdargs, I/O including input/output to FILEs, much of printf, etc. are all formalized in the semantics). There's even basic C11 thread support. All of this runs and can be reasoned about formally. I tried to give direct semantics to the things that couldn't be (easily) written in C, because much of the standard library CAN be written in C and so it isn't so critical that it's formalized.
To round out the library you can provide provide C implementations of any missing library functions at compile time (we provide some by default), and it will KCC those just like any other code. The resulting system is pretty good at catching undefined behavior, but it is super slow.
I'm not involved with the commercial version, but they offer a trade off: don't do any semantic checking inside standard library calls in exchange for faster execution times. My understanding is that instead of chugging through the semantics of printf for every bottle of beer on the wall, they just call out to a native of printf. This makes things a lot faster, but it's possible you won't catch as many problems. In general, the commercial version is trying to make using the semantics practical instead of "academically slow", which was all I managed :)
Any questions welcome.