FLUX Certify

Compile FLUX-C guard constraints and generate proof certificates for safety-critical systems.

Overview

FLUX Certify is a Python package + CLI tool for compiling .guard constraint specifications into FLUX-C bytecode and generating proof certificates. Designed for safety-critical deployment in aerospace, automotive, marine, and medical domains.

Installation

pip install flux-certify

CLI Usage

# Compile a guard constraint to FLUX-C bytecode
flux-certify compile "battery_temp in [15, 55] with priority HIGH"

# Generate a proof certificate
flux-certify prove "battery_temp in [15, 55]"

# Generate a signed certificate
flux-certify certify "sonar_frequency in [10, 50]"

# Verify a certificate file
flux-certify verify /path/to/certificate.json

# Show example constraints
flux-certify examples

# Generate signing keys
flux-certify keygen

# Check constraint certification status
flux-certify status "deceleration in [0.1, 0.8]"

Python API

from flux_certify import compile_guard, prove_guard, certify, verify_cert

# Compile
result = compile_guard("battery_temp in [15, 55]")
print(result['asm'])
print(result['guard_hash'])

# Prove
cert = prove_guard("battery_temp in [15, 55]")
print(cert['task_id'])
print(cert['theorem_status'])  # [PROVEN]

# Sign and verify
signed = certify("battery_temp in [15, 55]", signer="my-fleet")
print(verify_cert(signed))  # True

FLUX-C Assembly Format

Each guard constraint compiles to a sequence of FLUX-C opcodes:

; FLUX-C Guard Assembly
; Constraint: battery_temp in [15, 55]
LOAD_IMM  r0, 0xBD16E340  ; battery_temp
LOAD_IMM  r1, 0xBD16E341  ; in
LOAD_IMM  r2, 0xBD16E342  ; 15
LOAD_IMM  r3, 0xBD16E343  ; 55
LOAD_IMM  r0, 0xBD16E344  ; with
LOAD_IMM  r1, 0xBD16E345  ; priority
LOAD_IMM  r2, 0xBD16E346  ; HIGH
VERIFY_GUARD                  ; verify constraint
HALT                          ; end

Proof Certificate Structure

{
  "task_id": "uuid-here",
  "constraint": "battery_temp in [15, 55]",
  "guard_hash": "0xBD16E340",
  "verified": true,
  "prover": "FLUX-Certify-0.1.0",
  "proof_type": "constraint_compilation",
  "flux_c_version": "1.0",
  "theorem": "fluxc_terminates",
  "theorem_status": "[PROVEN]",
  "theorem_description": "All FLUX-C programs halt structurally. No backward jumps, bounded call stack (MAX_STACK=100)."
}

Theoretical Foundation

FLUX-C Turing-Incompleteness Theorem [PROVEN]

Theorem: All FLUX-C programs halt in bounded time.

Proof sketch:

1. All control-flow opcodes are forward-only (no backward jumps)
2. Call stack is bounded by hardware MAX_STACK=100
3. Therefore no infinite loops, no unbounded recursion
4. Every execution path is finite

This is the foundation for formal verification of FLUX-C programs in safety-critical systems.

Theorem status: [PROVEN] — mechanized in Coq (flux-certify/FluxC/FluxC.v)

Key Invariants

License

Apache 2.0

Links

• GitHub: https://github.com/SuperInstance/flux-certify
• FLUX-C ISA: https://github.com/SuperInstance/flux-research
• Dissertation: https://github.com/SuperInstance/flux-research/tree/main/dissertation