What's there to gain security-wise? Nondeterministic generation & then execution of that code without proper verification seems to be the opposite of a good security posture.

why are you assuming there would be no proper verification in this scenario?

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.

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.

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.

I doubt it. It seems far more likely that such code will be written just once by LLMs, but in a way that allows its claimed guarantees to be formally verified (e.g. in Lean). At that point there’s no need to JIT an implementation each time.

My bet is one ultra-hardened, minimal, front-facing system which does N-modular redundancy which N systems, each written on a different stack/different language.

The hardened software picks the computation that wins the majority.

It's not an issue to write all the implementations in the various stacks/languages: we'll have better and better LLMs to help us.

This shall bring security and shall allow to detect shitload of bugs (both in the implementation itself but also in the stack).

Heck, this could even be compatible with GP: one of the implementation could be JIT'e by a LLM, others could be written in advance (and Lean formally verified). Not sure which sense it'd make though.

I'm 99.9% sure it's coming for if it's not, I'll make one.

I feel like that idea is erroneously mixing concepts. You want quorum in safety critical contexts, generally to guard against hardware failure. I think using independent implementations in such a scenario is uncommon and to date largely a stop gap to save money by replacing formal verification.

For security formal verification is really what you need. Both of the software and also eventually the hardware, since typically formal verification of software won't hold up against something like rowhammer. (Although TBF I'm not sure what sort of formal verification would have caught rowhammer.)