What problem does K Framework solve?
Suppose we have a language L.
Formal Semantics of L is considered expensive and useless.
As a result, implementations of programs, model checkers, program verifiers, of L is based on adhoc understandings.
This can lead to imprecise behaviour since semantics are not formally defined.