Just generating code might be interesting too, but in the above comment I was actually thinking of generating formal proofs of correctness.

The process I'm thinking of for using the model is

    Program
    ---(compiler)---> SMT definition + SMT statements for assertions
    ---(z3)---> Proof, Disproof, or "IDK" for assertions
    ↑--(proof-system)--> Filter for "IDK" assertions
    |--(ai)--> A proof of the assertion in the form of simpler assertions
    ⌞---------⌟ back to z3 step

I haven't really thought deeply about training a model off of this, but provided the compiler and z3 are robust against hostile inputs it seems fine even with randomly/AI generated programs. A less pure reinforcement learning technique, where you take code off the internet and only use re-enforcement learning to make it produce useful simpler assertions might work better.

I've started doodling with implementing this loop on top of the rust compiler, but I'm not yet at the point where I can say whether or not it works as well as I hope.

You tell it what you want it to prove. Or the tooling surrounding it does.

The tooling surrounding it might want to prove that "this main function never invokes undefined behavior", or something more local like "for all possible inputs to the public interface to this module, no undefined behavior is invoked".

Or you might want to specify constraints by hand. For examples, you might do that by writing normal tests except you can use magical variables that take on any value [1], or you might do that by annotating functions with contracts that they obey [2]. Or at a simpler level you might just annotate functions that should never panic.

Ultimately once you can prove things about your code, it's a tool in the toolbox for querying how your code works. You can use that to write correct code from the start, or to debug incorrect code, or various other things. The problem is that right now the state of the art (non-ai) can't reason about very complex code without a lot of human help - making it a fairly impractical tool. I think AI might mange to fix that.

[1] This is how kani works in rust, here's an example: https://github.com/model-checking/verify-rust-std/pull/112/f...

[2] Creusot takes this route, here's an example https://github.com/sarsko/CreuSAT/blob/master/CreuSAT/src/so...

In most cases I expect saying "<this> assertion fires with <this> input" is enough to be useful. Or "I can't prove <this> assertion doesn't fire, but I don't have a counter example either". Assertion used broadly to include things like rules for avoiding undefined behavior.

Better explanations would be nice of course, but not obviously practical. I wouldn't actually trust the AIs reasoning much in the first place, only that it can't trick the proof checking tool.