ETAPS 2026

In April, I went to ETAPS 2026 to attend VerifyThis and the Rust Verification Workshop. In this post, I'll focus on writing about my experiences going to VerifyThis 2026. I do not know yet if I'm also going to write a post about the Rust Verification Workshop.

VerifyThis 2026

VerifyThis is a competition where competitors receive four challenges that contain a verification task. I took part in the competition in a team with Jack, another PhD student. Even though VerifyThis calls itself a competition, I would not see it as such. VerifyThis is a great place to learn more about how to verify real-world code. It also shows how a verification tool should be adapted to be able to handle real-world code. Even though we participated with Viper, I plan to use Prusti for next year and made multiple realisations.

General verification skills

When it comes to general verification skills, I mainly learned how to model concurrency with locks in a separation-logic based language. Locks can be seen as further resources. These resources contain the underlying permissions. For example, let's assume that we have some integer that can only be read by or written to by one thread at a time. Therefore, the lock would contain permission to access the integer. In Viper, this would be implemented as a predicate, roughly written as follows:

field val: Int

predicate Lock(addr: Ref) {
    acc(addr.val)
}
                    

Before we can spawn multiple threads, we need to make sure that we actually have access to the data we want to lock. In Viper, we can do this by folding the predicate.

// create data
var sharedData: Ref := new(val)
// lock data
fold Lock(sharedData)
// give up permission - make Lock available to threads
exhale Lock(sharedData)
                

When we now assume to have multiple threads, acquiring a lock can be seen as inhaling that permission.

// acquire lock
inhale Lock(sharedData)
// access data
unfold Lock(sharedData)

Why does this work? This works because only one place can hold full permissions to a Separation Logic resource at a time. Since the current thread holds full permission, we can assume that no other thread can also have full permission. The inhale is sound because we made sure to exhale the lock directly after creating it. The inhale of a permission therefore models the acquiring (including a potential wait until the lock is available) of the lock. To release a lock, we basically do it the inverse way: We first need to prove that we still hold access to the data that is locked (by folding the predicate) and then exhaling the lock.

fold Lock(sharedData)
exhale Lock(sharedData)

Prusti is more high-level than Viper. Therefore, we cannot just inhale and exhale permissions. We also do not have the option to define predicates. However, what we can do is model the lock as a struct. The struct contains a raw pointer to the actual data. The struct then implements two functions: One for acquiring and one for releasing the lock. When we acquire the lock, the acquire function shall ensure that we get access to the location through the raw pointer. The release function then does the opposite.

Except for locking, I could also see that it is crucial to first understand what we want to model before starting to code. I think that this was one of the issues that degraded our performance: We started to code before we even tried to understand what we need to do. That said, it's all a big learning experience, and for me this was valuable experience.

One more thing that I learned is related to finding a good model: One should try to find points where it's possible to make verification easier. For example, in one challenge we had to model memory allocation. Bytes in memory are never read alone. Therefore, the naive idea of just encoding the entire memory as a sequence of bytes is over-complicated. As we need to also read full addresses from the memory (modelling page tables) and parse those, it makes sense to treat the memory as a sequence of pages (since a page is the smallest entity that we can read/write). A page then consists of multiple 32 Bit unsized integers (since the instructions were about a 32 Bit machine; addresses are 32 Bit wide).

Another lesson-learned is that one should really pay attention to defining invariants: For the challenge with the page tables, it would have been more useful to first focus on defining the invariant: Properties about the machine that always need to hold. We can then structure the proof into two parts: Proving that the invariant always holds, and proving that the actual properties hold if the invariant holds. This greatly eases proving the properties and it also makes it easier to see what we actually want to prove.

Prusti

I decided to not use Prusti for this year's edition of VerifyThis because we are still in the process of completely rewriting Prusti to a new version. However, that's the beauty about VerifyThis: It shows what a tool needs to support to be able to verify real world code. I therefore set it as my personal goal for this year to write the challenges from this year's VerifyThis in Prusti and to get Prusti to a point, so that it can verify these programs. I then want to compete with Prusti next year. Prusti, as a Rust verifier, has one major advantage over other tools: After writing the code in Rust, we get the memory-safety proof "for free" because of Rust's ownership type system. We can therefore directly go to verifying correctness properties. In case, the program needs parts to be written in Unsafe Rust, this is one of the advantages that Prusti uses separation logic: We can also reason about Unsafe Rust - at least that's what I'm currently working on ;)

Results

Nevertheless, VerifyThis is still a competition. So, how did we do? Well, I didn't go into the competition expecting to win anything as a first year PhD student, nor did we. That said, I think we still did pretty well. We made quite some progress in most of the challenges. We even attempted a challenge that noone else tried to tackle. For that, we even got an unofficial award (Most Daring Team) from the organisers.

Concluding words

All in all, VerifyThis was tons of fun and I am glad that I could attend. I want to thank Jack for being my team-mate and the organisers for the great organisation! I am looking forward to next year 😄