I think we agree on this. Fil-C does not ensure this. Showing the absence of run-time errors at compile-time is a hard problem, and the most realistic solution in general is via model checkers which I think would be the ideal solution, but we would need better tooling. Dependently types languages are also interesting.

In the context of existing tooling and C, there is also a lot of potential in using the optimizer to show safety properties. This works quite well to show the absence of signed overflow issues and null-pointer correctness, but still less well for bounds checking, e.g. see here for some preliminary experiments: https://uecker.codeberg.page/2026-05-22.html