Comment by jdw64

That's fascinating. Does it mean it verifies mathematical proofs directly within the Rust code? Does anyone know the underlying principles of how this is possible?