Klythos v4.0

A provably-bounded, compositional AI architecture. Seven pillars, each enforcing one constraint of a single characteristic optimization, each backed by a mathematical guarantee that is machine-checked — exhaustively over a finite model, and by SMT over unbounded reals.

$ python -m klythos prove
[PROVED] G1 governor safety (all reals)
[PROVED] G2 governor Lyapunov (all reals)
[PROVED] G3 governor invariance is inductive (all reals)
[PROVED] V1 valve budget (all reals)
[PROVED] V2 odometer monotone (all reals)
[PROVED] V3 valve invariance is inductive (all reals)
[PROVED] L1 Lambda-valve conjunction (all reals)

The idea in one paragraph

There is no "most secure and most functional" AI — security and capability trade off, so the achievable systems form a Pareto frontier, not a peak. Klythos poses the solvable version instead: maximize functionality subject to explicit security, privacy, safety, and calibration constraints, with the trade-off exposed as tunable dials rather than hidden in a black box. Each pillar enforces one constraint; the security-critical gates are kept small enough to verify, and then actually verified.

Quickstart

cd klythos_pkg
python -m demo                 # narrated end-to-end run (rich, with slow-drip)
python -m pytest -q            # 17 tests, each verifying one guarantee

python -m klythos demo         # same run via the CLI
python -m klythos accountant   # basic vs advanced vs RDP composition, side by side
python -m klythos verify-core   # exhaustive machine-checked proofs (finite model)
python -m klythos prove         # SMT proofs over ALL REALS (Z3, unbounded)
python -m klythos ask private_count --dept Research      # one query through the pipeline
python -m klythos ask bulk_export --approve              # class-K with approvals
python -m klythos demo --save-audit audit.jsonl          # persist the audit chain
python -m klythos verify audit.jsonl                     # re-verify it (detects tampering)
python -m klythos config klythos.json                    # write the default operating point

No third-party dependencies for the library (pure stdlib); only pytest for tests, plus optional z3-solver for prove.

The operating point (klythos.json)

Every dial that places Klythos on the security-functionality frontier is data: tau (uncertainty threshold), alpha (conformal coverage), accountant (basic | rdp), delta, user_epsilon_budget, dp_query_epsilon, safe_level/v_max (governor), k_attesters (interlock), signing, and audit path. A medical Klythos and a creative-writing Klythos are the same code with different values here. Run with --config your.json.

Layout

File	Pillar / role	Guarantee
klythos/lattice.py	1 Lattice	information-flow non-interference
klythos/sheaf.py	2 Sheaf	consistency gluing + OOD abstention
klythos/governor.py	3 Governor	Lyapunov boundedness (V <= V_max)
klythos/confessor.py	4 Confessor	conformal coverage >= 1-alpha
klythos/lambda_valve.py	5 Lambda-valve	bounded cumulative leakage
klythos/contract.py	6 Contract	signed, unforgeable proof-carrying outputs
klythos/tribunal.py	7 Tribunal	k-of-n interlock (P <= prod p_i)
klythos/envelope.py	Envelope	Laplace + Gaussian DP, persistent audit chain
klythos/accountant.py	Accounting	basic / advanced / Renyi-DP composition
klythos/experts.py	Adapters	plug real models (incl. Anthropic API) behind the gates
klythos/config.py	Config	the operating point as data
klythos/klythos.py	Orchestrator	wires all seven into answer()
klythos/__main__.py	CLI	demo / ask / accountant / verify / config

Documents

• SPEC.md — the formal specification and honest provable-vs-open accounting.
• THREAT_MODEL.md — assets, adversaries, assumptions, residual risk. Edit first.

Honest scope

The experts are still toy database lookups by default, but experts.py shows how to place real models (including live Anthropic-API calls) behind the identical gates — the security-critical parts don't change, which is the whole design thesis: verify the small gates, not the large crowd. See SPEC.md §4.

Status and scope

Klythos is a reference architecture, not an audited production security product. The proofs establish that the gates obey their specified rules; they cannot establish that those rules fit your deployment — that is what THREAT_MODEL.md is for, and you are expected to rewrite it. See SECURITY.md for the full statement of scope and how to report a vulnerability, and SPEC.md §4 for what is provable today versus what remains open research.

License

MIT — see LICENSE.