Native Code

The form that was verified is the form that runs: native machine code, no garbage collector.

The policy that was proved is the policy that runs. Scope-Forge lowers the policy into Pancake once, and the CakeML toolchain, a compiler whose correctness is itself machine-checked, takes it to native machine code for ARMv7, ARMv8, x86-64, RISC-V and MIPS-64, and for Silver, the instruction set of a processor whose own design is formally verified. A verified front end, a verified compiler, and a verified back end: what you see is what you run. Every verified system trusts its toolchain. Scope-Forge's trusted base is small, and every item on it is listed.

The same compiled policy runs wherever the decision is made, and compiled policies integrate with existing applications and specialized systems through a dedicated Scope-Forge code generator.

• Data center servers
• Existing applications
• Specialized systems
• Low-power field equipment

Everything already decided at compile time is removed, so the running system executes only the checks that remain, and text checks run in a single pass over the input. The clearance band, the mission window, and the subset relation below are settled before the policy ever runs; what runs is the membership check on the live request. A policy that breaks a stated rule does not build.

Operator requires {
    station: str where in ("A".."Z")+ ++ ("0".."9")+
    clearance: num where in 1..5
    action: str where in "read" || "task" || "release"
}

MissionOperator requires Operator && {
    clearance: num where in 3..4
    mission_window: num where in 1400..2200
    action: str where in "read" || "task"
}