Bethel Hall (ቤቴል ሆል)

Generates formal encodings of natural-language requirements, checks for disagreements, and uses counterexamples to refine the requirements and answer safety questions.

• Formalized all 64 requirements in the ABZ hemodialysis benchmark.
• Clarification brought 12 flagged requirements into agreement across the sampled encodings.
• Verification is relative to the generated formal model; it does not prove complete faithfulness to human intent.

Uses Quacky and Z3 to identify candidate faulty policy statements, asks an LLM for targeted edits, and checks each repaired policy against the request specifications.

• With 30 request specifications, full repair was 54.3% versus 22.3% for the baseline, more than twice the baseline rate.
• Full repair means satisfying every supplied request specification, not every possible request.

Converts policy permissions to automata-derived regular expressions, then uses an LLM to simplify the resource characterization. Model counting compares the original and simplified regexes within a chosen string-length bound.

• A configured similarity threshold determines whether to accept the simplified regex or fall back to the automata-derived characterization.
• The checks apply to resource regexes within that bound; they do not prove unrestricted equivalence or the correctness of freeform prose.
• The overall mean similarity is 0.926, rounded to 0.93. See the July 2026 paper revision for the evaluation.