Proper verification would be deterministic rules the JIT-ed code would be checked against, so it would have to be non-JIT. Since the comment is talking about using more & more JIT for security reasons, I assumed it extended to verification too.

I don't get why you'd generally switch to JIT for security reasons.

Who writes the formal verification spec and when?

I suspect there are already plenty of test suites out there for something as universal as a networking stack.

Why can’t you JIT- generate the code and then run the verification?

Where did I say you can't do that? I answered you why I assumed the original comment was leaning towards JIT for everything.

Ok so if it is indeed possible to verify the code after JIT generating it, I still don’t understand why you would assume that in the hypothetical scenario we aren’t doing that verification?

You literally said it can’t be JIT, I’m just saying it seems like it can.

Again, I answered that in the earlier reply:

> Since the comment is talking about using more & more JIT for security reasons, I assumed it extended to verification too.

I wouldn't consider feeding the JIT-ed code to a JIT-ed verifier code proper verification.

Even ignoring the verification bit, I don't see the security benefits of having agents write JIT code, hence the original question. Because there might be some edge cases I don't know about, but I can't see this applying generally.

Because after proper verification you very much aren't at JIT territory. Take the network stack. From my memories a proper commercial test suit from say Defensics is from a few thousand to tens of thousand cases. For each of Ethernet, IP, TCP and UDP. Any decent coverage however fast will take some time. Most likely lot more than you want with just in time...

Yeah, the cost of running the test suite every time an agent generates code JIT would be the killer for running it at scale. I didn't even get into practicality of that approach too much because the gist of it for me was the question of agents writing code JIT having security benefits (?) - the verification thing is a sidetrack.

Certainly, adding agentic JIT code invites more complexity to properly do it, so what are the benefits that call for introducing it.

Because the verification would also be done by something non deterministic and then that’s a paradox.

Feed the LLM output into a “deterministic” verifier, problem solved. That’s how LLMs verify their new mathematical proofs with lean.

If you're doing formal verification, why are you JIT generating Code? Is the formal verification also being JITd? How do you know the agent wrote a good spec?

I don’t know why, but it’s certainly possible to imagine JIT-generating code and then verifying it. Which is why I asked why we were assuming the verification wasn’t happening.