FX is a compiler and proof assistant built on graded dependent type theory. It tracks fifteen orthogonal properties of every value through a single grade-checking algorithm. The type of a function is its complete specification: what it computes, what resources it consumes, what effects it performs, what information it leaks, and what protocols it follows. Programs that compile are correct by construction. The compiler verifies itself.
FX targets x86, ARM, and FEU, a ternary clockless wavefront processor. On FEU, the operating system is written in FX, the ISA is specified in FX, and hardware is verified in FX.
The compiler checks twelve dimensions with mathematical certainty and three with conservative bounds:
| Dimension | What the compiler checks |
|---|---|
| Type safety | values have the types declared |
| Refinements | properties like x > 0 hold where needed |
| Usage | linear values consumed exactly once, no use-after-free, no leaks |
| Effects | pure functions perform no IO, no allocation, no mutation |
| Security | secret inputs do not determine public outputs |
| Protocols | channels follow declared message sequences |
| Lifetimes | references do not outlive their data |
| Provenance | data lineage tracked from source through transformations |
| Trust | code paths with sorry or axiom flagged transitively |
| Representation | memory layout matches declared format |
| Observability | constant-time code has no secret-dependent branches or memory access |
| Clock domains | no unsynchronized cross-domain signal references in hardware |
| Complexity | operation count upper bounds from termination proofs |
| Precision | floating-point error accumulation through computation |
| Space | allocation upper bounds per function |
Graded modal type theory. Every binding carries a grade vector from a product of resource semirings. The compiler checks all dimensions in one pass through the same algorithm. User-defined semirings extend the system to domain-specific resource tracking.
Separation logic as a grade. The usage dimension is a permission algebra (partial commutative monoid). Separating conjunction is grade composition. The frame rule falls out of the typing rules. Fractional permissions enable verified concurrent sharing.
Algebraic effects with handlers. Effects are declared, not inferred. Handlers remove effects from the type. One-shot continuations compile to CPS with zero overhead. Effect variables enable higher-order functions that preserve caller effects.
Algebraic structure intrinsics. The compiler knows about monoids, rings, fields, and lattices. It uses algebraic laws for optimization and provides ring, field, linarith tactics for proof automation without SMT.
Bit-precise dependent types. bits(n) with compile-time width, bit-slice syntax, and concatenation. ISA specifications are executable FX functions that generate emulators, decoders, and formal models from a single source.
Constant-time verification. The CT effect proves that execution traces are independent of secret-graded inputs. Crypto code is verified correct and constant-time simultaneously.
VLIW compilation from types. Effects determine instruction independence, ownership eliminates alias ambiguity, refinements provide exact loop bounds. The type system gives VLIW schedulers the information that C compilers lack.
Runtime checks exist where unproven data enters the proven world (network input, file contents, FFI returns) and where the program interacts with unverified systems. The compiler detects these boundaries and generates validators from refinement predicates. Everywhere else, proofs are erased with zero runtime cost.
Stateful abstractions are codata types with graded self parameters. Subtyping is structural. Dynamic dispatch uses existential types. The grade system prevents use-after-close, double-close, and concurrent mutation at compile time.
Phase 1 — graded usage checking. Permission algebra in the type checker, linear and affine enforcement, fractional sharing.
Phase 2 — effect handlers and security. Handler typing, effect row polymorphism, information flow checking, constant-time verification.
Phase 3 — algebraic intrinsics and trust boundaries. Compiler-known algebraic structures, tactic-based proof automation, trust boundary detection with auto-generated validators.
Phase 4 — sessions, lifetimes, and hardware. Session type checking with duality and deadlock freedom, region variables, clock domain grade, bit-precise types.
Phase 5 — self-verification. Remove --lax from compiler source, verify the type checker kernel, normalizer, and SMT encoding.
FX extends F* (FStarX). The parser recognizes ownership, effect, security, session, and hardware syntax. The type checker enforces dependent types, refinements, and effects. Graded checking is the current implementation focus. The compiler bootstraps through OCaml extraction with a stage0 → stage1 → stage2 fixpoint cycle.
Prerequisites: OCaml 5.4+, Z3 4.13+, GNU Make.
make 1.full # build stage-1 compiler + verify ulib
make test-compiler-1 # run compiler test suite
Apache 2.0. See LICENSE.