3 ms·

For integer overflows and array out of bounds I'm quite optimistic about Flux https://github.com/flux-rs/flux https://github.com/flux-rs/flux I haven't actual

For integer overflows and array out of bounds I'm quite optimistic about Flux https://github.com/flux-rs/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.

0rzech 2y ago
> 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-understanding-liquid-types-contracts-and-formal-verification-with-ada-spark/ 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...