Pitfalls of Safe Rust

For integer overflows and array out of bounds I'm quite optimistic about Flux

https://github.com/flux-rs/flux

I haven't actually used it but I do have experience of refinement types / liquid types (don't ask me about the nomenclature) and IMO they occupy a very nice space just before you get to "proper" formal verification and having to deal with loop invariants and all of that complexity.

> refinement types / liquid types (don't ask me about the nomenclature)

There's a nice FOSDEM presentation "Understanding liquid types, contracts and formal verification with Ada/SPARK" by Fernando Oleo Blanco (Irvise): https://fosdem.org/2025/schedule/event/fosdem-2025-4879-unde.... One of the slides says:

  Liquid types!
  Logically Qualified Types, aka, Types with Logic! Aka dependent types, etc...