{
  "id": "specialization:formal-methods",
  "_kind": "Specialization",
  "_file": "domain/specializations/specializations-science.yaml",
  "_cluster": "domain",
  "attributes": {
    "displayName": "Formal Methods",
    "parentDomainId": "domain:computer-science",
    "description": "Mathematical techniques for specifying, modeling, and verifying software and\nhardware correctness. Encompasses model checking (TLA+, Alloy, SPIN), theorem\nproving (Coq, Lean, Isabelle/HOL), abstract interpretation, and satisfiability\nsolvers (SMT/SAT). Applied to safety-critical systems, concurrent protocols,\nsmart contracts, and compiler verification to provide machine-checked proofs\nof correctness.\n"
  },
  "outgoingEdges": [
    {
      "from": "specialization:formal-methods",
      "to": "domain:computer-science",
      "kind": "specializes"
    }
  ],
  "incomingEdges": [
    {
      "from": "domain:computer-science",
      "to": "specialization:formal-methods",
      "kind": "contains"
    },
    {
      "from": "skill-area:mathematical-reasoning",
      "to": "specialization:formal-methods",
      "kind": "applies_to",
      "attributes": {
        "confidence": "secondary"
      }
    }
  ]
}