Lean formalization of x86 and ARM

[chants]

So I wanted everyone's thoughts on whether this is worth doing or not. As I see it is in fact inevitable.

Here is the idea, Lean formalize x86 and AMD64 using the Intel and AND manuals. The same for ARM and ARM64. Including the fetch decoder execute cycle.

Now formalize various languages, like C, Python, etc and formalize security schemes and protection mechanism. It is a question whether a language should match its documentation or its compiler/virtual machine though ideally they are aligned.

Now reversing takes on a whole new dimension. Rather than break a license scheme, you rather *verify* it formally in Lean from asm and the provsble security scheme template.

If it is not provably secure you ask to fix it to make it more secure. Youve just identified literally every weakness inadvertently.

LLMs might be helping find issues. But they find 3 or 4 times as many often in subtle areas as formalization is brutally strict and can be presumed perfect up to axioms and assumptions. This is the strongest possible audit of security possible.

I wouldn't have suggested this before as it was ridiculously impractical. But the frontier models can write millions of lines of Lean in days and start to realize this. To me this is the future and such frameworks will be used in security analysis in the future. But if you know how to fix something then you also know how it is broken. Just wanted to see if anyone has any thoughts about it?