This is the same underlying tool that powers KCC and RVMatch. https://github.com/kframework/c-semantics https://github.com/kframework/c-semantics https://runt

This is the same underlying tool that powers KCC and RVMatch. https://github.com/kframework/c-semantics https://github.com/kframework/c-semantics https://runtimeverification.com/match/ https://runtimeverification.com/match/ Exactly what I’d hoped someone would do. Well, the first step anyway. The second step was doing a Rust semantics in terms of the C semantics already done. That allows quite a few things like Rust-to-C compilers, defeating Karger-Thompson attack, and potentially verification of interactions of Rust and C FFI code. On my end down the line, also use of C tooling for verification of equivalent Rust code.