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

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.

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.

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

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

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

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

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