Scope-Forge
The proven policy compiler. A policy is a precise set; a policy that contradicts itself does not build, and the proved policy runs as native machine code.
Verification
Proven, not just tested.
The scale of the proof
Over 150,000 lines of verified Rust code, specification, and proof.
About 54,000 lines of running code.
About 100,000 lines of machine-checked specification and proof.
More than 70 verified crates.
More than 7,400 functions, lemmas, and specifications checked with zero errors.
More than 16,000 machine-checked pre- and postconditions and loop invariants.
Over 4,700 verified functions, all machine-checked.
Fewer than 300 explicitly marked trusted primitives beneath them.
Every line of verified code carries nearly two lines of machine-checked specification and proof.
One sum, one run. About 54,000 lines of running code and about 100,000 lines of specification and proof make over 150,000 lines of verified Rust, nearly two to one. Every figure comes from a single measured run of Verus, built from commit 2de0e24, on October 6, 2026, with zero errors.
01Proof
Checked for every possible input, not a sample
Testing checks the cases someone thought of. An attacker looks for the case nobody thought of. A machine-checked proof covers every possible input, so there is no untested case left to find.
The Scope-Forge compiler and the verified core libraries are checked with Verus, an SMT-backed verifier for Rust: the developer writes a specification of what the code does, and Verus checks that the executable Rust code satisfies it for all possible executions, with the Z3 solver discharging each proof obligation (Verus guide). More than 7,400 such functions, lemmas, and specifications check with zero errors.
Policy properties become build-time facts, with a concrete counterexample when a rule fails.
Policy mistakes are caught before anything is deployed.
Machine-checked with Verus
02Trust
A small trusted base, stated plainly
Every verified system rests on something taken on trust, and every one of them trusts its toolchain. The seL4 microkernel assumes that its assembly code, its boot code, and its hardware behave correctly, and trusts its compiler and linker on the platforms its binary verification does not cover (seL4 proof assumptions). CompCert proves about 90 percent of its algorithms in Rocq; elaboration, presimplifications, assembling, and linking are not verified (CompCert manual). Of these, only CakeML has compiled itself inside the logic (CakeML), and Candle, a fully verified theorem prover, runs on top of it (Candle). That is the exception, not the standard. The question for an evaluator is never whether a trusted base exists. It is how small it is, and whether it is written down.
IronVelo's is small. Here it is, by kind.
- 001Fewer than 300 explicitly marked trusted primitives inside the verified libraries, each one individually marked and analyzed, under over 4,700 verified functions.inside the librariesSource: Verified core libraries
- 002The Rust compiler that builds the verified code.toolchainSource: Scope-Forge and the core libraries
- 003Verus, and the Z3 solver it relies on, which check the proofs when IronVelo builds its libraries and compiler.toolchainSource: Scope-Forge and the core libraries
- 004A memory allocator, used only while compiling.toolchainSource: Scope-Forge
- 005The formally verified CakeML back end that carries a compiled policy to native machine code, with what its own proofs rest on.toolchainSource: Scope-Forge
- 006The hardware the code runs on.hardwareSource: Scope-Forge and the core libraries
03Solver
No third-party solver in the decision
Many verification tools hand the hard question to a large outside solver. Scope-Forge decides every policy question with its own verified set arithmetic: whether a policy contradicts itself, whether a request belongs to the set a policy describes, whether a delegated authority is strictly narrower than its parent. No solver runs when a policy is compiled, so there are no solver time-outs and no machine-dependent resource limits. A policy's meaning never depends on how fast a computer is, and anyone re-running the check gets the same answer.
The proofs behind that arithmetic are checked by Verus, over the Z3 solver, when IronVelo builds the compiler; checking a policy runs no solver at all. An auditor needs to trust the compiler's core set operations and the listed toolchain, nothing more.
04Pipeline
The policy that was proved is the policy that runs
What is proved, in plain words: a policy describes exactly which requests are allowed, and granting access is checking whether a request belongs to that set; a policy that contradicts itself, or that no request could ever satisfy, does not build; every security rule the author writes down holds for every possible record, never a sample; and the exact form verified at compile time is the form that runs.
That last point is the pipeline: a verified front end checks the policy, a verified compiler removes everything already decided, and the formally verified CakeML compiler carries the rest to native machine code through Pancake, its low-level language. CakeML is proved to produce only machine code that is compatible with the behavior of its source program (CakeML). The running system executes only the checks that remain. What you see is what you run.
Explicit imports, private-by-default definitions, and module-by-module review mean an auditor can follow every permission to its source, and an audit scales with the size of the change, not the size of the whole policy base.
05Technologies
Three technologies, one standard
IronVelo's critical logic is proven correct by machine-checked mathematics, not just tested. The proofs cover the Scope-Forge compiler and the verified core libraries. IronIdP is built on those libraries; its sign-in flows are correct by construction at the state-transition level, with substantial verification, and its external dependencies are pinned and audited.
IronIdP's permissions are written in Scope-Forge and enforced by the policies Scope-Forge compiles. When a token is split to delegate part of its authority, Scope-Forge checks that the delegated token's authority is strictly narrower than its parent's.
06Foundations
The verified core libraries
Security software is only as sound as the memory handling, data structures, and parsers under it, and that is where classic vulnerabilities live: buffer overruns, leftover secrets in memory, malformed input. IronVelo proves these foundations correct instead of trusting them: a memory model proved down to the byte, ownership tracked by proof, and a secure wipe the compiler cannot optimize away, under strict constraints suited to bounded, deterministic hardware.
- 001Containers holding secrets are proven to zero their old memory before every reallocation and release.secrets wiped, provablySource: Verified core libraries
- 002Allocation never crashes: every operation that needs memory returns an error value when memory runs out and is proven not to crash or unwind.allocationSource: Verified core libraries
- 003A verified high-performance hash map, proven to behave exactly like a mathematical map, including as it grows.hash mapSource: Verified core libraries
- 004A verified serializer proven one-to-one, canonical, and exact on round trip, with proofs generated automatically for users' own data types; verified UTF-8 validation proven equal to its specification, including the accelerated paths.serializer and UTF-8Source: Verified core libraries
A verified stack from raw memory up: memory model, allocators, collections, a Swiss-table hash map, UTF-8, serialization, a regex engine, and a policy compiler.