proof-carrying-code

Five Tests Standard (5TS): a vendor-neutral published standard for verifiable AI governance through proof-carrying decisions. Includes schemas, machine-checkable conformance vectors, and a reference validator.

Coq formalization of a proof carrying code framework for inlined reference monitors in Java bytecode

Type-theoretic verification kernel for formally verified database queries, providing dependent, linear, session, quantitative, effect, and modal type coverage. Idris 2 formal specs, Rust verification kernel, Zig FFI bridge, JSON-RPC protocol. The "LLVM of type safety" for query validation.

Institutional proof-carrying GPU kernel generation with Lean 4, CUDA/PTX, Futhark, and PAX release governance.

A formally-verified Conway's Game of Life engine in which geometry may render the automaton's history but never author it. Exhaustive gates (512/512 local rules; 65,536/65,536 worlds vs an independent oracle) plus a machine-checked Idris2 constitution. A proven foundation — not yet a playable game.

Security-first programming language for building high-assurance services, secure communications, privacy-aware networking tools, policy-enforced runtimes, secret-safe data pipelines, and auditable least-authority systems.

Certificate protocol 0.2.0 and standalone reference verifier for AlchemQ proof-carrying quantum circuit optimization. Optimization engine not included.

Proof-carrying Python — Z3-backed formal verification via @verified decorators

A concept architecture for deadline-typed, proof-carrying neural inference with deterministic resource admission.

A certificate format for machine-checked program admission, and an independent checker for it. Zero dependencies.

Proof-carrying PR verification gate: automated AST invariants, test receipts, and scope fences for AI pull requests

An independent JavaScript checker for certkit program-admission certificates. Exact BigInt rational arithmetic, zero dependencies, runs in the browser.

Check the proof, not the promise — an index of ten open-source artifacts built on the producer/checker asymmetry.