{"$schema":"https://json-schema.org/draft/2020-12/schema","$id":"https://mandateshield.com/schemas/formal-model-results/v1","title":"MandateShield Bounded Formal Model Results v1","description":"Result contract for the executable finite-state exploration of the MandateShield execution-authorization abstraction.","type":"object","additionalProperties":false,"required":["$schema","schema_version","model","bounds","exploration","invariants","mutation_controls","outcome","claims","limitations"],"properties":{"$schema":{"const":"https://mandateshield.com/schemas/formal-model-results/v1"},"schema_version":{"const":"1.0.0"},"model":{"type":"object","additionalProperties":false,"required":["name","version","reviewed_on","tla_source","runner"],"properties":{"name":{"type":"string","minLength":1},"version":{"type":"string","pattern":"^\\d+\\.\\d+\\.\\d+$"},"reviewed_on":{"type":"string","format":"date"},"tla_source":{"type":"string","format":"uri"},"runner":{"type":"string","minLength":1}}},"bounds":{"type":"object","additionalProperties":false,"required":["tenant_count","budget_units_per_tenant","purchase_amount_units","receipt_key_generations","maximum_transition_depth","frontier_truncated"],"properties":{"tenant_count":{"type":"integer","minimum":1},"budget_units_per_tenant":{"type":"integer","minimum":1},"purchase_amount_units":{"type":"array","minItems":1,"uniqueItems":true,"items":{"type":"integer","minimum":1}},"receipt_key_generations":{"type":"integer","minimum":1},"maximum_transition_depth":{"type":"integer","minimum":1},"frontier_truncated":{"type":"boolean"}}},"exploration":{"type":"object","additionalProperties":false,"required":["states_explored","transitions_explored","frontier_states","safe_transition_violations"],"properties":{"states_explored":{"type":"integer","minimum":1},"transitions_explored":{"type":"integer","minimum":0},"frontier_states":{"type":"integer","minimum":0},"safe_transition_violations":{"type":"integer","minimum":0}}},"invariants":{"type":"array","minItems":8,"maxItems":8,"items":{"type":"object","additionalProperties":false,"required":["id","statement","passed"],"properties":{"id":{"enum":["budget_conservation","consume_at_most_once","revocation_prevents_reservation","unknown_never_restores_authority","release_requires_confirmed_non_success","late_success_dominates_unknown","retained_key_rotation_preserves_receipts","tenant_isolation"]},"statement":{"type":"string","minLength":1},"passed":{"type":"boolean"}}}},"mutation_controls":{"type":"array","minItems":8,"items":{"type":"object","additionalProperties":false,"required":["id","detected","violated_invariants","witness"],"properties":{"id":{"type":"string","minLength":1},"detected":{"type":"boolean"},"violated_invariants":{"type":"array","minItems":1,"uniqueItems":true,"items":{"enum":["budget_conservation","consume_at_most_once","revocation_prevents_reservation","unknown_never_restores_authority","release_requires_confirmed_non_success","late_success_dominates_unknown","retained_key_rotation_preserves_receipts","tenant_isolation"]}},"witness":{"type":"string","minLength":1}}}},"outcome":{"enum":["PASS","FAIL"]},"claims":{"type":"object","additionalProperties":false,"required":["mathematical_proof","tla_model_checker_executed","independent_audit","bounded_executable_exploration"],"properties":{"mathematical_proof":{"const":false},"tla_model_checker_executed":{"const":false},"independent_audit":{"const":false},"bounded_executable_exploration":{"const":true}}},"limitations":{"type":"array","minItems":1,"items":{"type":"string","minLength":1}}}}