With some help from the Kt native team im sure it could be made more stable and then it could provide a massive boon to the kt/native ecosystem

pretty interesting, how do you think it shall be better done?

So the biggest issue was, that kotlin methods like

@Kotlin_Int_inc

were not defined in the bitcode, so the verifier couldn't run against them. The seahorn guy worked around it by manually defining them

;;declare i32 @Kotlin_Int_inc(i32)
define i32 @Kotlin_Int_inc(i32) {
entry:
   %y = add i32 %0, 1
   ret i32 %y
}

It is in the bitcode, just one produced from C++ sources, but it is linked together, and so could be analyzed

I couldn't find a way with the compiler to get everything emitted to bitcode in one step

guess smth like bitcode stored here https://github.com/JetBrains/kotlin-native/blob/9e1e7559a2c39ebc51644234033fc44aa3a2b3e5/backend.native/compiler/ir/backend.native/src/org/jetbrains/kotlin/backend/konan/CompilerOutput.kt#L67 is what you need

Huh I might "hack" an emitter into that and report back