|
Important
|
This repository is not a collection of production-ready or formally verified
server implementations. It contains protocol models, Idris2 source, Zig FFI
prototypes, native-binding source, and scaffolding with varying levels of
implementation and verification. Directory counts are inventory only. Do not
infer security, interoperability, or release readiness from the name
|
The repository is a monorepo of protocol and connector models, per-package FFI experiments, language-binding sources, documentation, and audit artefacts. As of 2026-09-27, its top-level directory inventory is:
| Area | Directories | What the count means |
|---|---|---|
|
88 |
Protocol-named package directories; not 88 working servers. |
|
5 |
|
|
6 |
|
|
20 |
Language-named source directories; not 20 supported or tested bindings. |
The protocol directory names are:
agentic airgap amqp apiserver appserver authserver backup bfd
ca cache caldav carddav chat coap configmgmt ctlog dds
deception diode doh doq dot epistemic federation fileserver
ftp gameserver git graphdb graphql grpc hardened honeypot
http3 ids imap irc kerberos kms ldap ldp loadbalancer
logcollector lpd mcp mdns media metrics modbus monitor mqtt
nesy netconf neurosym objectstore ocsp odns opcua ospf pop3
pqc proxy ptp quic radius rtsp sandbox sdn semweb siem
smb smtp snmp socks sparql stun tacacs telnet timestamp
triplestore virt voip vpn wasm webdav ws xmpp zerotrust
An Idris2 proof, when the relevant .ipkg builds successfully with the declared
compiler, is a proof about the proposition encoded in that Idris2 model. It does
not by itself prove that a separate Zig implementation, generated header,
network service, or language binding conforms to the model. That relationship
requires independently reproducible conformance tests and a verified bridge;
there is no repository-wide machine-checked proof of that relationship here.
Build and test evidence is package- and revision-specific. The recorded audits
under audits/ are dated snapshots, not evidence for later source changes. The
shell checks under tests/ are source-pattern heuristics or partial samples;
they are not formal proofs, exhaustive protocol conformance suites, or security
certifications. Several operations intentionally fail closed rather than claim
functionality: for example, the OCaml native calls raise an unavailable error,
Authserver authentication is rejected, PQC operations reject, and DNSSEC
signing/validation are unavailable.
Before treating any component as usable, inspect its own README and ABI, build it with the declared toolchain, run its implementation tests, verify generated artifacts, and assess its protocol/security requirements. Do not use this repository as a production server or cryptographic implementation on the strength of these sources alone.
proven-servers/
├── protocols/ # 88 protocol-named source packages
├── core/ # Shared model/FFI packages
├── connectors/ # Connector and integration packages
├── bindings/ # 20 language-named source directories
├── not-proven/ # Explicitly non-proven examples/prototypes
├── tests/ # Sample runtime and source-pattern checks
├── audits/ # Dated historical audit records
├── generated/ # ABI/header artefacts; generation status varies
├── ffi/ # Root-level Zig FFI sources
├── src/abi/ # Root-level Idris2 ABI sources
└── .machine_readable/ # State, policies, registry, and agent guidanceMost protocol packages keep source, .ipkg files, Zig build.zig files,
tests, and generated ABI artefacts under that package. Presence and coverage
vary; there is no requirement that every directory provide every layer.
bindings/ contains 20 language-named directories. This is an inventory, not a
supported-language promise. Many directories contain only declarations or
source wrappers, and their native linking and tests have not been re-established
as a single cross-language matrix. The OCaml tree is explicitly unavailable
until OCaml-compatible C stubs are implemented; Java/Kotlin native method
declarations likewise do not establish that a JNI bridge exists. See
.machine_readable/BINDINGS.a2ml and bindings/ocaml/README.adoc for the
current qualifications.
The top-level Justfile is the task entry point. just build and just test
are intended to run real Idris2/Zig checks and fail if required tools are
missing; they are not success-printing placeholders. bash tests/e2e.sh runs a
selected Idris2/Zig package test sweep; it requires both compilers and does not
establish cross-language conformance or a full E2E server.
bash tests/source_smoke_test.sh, bash tests/aspect/security_test.sh, and
bash tests/binding_inventory.sh are explicitly static/source-inventory checks;
they do not execute language bindings or prove cross-language conformance.
The 2026-06-23 audit reports are historical. In the current audit environment
Idris2, Zig, OCaml, Dune, and Just were unavailable, so no build or test suite
could be run here. See READINESS.adoc and PROOF-NEEDS.adoc for the present
status and concrete evidence needed next.
No validated executable server or release artifact is produced by this
repository. Root container/cloud deployment, package release, and Pages
publishing automation are disabled or removed; prototype source under
connectors/ is not a deployment target. Do not infer operational readiness
from a Containerfile, endpoint name, deployment script, or workflow without
reproducible package and runtime evidence.