Skip to main content

validate_contract

Function validate_contract 

Source
pub fn validate_contract(contract: &Contract) -> Vec<Violation>
Expand description

Validate a parsed contract for completeness and consistency.

Returns a list of violations. If any violation has Severity::Error, the contract is considered invalid.

Validation is kind-aware: non-kernel contracts (registries, model-family schemas, reference documents) are validated only for metadata consistency; the provability invariant, equations, and proof/kani/falsification checks only apply to ContractKind::Kernel.