Program specification
From a well specified surface, ideally two (what comes in, and what must go out), we build a reference implementation and prove that it satisfies the specification.
Specialised API gateway
A faster API gateway, specialised to the configuration you can fix.
A gateway is configured declaratively. We compile in the parts you are willing to fix, and prove the result still does what the specification says. What you need to keep changing stays configurable.
Tell us about your gatewayWhy the gateway
A general gateway reads configuration on the request path that the deployment has already decided. Routes, policies and shard maps are consulted as data, request after request.
Large fleets use gateways for all sorts of routing, including sharding. Every service behind the gateway pays that cost. Taking the repeated work out of the gateway helps everything it routes.
Configurable up to a boundary
You choose what stays open. A route, a policy or a shard map you still want to change at runtime stays configurable, up to the boundary you set. Everything inside that boundary is specialised into the gateway.
Changing a specialised part is not a config edit. The gateway is compiled for that configuration, so those parts change by compiling it again.
Specification, then a faster program
The faster gateway is not a rewrite you have to take on trust. It is checked against the same specification as a reference implementation.
Program refinement
We replace that reference with a faster program, and prove that the faster program satisfies the same specification.
Which gateways are worth it
The same approach fits other systems. A gateway is a clear case, because the configuration is already declarative and the cost is paid on every request.
Well specifiable
The gateway is driven by a declarative configuration simple enough to be the specification. Routes, policies and shard maps that can be written down precisely.
Expensive to run
The gateway sits where compute cost is high, or where latency is expensive. A gateway in front of a large fleet is often both.
Built on vericoding
Vericoding is the method: people review the specification, AI proposes the program and the proof, and a theorem prover checks that the faster program refines the specification. The same idea specialises a database query to the plan the optimiser chose.
Tell us about your gateway
Which parts of the configuration you can fix, which you need to keep open, and where latency or compute cost matters.