Formally verify the code using a verification tool

[mlaveaux]

There are several formal verification tools for Rust, e.g, prusti, kani and creusot using different techniques to verify soundness. Apply one of those tools to a subset of the code to see if this is viable.

creusot uses the why3 platform under the hood and this is a full deductive theorem prover. It is written in OCaml. It uses contracts for pre and post conditions which are then checked by the verifier. It cannot handle concurrency and external dependencies that well.

prusti uses viper under the hood, but can verify multi-threaded programs using separation logic. The tool requires Java to be installed, but works under any platform. Uses contracts to specify pre and post conditions of functions. This tool has not had stable updates in the last year, a large 2.0 rewrite seems to be in progress, this also means that 2024 edition Rust is not supported on the stable release.

kani cannot verify multi-threaded algorithms. It checks for absense of panic and failing asserts in the code, and has annotations to guide the verification efforts. It is based on bounded model checking, but can be extended with loop invariants to give proofs for unbounded programs. Furthermore, since it is based on model checking it struggles with large inputs, for example parsing inputs. The code cannot have undefined behaviour, and the tool only works on linux (and maybe macos) and requires CBMC under the hood (which is a C++ project and requires a C++ compiler). However, it can verify unsafe code.