LLM coding has become a popular and powerful way to build software, but programmers are struggling with the resulting shift in software engineering. They must review large amounts of generated code, find bugs in code they did not write, and manage failures caused by errors in—or attacks targeting—generated code. These issues are exacerbated for systems software because it provides critical infrastructure and thus must be reliable and secure.

In the last blog post, I highlighted some important parts of systems development that should not be skipped by using AI. However, it is unclear that we can easily leverage LLMs to even build parts of reliable and secure systems. This blog post analyzes that gap and what we as systems researchers might do to bridge it.

Key Challenges

Let us evaluate LLMs as a method of specifying software behavior, similar to programming languages (i.e., Rust), and verification (i.e., Verus). We evaluate across four axes and use Rust and Verus as relatively optimal examples of the properties that we care about.

1. Precision - the amount of undefined behavior allowed by the method of specification.
2. Determinism - the likelihood that the specification will generate the same system each time.
3. Correctness - the likelihood that the generated system will have bugs that deviate from the intended behavior.
4. Ease of Use - the amount of time and effort it takes the programmer to specify the system’s behavior.

	Precision	Determinism	Correctness	Ease of Use
Rust	Average	High	Average	Average
Verus	High	High	High	Low
Claude	Low	Low	Low	High

Rust and its associated compiler and runtime are average for every metric except for determinism. The Rust compiler and runtime are likely to generate the same instructions and execution every time, but Rust does have undefined behavior which makes it imprecise. Rust code is mostly correct but unlikely to be entirely bug-free, and the time and effort to write a program in Rust is about average for a programming language. Other programming languages might deviate slightly on each metric but generally, we’ve settled on programming languages of various forms as the best trade off of ease of use and other metrics for specifying the behavior of software.

More recently, verification has become a popular technique for increasing the correctness of programs. Verification requires the programmer to write a separate specification that formalizes the behavior of the software, then proves that the code conforms to that specification. Verification significantly reduces the likelihood of bugs (although a bug in the specification and code can occur); however, it requires much more time and effort from the programmers.

In comparision, LLMs perform poorly on every axes except for ease of use. This is well understood given most people’s experience with Claude, Copilot, etc. While large amounts of code are easy to generate, it is hard to generate code that: 1) is precisely what the programmer would have written, 2) is reliably the same every time, and 3) totally bug-free and correct.

For now, we assume that the programmer does not carefully read every line of generated code (much like I don’t read the assembly generated by my Rust code). Regardless, reviewing generated code decreases the ease of use without significantly improving any of the other metrics. For example, we can assume that the programmer is not likely to find all the bugs, as previous work has shown that it is very difficult even for experts to find bugs in others’ code. Likewise, the programmer might achieve slightly more precision through successive iterations of prompt engineering but there is a limit to how precise natural language can be when describing a software and LLMs cannot be relied on for determinism.

Research Directons

Thus our goal is to increase the use of LLMs for specifying system behavior on one or more of these axes without reducing the ease of use. There is already much work on improving correctness, however it often trades off ease of use for correctness. For example, adding Verus specifications means that either the programmer has to write the spec or understand both the LLM-generated code and spec.

• RQ: Can we increase correctness without requiring the programmer to understand variables in the code (i.e., still using natural language)?

While we cannot increase the determinism of LLMs, we could decrease our reliance on determinism. Acceptability-oriented programming and approximate computing shows some potential in this direction. For example failure-oblivious Rust might be more resilient to non-determinism in cases where it doesn’t violate the acceptability envelope.

• RQ: Can we do other things with the language runtime or verification system to reduce the dependence on determinism for correctness?

Techniques developed for approximate computing might also work; however, approximate computing was largely about starting with precise programs and reducing that precision, rather than starting with imprecise programs, so we would need different techniques to refine rather than relax the program’s precision.

• RQ: Can we increase the precision with a more formal natural language specification? Can we train that into the model or add it to the context?