A catalog of 108 formally verified server components written in Idris 2 with dependent types: 94 protocol skeletons, 8 core primitives, and 6 connector interfaces.
Each component defines the correct types for its domain: message types, valid states, state transitions, error codes. Machine-checked. Proven safe at compile time.
The 6 connector interfaces have a complete ABI-FFI layer: Idris2 ABI definitions with dependent-type proofs, generated C headers, and Zig FFI implementations with integration tests. Any language that can call C can use them.
This is the core. Nothing else. No frameworks. No opinions. No "batteries included." You get the verified bones. You build the rest.
If you want to learn Idris 2: Read the source. It’s clean, documented, and teaches you both the protocol and the language.
If you never want to touch Idris 2: Use the FFI bindings from Rust, Zig, Elixir, or any of the 10 supported languages. Your server core is still formally verified. You don’t care how. It just is.
Either way, your server’s protocol handling is proven correct.
proven-servers/
├── core/ # 8 primitives (socket, frame, fsm, wire, compose,
│ # tls, config, audit)
├── protocols/ # 94 protocol skeletons
│ ├── proven-dns/ # Each with its own .ipkg and src/
│ ├── proven-smtp/
│ ├── proven-mqtt/
│ └── ...
├── connectors/ # 6 connector interfaces (with ABI-FFI)
│ ├── proven-dbconn/ # Database connections
│ ├── proven-authconn/ # Authentication lifecycle
│ ├── proven-cacheconn/ # Cache connections
│ ├── proven-queueconn/ # Message queue pub/sub
│ ├── proven-resolverconn/ # DNS resolution
│ └── proven-storageconn/ # Object storage
├── abi/ # Idris2 ABI definitions (src/abi/*.idr)
├── ffi/ # Zig FFI layer (ffi/zig/)
└── bindings/ # Language bindings (Rust, Zig, C, ReScript, Gleam,
# Elixir, Haskell, OCaml, Ada, Julia)dns smtp httpd ftp imap pop3 irc xmpp mqtt ldap
radius snmp nfs smb syslog tftp dhcp mdns coap amqp
grpc graphql modbus netconf opcua telnet rtsp voip stun
bgp ospf bfd sdn ptp ntp nts ws
firewall vpn ids siem honeypot deception ca ocsp kms
pqc zerotrust ctlog airgap diode sandbox hardened
authserver kerberos socks tacacs ssh-bastion
proxy loadbalancer apiserver appserver fileserver dbserver
objectstore cache webdav graphdb sparql triplestore semweb ldp
| Connector | Purpose | States |
|---|---|---|
|
Relational databases (query, transaction, prepare) |
5 |
|
Authentication lifecycle (MFA, tokens, lockout) |
6 |
|
Cache connections (TTL, eviction, degradation) |
4 |
|
Message queues (subscribe, publish, ack/reject) |
5 |
|
DNS resolution (13 RR types, DNSSEC, caching) |
4 |
|
Object storage (upload, download, integrity) |
5 |
Each connector has a complete ABI-FFI layer: Idris2 proofs, C headers, Zig FFI,
and integration tests. See connectors/README.adoc for details.
-
Secure by default. If there is a secure and insecure version of something, only the secure version exists here.
-
Minimal. Only the types needed to define protocol correctness. No helpers, no utilities, no extras.
-
Composable. Protocols are atoms. Oblivious DNS is
odnsrelay +dns. An OIDC proxy isproxy+authserver. Compose them; don’t create new skeletons. -
Proven. Every type is total. No
believe_me. Noassert_total. No escape hatches. -
Permanent. Protocol types don’t change. DNS message types from 1987 are still the same types today. This code is meant to last.
-
ABI (Idris 2): Interface definitions with dependent type proofs →
abi/ -
FFI (Zig): C-compatible implementation →
ffi/ -
Bindings: Thin wrappers for 10 languages →
bindings/
See ABI-FFI-README.md for the full standard.