## Report.proved


Every postcondition holds and no runtime error is possible. With


`Report.proved: bool`


an observation (`sv.equivalent`), no postcondition depends on what it ignores, and some engine's doubles meet it ([floats_unmet](Report.floats_unmet.md#sverify.Report.floats_unmet)). Under `semantics="substrait"`, the reference's proof also carries over (`transfer` is empty).