Policy enforcement and formal verification as Energy-Based Model (EBM)…

Research Question

How can discrete policy engines and formal verifiers be translated into continuous or structured optimization signals that guide Energy-Based Model (EBM) search while preserving the original natural-language intent of requirements?

Findings

Executive Summary

Policy and formal-verification signals should guide Energy-Based Model (EBM) search, where candidate configurations are ranked by an energy score, through a two-tier objective stack in which non-negotiable obligations remain hard feasibility constraints and repairable obligations become named weighted penalties over a normalized, policy-relevant field representation of the candidate.

Rego policies are well-suited to this translation because OPA can partially evaluate policies against known context and emit residual conditions over unknown candidate fields, which can then become hard or soft objective terms rather than opaque final-stage booleans.

Natural-language intent is best preserved by an intermediate requirement representation, similar to FRETish, that keeps clause-level semantic links between business wording, formal rules, canonical state fields, and resulting penalties or verifier diagnostics.

Verifier outputs should enter the loop as structured repair guidance, such as unsatisfiable cores, remaining proof goals, affected state paths, and explicit unknown states for unresolved obligations, with fail-closed escalation when policy-critical proof work cannot be discharged in time.

Key Findings

1. The most reliable translation keeps legally or safety-critical obligations as hard constraints while mapping repairable policy clauses to named weighted penalties, because Z3-style soft constraints support graded infeasibility without blurring the obligations that must never be traded away.
2. OPA partial evaluation provides a practical compilation mechanism for policy-guided search because it specializes Rego against known business context and leaves residual conditions over unknown candidate fields that can be re-used as structured objective terms.
3. A canonical state boundary is necessary because policy compilation and optimization both depend on stable field-level semantics, while adjacent repository work shows that scoring raw text directly leaves too much variance and too little traceability for governance use.
4. Intent preservation is strongest when each business clause is linked through an intermediate structured requirement record to one formal rule family and one optimization term family, because FRET's multiple representations and semantic-equivalence proofs make translation drift easier to detect.
5. Wrong-but-provable encodings are best caught with two-way validation harnesses that combine side-by-side requirement views, executable positive and negative examples, and policy decision traces, because formal consistency alone does not guarantee business-semantic fidelity.
6. Verifier failures should be converted into localized repair artifacts, such as unsatisfiable cores, remaining proof goals, and affected state paths, because those diagnostics expose the smallest conflicting obligation set more directly than a single negative reward number can.
7. Approximate or relaxation-based verification results should guide ranking and repair but should not silently authorize policy-critical actions, because the verification literature distinguishes exact guarantees from scalable but conservative approximations.
8. Unresolved proof obligations, timeouts, and unsupported fragments need an explicit unknown or escalation status instead of a soft pass, because a search loop cannot treat incomplete formal evidence as equivalent to either compliance or violation.
9. Explainable audit trails require one correlated record that ties business clause identifier, formal rule revision, canonical state snapshot, violated path or proof goal, penalty family, and final action, because OPA decision logs and FRET requirement views solve different parts of the traceability problem and need to be joined.

Assumptions

• The orchestration layer can persist clause identifiers, canonical state snapshots, and repair diagnostics per iteration. Justification: without stored trace links, the proposed audit model cannot be implemented.
• The search loop can accept structured objective families and local patch proposals instead of only a single scalar loss. Justification: hard and soft clause structure is central to the recommended translation.

Analysis

The evidence favors clause-level compilation over direct prose scoring because OPA already separates known context from unknown candidate state and because structured optimization tools already separate hard and soft obligations.

The main design trade-off is between preserving exact formal meaning and keeping the search loop computationally useful. A system that keeps every obligation hard will often become brittle or non-progressing, while a system that softens everything loses the distinction between unacceptable and repairable deviations.

Semantic anchoring through structured requirement representations similar to FRET resolves the most serious translation risk because it provides a reviewable path from business prose to formal clause, whereas direct natural-language-to-penalty compilers leave too few checkpoints for human review.

Lean proof states and Z3 unsatisfiable cores matter because they already expose repair-relevant structure. A loop that ignores that structure and consumes only pass or fail outcomes throws away the most valuable part of the verifier signal.

The rival design, keeping policy engines and provers as pure final gates, is simpler to implement and avoids mixing search with governance logic. It is weaker when the goal is guided repair, because the model learns only that a candidate was rejected, not which obligation family should change next.

Risks, Gaps, and Uncertainties

• Public documentation is strong on policy compilation, solver objectives, and verifier diagnostics, but weak on end-to-end production case studies that combine Large Language Model generation, Energy-Based Model search, and formal proof systems in one deployed control path.
• The recommended intermediate representation borrows heavily from structured requirement representations similar to FRET, but no consulted source proves that one representation fits every policy domain or every proof system.
• The evidence base supports grouped hard and soft objectives well, but it does not specify one canonical weighting scheme for business risk classes; organizations will still need governance decisions about weight assignment.
• Recent architecture-specific advances beyond the accessible 2018 verification survey may be underrepresented in the exact-versus-approximate trade-off discussion here.

Open Questions

• Which canonical state schema works best for mixed code, workflow, and natural-language candidates when one candidate spans several artifact types?
• Which mutation or adversarial test suites are most effective for detecting translation inversion between prose policy and formal clauses?
• Which human-review interfaces best present unsatisfied clause sets and proof-state diagnostics without overwhelming policy owners?
• When approximate verification remains unresolved, what escalation threshold best separates safe retry from mandatory human review?

sources

• [x] Open Policy Agent Rego Policy Language
• [x] Open Policy Agent REST API Compile API
• [x] Open Policy Agent Evaluating a Data Filter Policy
• [x] Open Policy Agent Writing Valid Data Filtering Policies
• [x] Open Policy Agent Decision Logs
• [x] LeCun et al. (2006) A Tutorial on Energy-Based Learning
• [x] Lean Community Theorem Proving in Lean 4 Tactics
• [x] Lean Language Reference Reading Proof States
• [x] NASA Formal Requirements Elicitation Tool
• [x] NASA SW-VnV FRET User Manual
• [x] Conrad et al. (2022) A Compositional Proof Framework for FRETish Requirements
• [x] Microsoft Z3 Guide Optimization
• [x] Microsoft Z3 Guide Soft Constraints
• [x] Microsoft Z3 Guide Cores and Satisfying Subsets
• [x] Microsoft Z3 Guide Parameters
• [x] Bjorner et al. (n.d.) Programming Z3
• [x] Leofante et al. (2018) Automated Verification of Neural Networks: Advances, Challenges and Perspectives
• [ ] Open Policy Agent Documentation - identified parent documentation page, but narrower consulted pages above were used for extractable claims
• [ ] The Lean Theorem Prover - identified parent documentation page, but the consulted tactic and proof-state pages above were more specific
• [ ] Katz et al. (2023) Formal Verification of Neural Networks: Advances and Challenges - identified in the seed list, but the linked identifier resolves to an unrelated paper, so it was not used as evidence here