Self-insert time.

I spent some time exploring this topic. Here's my thesis: Formal verification was expensive. 20x expensive compared to just developing the software, as the author notes. The cost of finding and developing exploits also was high. That creates an incentive to put software verification aside, since it solves a relatively small problem, at an extremely high cost.

We've seen how Mythos has found more vulnerabilities than the rest of the security industry combined. (you can argue about the quality and what counts as a vulnerability, but not the point) So the cost of finding and developing exploits has dropped dramatically.

On the other hand, formal verification is now much easier, since LLMs can automate the proof. You don't even need to worry about hallucinations, you merely need to trust Lean core. If the LLM is wrong, the proof will get rejected!

The problem of exploits gets bigger, and the solution of formal verification gets cheaper. As a result, the needle is now moving in the direction of "more formal verification".

I, personally, think that it is ridiculous that ~none of the software we use is known to work correctly. It just happens to work correctly, most of the time.

My (ambitious) goal is to have a self-hosting, formally verified compiler, which allows proof transfer from source code down to assembly. I have not achieved that goal yet.

What I have so far:

- one (non-optimized) compiler step which is formally verified

- three simple functions (hex, hex with labels, strtoull) formally verified, against RISC-V assembly, and against a custom IR

https://github.com/m1el/riscv-fv-bootstrap

The project is in quite a bad shape, and I am trying to improve my skills in that direction.