“Formal semantics can avoid stupid errors, for example, programs that give different results for different for different compilers version.” – Prof Grigore Rosu.
K-framework, from the Runtime Verification team, and by the group of Prof Grigore Rosu at University Urbana Campaign.
K-framework is a language to describe other languages.
His main idea is to use the k-framework to verify smart contracts.
Youtube interview with Prof Grigore Rosu