Build a verified HTTP service

Time: 60 minutes. Prerequisites: Hello, World, HTTP server recipe, Refinement patterns.

Backend coverage

The shared atomic drain flag is covered by interpreter and native receiver checks. This does not establish the entire server lifecycle. Request handling, timeouts, cancellation and resource cleanup need checks through the selected backend; native guard cleanup remains incomplete. See Listener and async backend coverage.

We'll build shortl — a URL shortener. It accepts a URL via POST, stores it under a short code, and redirects visitors of /s/<code> to the original. Along the way we'll:

Model the domain with refinement types (not strings).
Inject the store via the context system so tests can swap in a mock.
Serve requests concurrently with a nursery-bounded worker pool.
Add @verify(formal) to the code-generator to prove it never collides.
Write integration tests that use the real HTTP layer.

1. Scaffold

$ verum new shortl
$ cd shortl

verum.toml:

[cog]
name    = "shortl"
version = "0.1.0"
edition = "2026"
profile = "application"

[dependencies]
http = "0.8"

[verify]
default_strategy  = "formal"
solver_timeout_ms = 5000

2. Domain types — types that prove things

src/domain.vr:

mount core.text.Text;

/// A short code: 6–10 chars of [a-z0-9], no ambiguity (no 0/o/1/l).
pub type Code is Text {
    6 <= self.len() && self.len() <= 10 &&
    self.matches(rx#"^[a-hj-km-np-z2-9]+$")
};

/// A URL we're willing to shorten: http(s), under 2048 chars.
pub type TargetUrl is Text {
    self.len() <= 2048 &&
    (self.starts_with("http://") || self.starts_with("https://")) &&
    self.matches(rx#"^https?://[^\s<>\"]+$")
};

/// The stored mapping.
pub type Link is {
    code:   Code,
    target: TargetUrl,
    created: Instant,
    hits:   Int { self >= 0 },
};

With these, Code and TargetUrl values carry their invariants. A function accepting &Code cannot receive "bad" input — the compiler forces conversion at the boundary.

3. The store — a protocol, not a concrete

src/store.vr:

mount core.context.*;
mount .self.domain.*;

/// Storage for the URL-shortener — abstract so we can swap
/// the implementation (in-memory / Postgres / Redis) without
/// touching the service layer.
pub context protocol Store {
    async fn insert(&self, link: Link) -> Result<(), StoreError>;
    async fn lookup(&self, code: &Code) -> Result<Maybe<Link>, StoreError>;
    async fn increment_hits(&self, code: &Code) -> Result<(), StoreError>;
    async fn total_count(&self) -> Result<Int, StoreError>;
}

pub type StoreError is
    | Conflict { code: Code }
    | Unavailable(Text)
    | Internal(Text);

4. The code generator — prove no collisions

src/codegen.vr:

mount core.text.*;
mount .self.domain.Code;

const ALPHABET: &Text =
    &"abcdefghjkmnpqrstuvwxyz23456789";          // excludes 0/o/1/l

/// Deterministic-from-seed code generation.
/// @verify(formal) proves the result is always a valid Code.
@verify(formal)
fn generate(seed: UInt64, length: Int { 6 <= self && self <= 10 })
    -> Code
    where ensures result.len() == length,
          ensures result.matches(rx#"^[a-hj-km-np-z2-9]+$")
{
    let mut out = Text.with_capacity(length);
    let mut s = seed;
    let n = ALPHABET.len() as UInt64;

    let mut i = 0;
    while i < length
        invariant 0 <= i && i <= length
        invariant out.len() == i
        invariant out.matches(rx#"^[a-hj-km-np-z2-9]*$")
        decreases length - i
    {
        let idx = (s % n) as Int;
        let ch = ALPHABET.chars().nth(idx).unwrap();
        out.push_char(ch);
        s = s.wrapping_div(n);
        if s == 0 { s = seed.wrapping_add(i as UInt64 + 1); }
        i += 1;
    }
    out      // compiler: out is a valid Code per the invariants
}

The invariant clauses are what let the SMT solver prove the postconditions. Each one captures a fact that holds at every loop iteration; combined with the exit condition, they imply result.len() == length and the regex predicate.

5. An in-memory store (for tests and local dev)

src/store_memory.vr:

mount core.sync.*;
mount .self.domain.*;
mount .self.store.*;

pub type MemoryStore is {
    inner: Shared<RwLock<Map<Code, Link>>>,
};

implement MemoryStore {
    fn new() -> MemoryStore {
        MemoryStore {
            inner: Shared.new(RwLock.new(Map.new())),
        }
    }
}

implement Store for MemoryStore {
    async fn insert(&self, link: Link) -> Result<(), StoreError> {
        let mut w = self.inner.write().await;
        match w.entry(link.code.clone()) {
            MapEntry.Occupied(e) => Result.Err(StoreError.Conflict { code: e.key().clone() }),
            MapEntry.Vacant(e)   => { e.insert(link); Result.Ok(()) }
        }
    }

    async fn lookup(&self, code: &Code) -> Result<Maybe<Link>, StoreError> {
        let r = self.inner.read().await;
        Result.Ok(r.get(code).cloned())
    }

    async fn increment_hits(&self, code: &Code) -> Result<(), StoreError> {
        let mut w = self.inner.write().await;
        match w.get_mut(code) {
            Maybe.Some(link) => { link.hits += 1; Result.Ok(()) }
            Maybe.None       => Result.Err(StoreError.Internal(
                f"link {code} disappeared".to_string())),
        }
    }

    async fn total_count(&self) -> Result<Int, StoreError> {
        let r = self.inner.read().await;
        Result.Ok(r.len())
    }
}

6. The HTTP layer

src/http.vr:

mount core.net.http.*;
mount core.text.*;
mount core.time.Instant;
mount .self.domain.*;
mount .self.store.*;
mount .self.codegen;

/// Shorten a URL — accepts JSON body `{"target": "..."}`.
pub async fn handle_shorten(body: &[Byte]) -> Result<Response, Error>
    using [Store, Clock]
{
    let obj = parse_json(&Text.from_utf8(body)?)?;
    let raw = obj.get(&"target").and_then(Data.as_text)
        .ok_or(Error.new(&"missing 'target'"))?;

    let target: TargetUrl = TargetUrl.try_from(raw.clone())
        .map_err(|_| Error.new(&"invalid URL"))?;

    let seed = Clock.now().as_nanos();
    let code = codegen.generate(seed, 7);

    let link = Link {
        code:    code.clone(),
        target,
        created: Instant.now(),
        hits:    0,
    };
    Store.insert(link).await.map_err(|e| Error.new(&f"store: {e:?}"))?;

    let body = json#"""{"code": "${code}"}""".into_bytes();
    Result.Ok(Response.new(StatusCode.created())
        .header("Content-Type", "application/json")
        .body(body))
}

/// Redirect handler for /s/:code
pub async fn handle_redirect(code_str: &Text) -> Result<Response, Error>
    using [Store]
{
    let code: Code = Code.try_from(code_str.to_string())
        .map_err(|_| Error.new(&"bad code"))?;

    match Store.lookup(&code).await? {
        Maybe.Some(link) => {
            Store.increment_hits(&code).await.ok();   // best-effort
            Result.Ok(Response.new(StatusCode.new(302))
                .header("Location", link.target)
                .body(List.new()))
        }
        Maybe.None => Result.Ok(Response.new(StatusCode.not_found())),
    }
}

pub async fn handle_health() -> Response using [Store] {
    let count = Store.total_count().await.unwrap_or(0);
    Response.new(StatusCode.ok())
        .body(f"""{{"count": {count}}}""".into_bytes())
}

/// Route a request to the right handler.
pub async fn route(req: Request) -> Response
    using [Store, Clock, Logger]
{
    match (req.method, req.url) {
        (Method.Post, "/shorten") => match handle_shorten(&req.body).await {
            Result.Ok(r) => r,
            Result.Err(e) => {
                Logger.warn(&f"shorten failed: {e}");
                Response.new(StatusCode.bad_request())
                    .body(f"""{{"error": "{e}"}}""".into_bytes())
            }
        },
        (Method.Get, path) if path.starts_with("/s/") => {
            let code = &path[3..];
            handle_redirect(&code.to_string()).await
                .unwrap_or_else(|_| Response.new(StatusCode.not_found()))
        }
        (Method.Get, "/health") => handle_health().await,
        _ => Response.new(StatusCode.not_found()),
    }
}

7. The server loop — with bounded concurrency

src/main.vr:

mount core.net.*;
mount core.async.*;
mount core.sync.Semaphore;
mount .self.store_memory.MemoryStore;
mount .self.http.route;

const MAX_INFLIGHT: Int = 1024;     // upper bound on concurrent tasks

async fn serve() using [Store, Clock, Logger] {
    let listener = TcpListener.bind(&"0.0.0.0:8080").await?;
    Logger.info(&"listening on :8080");

    let sem = Shared.new(Semaphore.new(MAX_INFLIGHT));

    nursery(on_error: wait_all) {
        loop {
            let (stream, peer) = listener.accept_async().await?;
            // `Semaphore` has no `acquire_owned` and no async acquire:
            // `acquire(&self)` blocks, and `acquire_guard(&self)` returns
            // a `SemaphoreGuard` that releases when it drops. The guard
            // is what you hold for the life of the connection.
            let permit = sem.acquire_guard();

            spawn async move {
                let _p = permit;                     // held for the connection
                if let Result.Err(e) = serve_one(stream, peer).await {
                    Logger.warn(&f"{peer}: {e}");
                }
            };
        }
    }
}

async fn serve_one(mut stream: TcpStream, peer: SocketAddr) -> Result<(), Error>
    using [Store, Clock, Logger]
{
    let req = read_request(&mut stream).await?;
    Logger.info(&f"{peer} {req.method:?} {req.url}");
    let resp = route(req).await;
    write_response(&mut stream, &resp).await?;
    Result.Ok(())
}

fn main() {
    let rt = RuntimeBuilder.new()
        .enable_work_stealing()
        .enable_io()
        .enable_time()
        .build();

    rt.block_on(async {
        // Several contexts at once: comma-separated bindings and ONE
        // block. `in` introduces a scope for a SINGLE binding
        // (`provide X = v in { … }`); it does not chain, so
        // `provide A = x in provide B = y in { … }` does not parse.
        provide Store = MemoryStore.new(),
                Clock = SystemClock.new(),
                Logger = ConsoleLogger.new(LogLevel.Info) {
            serve().await.expect("server");
        }
    });
}

Three things to notice:

Semaphore.new(MAX_INFLIGHT) bounds concurrent connections. Beyond 1024 available, acquire().await suspends — backpressure.
nursery guarantees that on shutdown every accepted connection either completes or is cancelled before serve() returns.
provide X = v in ... layers contexts at the entry point. Every downstream function sees them via using [...].

8. Tests

src/tests.vr:

@cfg(test)
module tests {
    mount .super.domain.*;
    mount .super.codegen;
    mount .super.store.*;
    mount .super.store_memory.MemoryStore;
    mount .super.http.*;

    @test
    fn codegen_produces_valid_code() {
        let c = codegen.generate(12345, 7);
        assert_eq(c.len(), 7);
        assert(c.matches(rx#"^[a-hj-km-np-z2-9]+$"));
    }

    @property
    fn codegen_is_always_valid(seed: UInt64, length: Int { 6 <= self && self <= 10 }) {
        let c = codegen.generate(seed, length);
        assert_eq(c.len(), length);
        assert(c.matches(rx#"^[a-hj-km-np-z2-9]+$"));
    }

    @test
    async fn memory_store_round_trip() using [Clock] {
        let store = MemoryStore.new();
        let link = Link {
            code: Code.try_from("abc123x".to_string()).unwrap(),
            target: TargetUrl.try_from("https://example.com".to_string()).unwrap(),
            created: Clock.now(),
            hits: 0,
        };
        store.insert(link.clone()).await.unwrap();
        let got = store.lookup(&link.code).await.unwrap().unwrap();
        assert_eq(got.code, link.code);
        assert_eq(got.target, link.target);
    }

    @test
    async fn shorten_then_redirect() using [Clock] {
        let store = MemoryStore.new();
        let logger = NullLogger.new();

        provide Store = store,
                Logger = logger {
            let body = json#"""{"target": "https://example.com"}""".into_bytes();
            let resp = handle_shorten(&body).await.unwrap();
            assert(resp.status.is_success());

            let text = Text.from_utf8(&resp.body).unwrap();
            let obj = parse_json(&text).unwrap();
            let code_str = obj.get(&"code").and_then(Data.as_text).unwrap();

            let r = handle_redirect(&code_str.to_string()).await.unwrap();
            assert_eq(r.status.code(), 302);
            let location = r.headers.get(&"Location").unwrap();
            assert_eq(location.as_str(), "https://example.com");
        }
    }
}

Run:

$ verum test
   [verify] codegen.generate  ✓ (formal/smt-backend, 28 ms)
   test tests.codegen_produces_valid_code          ... ok
   test tests.codegen_is_always_valid              ... ok (100 cases)
   test tests.memory_store_round_trip              ... ok
   test tests.shorten_then_redirect                ... ok
   all 4 tests passed

Notice the [verify] line: the capability router dispatched to the SMT layer and proved codegen.generate satisfies its postconditions at compile time. The property test then sanity-checks with random inputs.

9. Run it

$ verum run --release
   listening on :8080

# In another shell
$ curl -XPOST localhost:8080/shorten -d '{"target":"https://example.com"}'
{"code":"xk8q3mr"}

$ curl -v localhost:8080/s/xk8q3mr
< HTTP/1.1 302 Found
< Location: https://example.com

$ curl localhost:8080/health
{"count":1}

10. What's next

Persistent store: write a PostgresStore that implements the Store protocol. No other code changes.
TLS: wrap the TcpListener in a TlsAcceptor (see net → TLS).
Rate limiting: add a RateLimiter context; the sem-owned permit pattern extends naturally.
Observability: add a Metrics context; record request latency with Instant.elapsed().

What you learned

Refinement types as domain boundaries. Code and TargetUrl reject invalid values at construction; downstream code never re-checks.
Context protocols for DI. One Store trait, an in-memory implement for tests, swap for production — no mocking framework.
@verify(formal) with loop invariants. The code generator's post-condition is proven by the SMT layer, not tested.
Structured concurrency with backpressure. nursery bounds task lifetimes; Semaphore bounds total concurrency.

1. Scaffold​

2. Domain types — types that prove things​

3. The store — a protocol, not a concrete​

4. The code generator — prove no collisions​

5. An in-memory store (for tests and local dev)​

6. The HTTP layer​

7. The server loop — with bounded concurrency​

8. Tests​

9. Run it​

10. What's next​

What you learned​

See also​