pronounced "ser-Q": serving + Queue

serQ describes an LLM serving deployment as a program: its memory pools, engines, workload and scheduling policy. Use the same program to simulate performance, state claims for Lean proofs and draw the deployment. Programs supported by the vLLM target also compile to a scheduler configuration.

Start with installation and a first run, or build a serving model step by step in the tutorial.

What you can do with it

• Simulation

  serq run executes the program as a discrete-event simulation and reports each stage's throughput, utilisation and waits, an engine's inter-token latency, and whatever the program observes (time to first token, say) with a confidence interval. --set supplies declared inputs and --def changes definitions in a constant or a law without editing the file, for sweeps. Getting started, use cases

• Formal verification

  Write claims in a program and prove them about its Lean model, under explicit assumptions. For supported programs and claims, Lean statements are generated from the IR; their proofs are written separately and checked by Lean. The simulator also checks claims on the path it runs. The interpreter and Lean semantics are tested for agreement; their equivalence is not proved. The Lean model, formal verification examples

• Deployment visualization

  serq draw renders the program as a queueing network, in TikZ or SVG. Regenerate the figure when the program changes. Visualization