Another problem with LLVM I’ve heard about is that it’s intermediate language or API or something is a moving, informally-specified target. People who know LLVM internals might weigh in on that claim. If true, it’s actually easier to target C or a subset of Rust just because it’s static and well-understood.

Two projects sought to mitigate these issues by going in different directions. One was a compiler backend that aimed to be easy to learn with well-specified IL. The other aimed to formalize LLVM’s IL.

http://c9x.me/compile/

https://github.com/AliveToolkit/alive2

There have also been typed, assembly languages to support verification from groups like FLINT. One can also compile language-specific analysis with a certified to LLVM IL compiler. Integrating pieces from different languages can have risks. That (IIRC) is being mitigated by people doing secure, abstract compilation.

My guess is that LLVM IR preserves too little semantic information to implement such a feature.

klee is a similar tool that operates on llvm bytecode: http://klee-se.org/

I think the LLVM level doesn't work as it throws away too much semantic information, but much of the CLANG front end can be used via it's API.

There is a fork of CBMC called ESBMC that does this and many other changes: https://ssvlab.github.io/esbmc/documentation.html

It predates LLVM. That's one reason, anyway.

VCLLVM was presented at ETAPS 2024. The goal is to compile both languages and specifications to LLVM IR.