They talk about SPARK, but I never heard about it until now. Reading up on Wikipedia it seems an ADA derivative.
I assumed they were switching to Rust, but that doesn't seem to be the case.
SPARK allows you to formally prove that your code is correct according to a given specification. It can thus provides much stronger guarantees than what Rust would be able to provide.
Similar technology exists for Rust, but it is much less advanced than SPARK is (https://github.com/xldenis/creusot)