This package basically exposes information that the standard Julia compiler already knows internally (extracted using some hooks I added last year to make the compiler more extensible) and uses for optimization. As such, it has quite good information about whether or not its analysis is complete, because we need that information to generate correct code. It is very possible to just error when the information is incomplete, which we do e.g. when compiling for GPU or TPU. In such a mode, the absence of type errors (or any other kind of error you wish to exclude would be proven). Of course Julia's type system is designed for semantics specification, not proofs, so it's not really what you'd want to use there. I think the most promising way to go is basically to let the users specify their own correctness criteria (for example, some people really care about correctness of array dimensions), and then just go to a full theorem proving system for that. I really like F* in this area as a design point and have played with some ideas in that direction. A package like JET.jl is of course a good step in this direction, since it can at least make use of the static information that the compiler does already need to prove for its internal optimization purposes.