Struct ObligationStatus 

pub struct ObligationStatus {
    pub property: String,
    pub obligation_type: String,
    pub l2_tested: bool,
    pub l3_kani: bool,
    pub l4_lean: bool,
    pub max_level: ProofLevel,
}

Verification status for a single obligation across all proof levels.

Fields

property: String

Human-readable obligation property name

obligation_type: String

Obligation type (invariant, bound, equivalence, etc.)

l2_tested: bool

Whether at least one falsification test covers this obligation

l3_kani: bool

Whether at least one Kani harness covers this obligation

l4_lean: bool

Whether the obligation has a Lean proof with status “proved”

max_level: ProofLevel

Highest achieved level for this specific obligation

Trait Implementations

impl Clone for ObligationStatus

fn clone(&self) -> ObligationStatus

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for ObligationStatus

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for ObligationStatus

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Serialize for ObligationStatus

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.