1  {
 2    "$schema": "http://json-schema.org/draft-07/schema#",
 3    "title": "FerrisProof Configuration",
 4    "type": "object",
 5    "properties": {
 6      "profile": {
 7        "type": "object",
 8        "properties": {
 9          "level": {
10            "type": "string",
11            "enum": ["minimal", "standard", "strict", "formal"]
12          },
13          "enforcement": {
14            "type": "string",
15            "enum": ["advisory", "warning", "error"]
16          },
17          "enabled_techniques": {
18            "type": "array",
19            "items": {
20              "type": "string",
21              "enum": [
22                "TypeSafety",
23                "PropertyTests", 
24                "SessionTypes",
25                "RefinementTypes",
26                "ConcurrencyTesting",
27                "FormalSpecs",
28                "ModelChecking"
29              ]
30            }
31          }
32        },
33        "required": ["level", "enforcement", "enabled_techniques"]
34      },
35      "tools": {
36        "type": "object",
37        "properties": {
38          "tla_plus": {
39            "type": "object",
40            "properties": {
41              "tlc_path": { "type": "string" },
42              "timeout": { "type": "integer", "minimum": 1 },
43              "workers": { "type": "integer", "minimum": 1 }
44            }
45          },
46          "alloy": {
47            "type": "object", 
48            "properties": {
49              "analyzer_path": { "type": "string" },
50              "scope": { "type": "integer", "minimum": 1 }
51            }
52          },
53          "proptest": {
54            "type": "object",
55            "properties": {
56              "cases": { "type": "integer", "minimum": 1 },
57              "max_shrink_iters": { "type": "integer", "minimum": 1 }
58            }
59          },
60          "kani": {
61            "type": "object",
62            "properties": {
63              "cbmc_path": { "type": "string" },
64              "unwind": { "type": "integer", "minimum": 1 }
65            }
66          }
67        }
68      },
69      "features": {
70        "type": "object",
71        "properties": {
72          "cache_enabled": { "type": "boolean" },
73          "parallel_execution": { "type": "boolean" },
74          "generate_reports": { "type": "boolean" }
75        },
76        "required": ["cache_enabled", "parallel_execution", "generate_reports"]
77      },
78      "thresholds": {
79        "type": "object", 
80        "properties": {
81          "max_verification_time": { "type": "integer", "minimum": 1 },
82          "max_memory_usage": { "type": "integer", "minimum": 1 },
83          "cache_ttl": { "type": "integer", "minimum": 1 }
84        },
85        "required": ["max_verification_time", "max_memory_usage", "cache_ttl"]
86      }
87    },
88    "required": ["profile", "features", "thresholds"]
89  }