Great idea! CISC like x86 would be too hard. RISC like ARM, MIPS is worth trying.

But yes you can make Isabelle happy if you don't produce runnable code from Isabelle. However in that case it's harder to verify if your translation is correct.

Simple recursion like N factorial problem is easily expressed in Isabelle because it can be automatically proved terminated in finite time. However in real life, most applications would have recursive functions that relies on real life assumption to prove termination. Isabelle simply rejects them.

Espescially given Isabelle AFP entries usually have a detailed document with the proof code, it is worth trying to finetune LLM models on those valuable documents.

Another thing: I tried ChatGPT, claude code to generate Isabelle code when I was doing my master thesis and they weren't good at generating Isabelle code at all. Zero lines of my master thesis code was generated by them :( another thing we can try is to finetune LLM model on Isabelle code.

That's why we need framework like stateright, which verifies Rust code directly. However LLM isn't good at Rust at all, even recently in Dec 2025 that still holds.

Formal verification framework like Lean, Isabelle couldn't do verification for mainstream runnable programing language directly. It could go wrong when you translate programing language to Lean and Isabelle. Even worse, common logic like recursion couldn't be easily expressed in Isabelle(also lean?)

I had the exact same idea one and a half years ago. I talked about it with Leo during PaPoC and I said I want to build a similar framework like Stateroght in go because most applications aren't written in Rust and it's also hard for LLM to generate compilable Rust code. Sadly I didn't go further.