Improving software performance often means finding ways to make existing code run more efficiently. This might involve rewriting a function, changing how data is processed, or making better use of the hardware available.
The challenge is making these improvements without changing what the software is supposed to do. An optimisation might make a program faster, but how can you be sure it has not introduced a bug or affected something elsewhere in the system?
This is where formal methods can help.
At Scidonia, we use Lean 4 and formal verification to optimise software while proving that the resulting code still meets its original specification. This gives development teams a way to improve software speed without having to rely on testing alone.
Why software speedups can be difficult to maintain
There are two common challenges when optimising software.
The first is making sure the optimised code still does what it was designed to do. Developers can use tests to check for problems, but tests only cover the cases they have been written for. A change that works in one situation could still cause problems elsewhere.
The second is keeping those improvements in place as the software develops. A compiler update, a change to build settings, or a seemingly small code change can affect how the program runs. Without a way to check that the optimised code still behaves as expected, it can be difficult to know whether a performance improvement is safe to keep.
Formal methods offer another way to approach this.
Rather than relying solely on tests, we write software in Lean 4, where the code and its specification can be developed together. We can then use mathematical proofs to check that optimisations preserve the behaviour defined by that specification.
How our approach works
At Scidonia, we use Lean 4 to develop and optimise software, then work with the compiled output to look for further performance improvements.
The process has four main stages:
- Write a specification in Lean. Define what the software needs to do.
- Develop an implementation. Write a candidate implementation that meets the specification.
- Optimise the implementation. Improve how the code works while checking it against the original specification.
- Optimise the compiled code. Compile to C, then LLVM IR, and use a conditional refinement relation on the LLVM IR to introduce further optimisations, such as SIMD instructions.
LLVM IR is an intermediate representation of the program, sitting between the source code and the machine instructions that run on the hardware.
Working at this level allows us to make optimisations that may not be available through the original source code alone. More importantly, we can use formal verification to prove that the resulting code still behaves within the limits of the original specification.
A practical example: improving JSON parsing performance
A JSON parser is a useful example of how this approach works. Parsing involves processing data byte by byte, identifying characters such as quotation marks, backslashes, and structural symbols.
These operations can create opportunities for performance improvements, particularly when the same checks need to be repeated across large amounts of data.
Here is how we approach the problem in five steps.
1. Define the rules in Lean
We start by defining the scanner’s byte transition in Lean. This is an executable definition, with correctness theorems already proved against the reference.
2. Write the implementation in C
We translate the rule into C, keeping the code within a restricted subset that the Lean semantics can model. This avoids relying on instructions or compiler features that are not covered by the proof.
3. Let the compiler optimise the code
We use Clang with -O2 -mavx2 to compile the code. The compiler vectorises the main loop rather than requiring us to write the vector instructions by hand.
In this example, three AVX2 lane masks identify quotation marks, backslashes, and control characters across a 32-byte window. A two-word bit table checks the twelve structural bytes, while a select chain applies the byte rule without branches.
4. Capture and prepare the LLVM IR
We capture the compiled LLVM IR and normalise it using opt -passes='reg2mem,instnamer'.
This moves loop-carried values into memory, giving the code a structure that the Lean semantics can model. Any compiler attributes that are removed are also recorded, along with the reason for removing them.
5. Prove that the compiled code is correct
Finally, we parse the LLVM IR back into Lean and prove a machine-checked theorem relating the emitted instructions to the original Lean definition.
This means that every behaviour the compiled code can exhibit is allowed by the specification.
If someone changes the compiler flags, pragmas, or C code, the proof can detect when the resulting implementation no longer satisfies the required refinement conditions. This helps prevent performance improvements from quietly introducing bugs.
What does formal verification actually prove?
It is worth understanding what the proof does and does not tell you.
The theorem shows that the compiled code behaves in ways permitted by the specification. It does not prove that the specification itself is correct. That still needs to be reviewed carefully.
The refinement is also conditional, and the conditions are stated alongside the proof.
It is equally important to understand that formal verification does not make code faster by itself. The performance improvements come from the compiler and the optimisations made to the code.
What the proof provides is confidence that these changes have not altered the behaviour of the software in ways the specification does not allow.
This is particularly useful when working with software that needs to remain reliable over time. You can continue to make performance improvements while having a formal way to check that the implementation still meets its requirements.
Looking beyond individual functions: system speedup
Improving the performance of one function is useful, but many businesses need to look at the performance of their systems as a whole.
This is something we have been exploring with LeanIn, our experimental concurrency runtime and work-stealing scheduler for Lean 4. It includes machine-checked proofs and a set of benchmarks that you can run yourself.
One of the results in the repository is particularly interesting. In a pipelined HTTP test, the server handled around three times as many requests per second as Node 22 when running with eight concurrent connections.
There are some important qualifications to that result.
Requests per second measures throughput, or how much work a system can handle over a given period. It is not the same as measuring how quickly an individual request receives a response.
The results also vary depending on the workload. In tests where a new connection is created for every request, LeanIn is slower than Node. The repository reports run-to-run variation of around 30%, so the figures should be treated as experimental rather than guaranteed performance improvements.
We would encourage you to look at the benchmarks, consider the conditions under which they were run, and try them on your own hardware.
How to get started with software performance improvement
You do not need to rewrite an entire application to explore this approach. In many cases, it makes more sense to start with one part of the system.
Here are four steps to consider:
- Find an area that could benefit from optimisation. Look for a function or section of code that has a noticeable effect on performance. This could be a parser, validator, routing rule, or another frequently used operation.
- Define what the code needs to do. Write down the expected behaviour, including the important inputs and outputs. This gives you a specification to work towards and a basis for checking future changes.
- Measure the existing performance. Record a baseline before making changes. Depending on what you are trying to improve, this might include throughput, response times, or the time taken to complete a particular operation.
- Explore what can be improved. At Scidonia, we can help turn your specification into Lean, optimise the implementation, and prove that the resulting code still meets the original requirements.
A small, well-defined example is often a good place to start before considering how the approach might work across a larger system.
If you want to explore how formal methods could help improve the performance of your software, talk to our engineering team.
You can also find out more about our technology, or read about our approach to performance and speedup.
