Is there any sort of memory safety prover for zig? Similar to SPARK for Ada
2 Likes
No - but there are interesting proofs-of-concept and linters and strategies that I’m fairly convinced will lead there in time.
2 Likes
I’m aware of this project -
2 Likes
why not valgrind?
or it’s not enough?
Valgrind can detect memory safety violations in a particular run of software (for particular inputs). SPARKAda can prove that no run can violate memory safety, irrespective of inputs. The difference is ∀ quantifier.
9 Likes