I don't think it matters because hacspec on this case is just the language which is a subset of rust. He still just uses cargo so treat it as rust code.

The point is that you can check the binary against some sort of formal definition to make sure the implementation you have at hand has not been tampered with. But it seems the idea is to check during dev not usage which for me is a missed opportunity. Why can't it check if it's correct every time it's loaded?

   Keep in mind that Bertie is written in hacspec -- a more "restrictive" version of Rust that lends itself to formal verification. Working on Bertie feels a lot like working on a typical Rust crate but all code needs to be valid according to hacspec. Thus, you may also find that some code is "unusual" compared to vanilla Rust.