Skip to main content

​
Policy Circuits

Policy circuits are PCD programs that act as deterministic guardrails for AI systems. Unlike traditional rule engines or RLHF alignment, a policy circuit is formally verified (Φ_c = 1) and cannot be bypassed, updated, or overridden at runtime.
A policy circuit is a regular PCD circuit that takes an action as input and emits ALLOW or BLOCK as output. Because PCD is deterministic, the same action always produces the same verdict.

​
Why Policy Circuits?

Traditional GuardsPolicy Circuits
Code that can be patchedImmutable verified circuit
Runtime exceptionsCompile-time rejection
Probabilistic (RLHF)Deterministic (Φ_c = 1)
Trust the developerTrust the math

​
Quick Start

​
Create a Policy

brikc policy new --template sandbox
This generates a .pcd file from a built-in template. Five templates are available:
TemplateDescription
no_networkBlocks all network I/O operations
no_filesystemBlocks all filesystem access
memory_boundEnforces memory allocation limits
sandboxCombines no_network + no_filesystem + memory_bound
allow_allPermits all actions (useful as a starting point)

​
Verify a Policy

brikc policy verify my_policy.pcd
Verification checks that Φ_c = 1 for the policy circuit. If the circuit has dead branches, unreachable paths, or ambiguous verdicts, verification fails and the policy cannot be deployed.

​
Pre-Built Policies

​
no_network

PC no_network {
    fn check(action: Action) -> Verdict {
        match action.category {
            "net_connect" => BLOCK,
            "net_listen"  => BLOCK,
            "net_send"    => BLOCK,
            "net_recv"    => BLOCK,
            _             => ALLOW,
        }
    }
    OUTPUT check;
}

​
memory_bound

PC memory_bound {
    domain mem_limit: Range [0, 536870912]; // 512 MB

    fn check(action: Action) -> Verdict {
        match action.category {
            "mem_alloc" => {
                let requested = action.params.bytes;
                if requested > mem_limit.max {
                    BLOCK
                } else {
                    ALLOW
                }
            },
            _ => ALLOW,
        }
    }
    OUTPUT check;
}

​
Example: Robot Arm Force Limiter

A policy circuit that prevents a robotic arm from exceeding safe force thresholds: 
PC robot_arm_force_limiter {
    domain force_newton: Range [0, 50];    // max 50 N
    domain speed_mms:    Range [0, 500];   // max 500 mm/s

    fn check(action: Action) -> Verdict {
        match action.category {
            "motor_move" => {
                let f = action.params.force;
                let s = action.params.speed;
                if f > force_newton.max {
                    BLOCK
                } else if s > speed_mms.max {
                    BLOCK
                } else {
                    ALLOW
                }
            },
            "motor_grip" => {
                let f = action.params.force;
                if f > force_newton.max {
                    BLOCK
                } else {
                    ALLOW
                }
            },
            _ => ALLOW,
        }
    }
    OUTPUT check;
}

brikc policy verify robot_arm_force_limiter.pcd
# ✓ Φ_c = 1 — all paths terminate with ALLOW or BLOCK

​
Example: LLM Output Filter

A policy circuit that blocks LLM responses containing prohibited content patterns: 
PC llm_output_filter {
    fn check(action: Action) -> Verdict {
        match action.category {
            "llm_response" => {
                let text = action.params.content;
                if STR_CONTAINS(text, "EXECUTE_SQL") {
                    BLOCK
                } else if STR_CONTAINS(text, "rm -rf") {
                    BLOCK
                } else if STR_LEN(text) > 100000 {
                    BLOCK
                } else {
                    ALLOW
                }
            },
            _ => ALLOW,
        }
    }
    OUTPUT check;
}

​
Writing Custom Policies

1
Define the action space
2
Identify which action categories your system emits. Each action has a category string and a params record.
3
Declare closure domains
4
Use domain declarations for numeric constraints. This gives the TCE engine the information it needs to verify completeness.
5
Write the check function
6
Pattern-match on action.category and return ALLOW or BLOCK for every path. The circuit must be total — every possible input must reach a verdict.
7
Verify
8
Run brikc policy verify <file> to confirm Φ_c = 1. Fix any dead branches or uncovered paths.
9
Compile to target
10
brikc compile my_policy.pcd --target js    # JavaScript guard function
brikc compile my_policy.pcd --target py    # Python guard function
brikc compile my_policy.pcd --target rust  # Rust guard function
A policy circuit that does not cover all action categories will fail verification. Always include a wildcard _ => ALLOW or _ => BLOCK as the final match arm.