Days runs on one CPU thread, a multicore pool, Apple Metal, or NVIDIA CUDA, and every backend produces the complete state of a serial run, byte for byte. The parallel backends earn their speed under a safe horizon proved in Lean.
=4 captured runs, one fingerprint: d7de73ee33579682
Every backend ends the same scenario with the same fingerprint. These are real runs of the quick-start fixture: Scalar and CPU on an Apple M1 Max, Metal on an Apple M5 Max, CUDA on an NVIDIA GB10.
Up to1,279×
faster than sequential ns-3. UDP, CUDA backend, native clocks, RTX 4090 host
Up to81×
faster than Unison at 24 threads. Same experiment and clocks
3,918×
faster than GeDES on TCP run to full completion. Native clocks, same RTX 4090
0.563 s vs 0.565 s
Days vs GeDES in the densest TCP phase: statistically even on GeDES's own clock
4 backends
Scalar, CPU, Metal, CUDA: one byte-identical complete state
5 theorems
about the scheduling model, proved in Lean on standard axioms only
01Exact
One answer, to the byte.
Every event in Days carries a canonical key: time in integer nanoseconds, then a phase, then the sending process and its sequence number. The key orders every pair of events, simultaneous ones included. The reference result is what you get by always executing the pending event with the least key.
Every backend must produce that result exactly. That means the complete final state, not a set of summary statistics. It must hold at any worker count and any assignment of processes to workers. No floating point appears anywhere in the semantics. Fractional quantities, such as Weighted Fair Queueing finish tags, are computed as exact rationals. Each run ends with an FNV-1a-64 fingerprint of the complete state. Equal fingerprints mean byte-identical results.
On one long open-loop run, six independently configured runs across all four backends and two CUDA architectures returned the same 70,900,544-byte state. That run covered 132,988,928 packets and 2.53 billion transitions.
01
t
time, integer ns
02
phase
then a phase
03
origin
the sending process
04
seq
its sequence number
least key first → canonical serial order → one complete state → fnv1a64
Why it matters
Exactness makes approximation measurable. We aligned Days and GeDES on identical scenarios, with the same sources, routes, and queue capacities, and compared the results. GeDES reports 3.7× the acknowledgment losses and 9.5× the retransmission timeouts, and its completion instant is 11× removed from the exact account of the same workload. Because everything else was equalized, these gaps come from batching events into fixed slots.
Other simulators also depart from their references. Unison departs from sequential ns-3's trajectory even when it runs single-threaded. In drop-free tests, legacy Days in multi-threaded mode returns different packet counts from run to run.
With Days, a misbehaving flow at hour three reappears at hour three on any backend. Bisecting a regression compares two states that are either equal or not. Continuous integration pins the complete final state of every test scenario, so any one-byte change in behavior fails visibly.
GeDES ÷ exact account · aligned TCP workload
GeDES factor
Exact account (1×)
GeDES against the exact account, same TCP workload, aligned configuration. All drops: 721 vs 549 (1.31×). ACK losses: 259 vs 70 (3.7×). Retransmission timeouts: 19 vs 2 (9.5×). Completion instant: 11.0 s vs 1.0 s simulated (11×).› Data table
Metric
Days (exact)
GeDES
GeDES ÷ Days
Unit
All drops
549
721
1.313297
count
ACK losses
70
259
3.7
count
Retransmission timeouts
2
19
9.5
count
Completion instant
1,000,362,708
11,000,362,024
10.996374
simulated ns
02Fast
A horizon that moves with the traffic.
Parallelism comes from lookahead. No packet can cross a link faster than the smallest packet's serialization plus propagation delay. The validator certifies that bound for every channel before the run starts. Each round, Days computes a safe horizon:
No event a process has not yet seen can arrive before H. A round then takes three steps:
Safe horizon
H equals the minimum of S and the minimum over i of N sub i plus LH = min(S, miniNi + L)
Nᵢ is process i's earliest pending event, L is the smallest certified channel bound, and S is the stop time.
01
Drain. Every process executes its events below H in key order, in parallel. Messages for other processes go to a private outbox.
02
Exchange. One deterministic exchange delivers every outbox, merged in key order.
03
Advance. The next horizon is computed from what is now pending.
Fixed 1,000 ns slots vs adaptive safe horizon · L = 1,000 ns · time in ns
slot 13 of 13 · [12,000, 13,000) ns · 1 event
round 8 of 8 · H = min(13,000, 12,000 + 1,000) = 13,000 ns · advance 5,996 ns
Top: fixed slots run every stage on every slot, busy or idle, and an ACK waits for the next boundary. Bottom: each adaptive round ends where lookahead says it must, and an idle stretch is one round.
The contrast with a fixed slot. GeDES advances simulated time in fixed 1,000 ns slots. An acknowledgment that arrives 4 ns into a slot cannot influence anything until the next slot boundary. Days, instead, ends the round 4 ns in and honors the causal chain exactly. The cost is visible as more rounds, and the result is unchanged. When the network is idle, the horizon crosses the dead time in a single round, while a slot pipeline runs its full kernel sequence on every slot.
In short, a slot engine pays for each slot of simulated time, and Days pays for each round and each event of actual work.
What each engine pays for · runtime vs span, and horizon advance per round
Days (CUDA)
GeDES
F-HET (tiered delays)
F-BURST (bursty coflows)
Left: what each engine pays for simulated time on the TCP experiment. GeDES's runtime grows in proportion to span, from 0.565 s at its active frontier to 2,252.5 s at full completion. Days levels off at 0.575 s once the fabric is idle. Right: how far each round advances. In the tiered-delay scenario, 229 rounds cover 893 slots' worth of time. In the bursty scenario, the 462 idle slots between bursts cost three rounds.› Data table
Series
Framing
Simulated span (ms)
Runtime (s)
Days CUDA
active
0.640628
0.56314
Days CUDA
full configured horizon
3,000
0.574902
GeDES
active
1.082
0.565158
GeDES
full configured horizon
3,000
2,252.5
03Proved
The parallelism is licensed by proof.
The theorems are about a model of the executor defined in Lean: a transition system whose moves are the executor's moves. Every definition in the model is annotated with the executor source location it formalizes. Together, the five theorems say that every execution the parallel machinery may perform ends in the same complete state as canonical serial execution.
17,247
lines of Lean
1,179
declarations across 31 modules, checked by an audit driver
3
standard axioms, and nothing more: no placeholders, no native_decide
01
Remote lower bound. The horizon rule the executor ships is safe: no unseen event can arrive below it.
02
Round serializability. Running one round in parallel gives exactly the state that running its events one at a time, in canonical order, would give.
03
Run composition. A whole run of such rounds ends in the serial result at the stop time. It does not prove that the run terminates.
04
Decision-point scope. The one rule queue disciplines must follow: choose a packet only when service actually starts, and never change, drop, or duplicate a packet in service. Four executable countermodels show that each clause is necessary.
05
Intra-round reordering license. Within a round, events need to keep their order only on the same packet's causal chain or at the same process's queues. Any other order gives the same result, and this is the freedom a GPU needs.
From the model to the backends
A proof is about the model, not about a compiled binary. Testing closes that gap, and a backend passes only when its bytes match. The CPU pool and every device backend must reproduce the serial oracle's complete state in four-backend agreement tests. The GPU kernels must report no races under the vendor's race detector on both kinds of GPU. Byte-identity is a precondition of every timed configuration we report, so nothing is timed unless its state matches. LeanGuard adds a second check on the mechanisms: a Scalar run under full observation writes exact-integer transition certificates, and Lean checkers replay each record against an executable reference in CI.
04Programming model
Write a process once. Run it on a GPU.
In Days, every network element, whether a host or a switch egress port, is an isolated sequential process. It holds private state, reacts to timestamped messages, and affects other processes only by sending messages. It is a loop that receives, updates, and sends. It is not a set of callbacks against a global event queue.
Private state. No two processes share mutable state, so the CPU pool needs no locks.
Messages only. Processes interact only through the round's exchange, whose merge order is fixed by the canonical key.
Written once. Protocol logic is defined once, by the serial oracle, against a fixed vocabulary of seven mechanisms. The Metal and CUDA kernels are ported from it in the same per-element form. The reordering theorem, not the protocol author, absorbs what the hardware demands.
GeDES gets uniform GPU work by organizing execution around protocol stages: one kernel per stage, every slot. As a result, a protocol's logic is spread across those kernels, and adding a protocol means editing the whole pipeline.
The process model dates to Conway's coroutines and SIMULA's processes, more than six decades ago. Days carries it onto GPUs.
Byte-identity makes this checkable. Every new protocol, backend port, and measurement campaign in the paper was produced by coding agents and accepted only when the bytes matched.
05Evaluation
Measured against ns-3, Unison, legacy Days, and GeDES.
Three machines: an Apple M5 Max, an i7-13700K with an RTX 4090, and an NVIDIA DGX Spark (GB10). Every cross-simulator ratio was measured on the i7-13700K + RTX 4090 machine. Each sample records two clocks: the native clock (the simulation itself) and the process wall (end to end, including compilation, upload, and readback). Results from the paper, which is under review.
(a)TCP
TCP: even where slots are strongest, far ahead at the finish
FatTree-32, 8,192 closed-loop TCP Reno flows of 1 MiB each, run until every flow finishes, losses and retransmissions included. We report two framings of the same runs. The active frontier ends at the last data-bearing instant. Full completion ends when the last flow finishes.
Densest phase, vs GeDES: 0.563 s vs 0.565 s on the native clock, statistically even (a 0.4% median edge, inside GeDES's own run-to-run spread). On the process wall, Days is 1.9× faster (2.75 s vs 5.19 s).
Full completion, vs GeDES: 3,918× on native clocks and 821× on the process wall. GeDES spends 2,252 s stepping slots through a stretch of simulated time that includes a retransmission after a full 1-second timeout. The adaptive horizon crosses it in milliseconds.
CPU pool (22 workers), full-completion native clocks: 82.6× faster than sequential ns-3, 15.4× than ns-3 MPI at 8 ranks, and 9.0× than Unison at 24 threads. The CUDA backend is a further 8.7× faster.
One thread against one: the serial oracle is 3.3× faster than sequential ns-3.
The one loss: legacy Days at 24 workers beats the serial oracle on the native clock (0.84×), and loses on the wall clock.
Unison does not reproduce sequential ns-3's trajectory, even single-threaded, so its times measure speed on a divergent computation.
TCP experiment · native clock, seconds (log)
Active frontier
Full completion
Days
GeDES
Other
Native-clock seconds for every configuration, log scale. Days (CUDA) and GeDES are even at the active frontier; run through completion, they separate by 3,918×. Legacy Days and ns-3 MPI have no supported active-frontier clock, so they show full completion only.› Data table
Configuration
Active (s)
Full (s)
Clock
Days, Scalar (serial oracle)
125.355489
126.224843
run_ns
Days, CPU (22 workers)
5.002304
5.006736
backend_ns
Days, CUDA (RTX 4090)
0.56314
0.574902
device_ns
Legacy Days, 1 thread
n/a
356.836233
Nexosim total
Legacy Days, 24 workers
n/a
106.110999
Nexosim total
GeDES (ported)
0.565158
2,252.5
Simulation Duration
ns-3, sequential
413.260065
413.40148
E5_CLOCK runS
ns-3 MPI, 8 ranks
n/a
77.001764
rank-0 E5_CLOCK runS
Unison, 24 threads
43.139538
44.89506
E5_CLOCK runS
Unison, 1 thread
401.564964
404.575131
E5_CLOCK runS
(b)UDP
UDP: where the curves cross
Same FatTree-32 fabric, constant-bit-rate traffic at 1%, 10%, 30%, and 60% offered load, 5,000 ns propagation, 60–126 million packets per load. GeDES executes 90,000 down to 2,000 slots as the simulated span shrinks. Days executes 17,046 down to 391 rounds, a count set by the traffic and identical on every backend.
On the RTX 4090's native clocks, Days (CUDA) is 6.1× faster at 1% load and 1.45× faster at 10%. At 30% and 60%, where the slots are full, GeDES leads, by 1.06× and 1.07×. On the process wall, Days is faster at every load on this machine, from 6.3× at 1% down to 1.2× at 60%.
On the DGX Spark's GB10, the crossover moves earlier. Days is 4.1× faster at 1%. GeDES leads on the native clock at 10%, 30%, and 60%, by 1.04×, 1.61×, and 1.89×. On the process wall, Days is faster at the first three loads and 6% slower at 60%.
Against the CPU simulators, the gaps are wider. Days (CUDA) runs 467–1,279× ahead of sequential ns-3 and 47–81× ahead of Unison at 24 threads, on native clocks on the RTX 4090 host.
Fixed slots pay for simulated time and events pay for work. On native clocks (left), the curves cross between 10% and 30% load, and GeDES leads at 30% and 60%. On the end-to-end process wall (right), Days (CUDA) is faster at every load on the RTX 4090 host.› Data table
Panel
Load
Series
Seconds
Clock
Native
1%
Days CUDA
3.039444
cuda_device_ns
Native
10%
Days CUDA
3.476381
cuda_device_ns
Native
30%
Days CUDA
1.936836
cuda_device_ns
Native
60%
Days CUDA
1.414949
cuda_device_ns
Native
1%
Days CPU
43.216664
executor_backend_ns
Native
10%
Days CPU
42.532565
executor_backend_ns
Native
30%
Days CPU
27.189576
executor_backend_ns
Native
60%
Days CPU
21.573915
executor_backend_ns
Native
1%
GeDES
18.4784
gedes_simulation_duration_ns
Native
10%
GeDES
5.04364
gedes_simulation_duration_ns
Native
30%
GeDES
1.8306
gedes_simulation_duration_ns
Native
60%
GeDES
1.31632
gedes_simulation_duration_ns
Process wall
1%
Days CUDA
3.88
GNU time -p real
Process wall
10%
Days CUDA
4.82
GNU time -p real
Process wall
30%
Days CUDA
4.43
GNU time -p real
Process wall
60%
Days CUDA
5.95
GNU time -p real
Process wall
1%
Days CPU
44.25
GNU time -p real
Process wall
10%
Days CPU
43.68
GNU time -p real
Process wall
30%
Days CPU
29.32
GNU time -p real
Process wall
60%
Days CPU
25.73
GNU time -p real
Process wall
1%
GeDES
24.45
wrapper-monotonic process_elapsed_ns
Process wall
10%
GeDES
11
wrapper-monotonic process_elapsed_ns
Process wall
30%
GeDES
7.78
wrapper-monotonic process_elapsed_ns
Process wall
60%
GeDES
7.26
wrapper-monotonic process_elapsed_ns
Native clock, seconds, RTX 4090 host
Load
1%
10%
30%
60%
Days (CUDA)
3.039
3.476
1.937
1.415
GeDES
18.48
5.044
1.831
1.316
Faster
Days 6.1×
Days 1.45×
GeDES 1.06×
GeDES 1.07×
Days rounds / GeDES slots
17,046 / 90,000
3,707 / 19,000
781 / 4,000
391 / 2,000
(c)Propagation
More lookahead, fewer rounds
The horizon is set by link delay, so Days should gain as propagation grows, and it does. At 1% load, sweeping propagation through 1, 2.5, 5, and 10 µs moves the native-clock ratio from 3.06× through 4.12× and 6.07× to 8.72× in Days' favor. Days' rounds fall from 51,138 to 8,767. GeDES keeps its 1,000 ns slot and runs the same 90,000 slots at every point, flat at about 18.5 s.
Propagation sensitivity at 1% load, RTX 4090 native clocks. The GeDES-to-Days ratio grows with lookahead because Days' round count falls (annotated), while GeDES executes 90,000 slots at every point.› Data table
Propagation (µs)
Days CUDA (s)
GeDES (s)
Ratio
Days rounds
GeDES slots
1
6.040599
18.4752
3.058505
51,138
90,000
2.5
4.482034
18.4811
4.123373
29,222
90,000
5
3.045635
18.4867
6.0699
17,046
90,000
10
2.122161
18.5145
8.724361
8,767
90,000
(d)Width
A GPU needs width
Width is the number of processes with pending work in a round. At 918 active processes, no GPU wins a single paired sample: the round offers too little parallelism to pay for the dispatch. Near 10,000, the CUDA devices take the lead. Metal never beats its own M5 Max CPU at any width we tested. It comes within 4.4% and stays behind.
Device over own host's CPU pool · per-round speedup (log)
RTX 4090 (vs i7, 24 workers)
GB10 (vs Grace, 20 workers)
Metal (vs M5 Max, 16 workers)
262,144 flows
Each GPU against its own host's CPU pool, per-round native clocks. The CUDA devices cross parity near 10⁴ active processes, and Metal stays below parity at every width. The open symbols mark the 262,144-flow run, measured on device clocks in a separate session.› Data table
x
x basis
Device
Speedup
Point
918
mean active LPs
Metal
0.193
curve
918
mean active LPs
RTX 4090
0.846
curve
918
mean active LPs
GB10
0.676
curve
10,132
mean active LPs
Metal
0.956
curve
10,132
mean active LPs
RTX 4090
3.21
curve
10,132
mean active LPs
GB10
1.372
curve
23,739
mean active LPs
Metal
0.955
curve
23,739
mean active LPs
RTX 4090
2.79
curve
23,739
mean active LPs
GB10
1.206
curve
262,144
flow count
RTX 4090
13.11
frontier
262,144
flow count
GB10
6.12
frontier
Each device over its own host's CPU pool, same experiment; above 1.00 favors the device
Mean active processes
Metal (vs M5 Max, 16 workers)
RTX 4090 (vs i7, 24 workers)
GB10 (vs Grace, 20 workers)
918, closed-loop TCP
0.193
0.846
0.676
10,132, sustained
0.956
3.21
1.37
23,739, FatTree-48 sustained
0.955
2.79
1.21
(e)Largest run
262,144 flows, one state
Our largest experiment runs 262,144 closed-loop TCP Reno flows on FatTree-32: 1,151 rounds and 675 million transitions. It ends in one 2,274,074,943-byte state that is identical on both hosts and both GPUs.
On the GPU clock alone, the RTX 4090 is 13.1× faster than its own 24-worker CPU, and the GB10 is 6.1× faster than its Grace host. End to end, a first run gains only 1.92× and 1.11×, because host-side memory planning and readback dominate. The memory plan a run settles on is deterministic, so a later run can reuse it. That raises the end-to-end gain to 3.21× and 2.11×, with no change to the GPU time or the result.
(f)Cost model
Two constants predict the winner
time = A · rounds + B · transitions
A run costs a fixed amount per round plus a fixed amount per event executed: time = A · rounds + B · transitions. Fit per machine from its UDP runs, the model reproduces all fourteen measured runs with a median error of 0.4% (worst 9.6%). On the RTX 4090, A = 0.093 ms per round and B = 1.28 ns per event. The same form fits GeDES, at about 172 µs per slot plus 16 ns per packet, against about 27 ns per packet for Days. That is why the curves cross: GeDES does less work per packet, but it pays for every slot, whether or not any packet is in flight.
06Backends
Four backends, one image.
A scenario compiles once into an immutable image. The validator admits the image before anything runs. Any backend then executes it to the same byte-identical state. A backend that can't run a scenario faithfully refuses it up front, and so does the compiler: every Days AGO table refuses an unknown key, naming the key and the table it sits in.
Backends, where they run, and their role
Backend
Where it runs
Role
Scalar
One CPU thread
The reference oracle. It defines the semantics, and every other backend is checked against its bytes.
CPU
A multicore worker pool
Safe-horizon rounds across workers with no shared mutable state and no locks. It is byte-identical at every width.
Metal
Apple GPUs (not the M1 family)
The round loop runs on the device in waves, with a per-element design licensed by the reordering theorem.
CUDA
NVIDIA GPUs (built for sm_86, sm_89, and sm_121)
The kernels of a round form a fixed sequence that is captured as a CUDA Graph and replayed in bounded waves. Tested on a discrete RTX 4090, a discrete RTX A4500, and a unified-memory GB10.
What it models
Topologies: fat-tree, torus, dragonfly, custom graphs, and the Spectrum-X rail-optimized fabric of SimAI, with NVLink inside a server as a delay only, sized by how many messages share the sender's port, and SimAI's Murmur3 ECMP.
Transport: deterministic packet-distribution sources, closed-loop TCP Reno and CUBIC, Mellanox-form DCQCN with CNP on unreliable flows, and RoCE queue pairs with Go-back-N reliability and ECN echo.
Switches: FIFO, strict-priority, DRR, WRR, and exact-rational WFQ scheduling; tail-drop admission and ECN marking on a Kmin/Kmax/Pmax ramp in bytes, decided at enqueue by a deterministic draw; PFC on switch links and host links.
Collectives: ring all-reduce, all-gather, reduce-scatter, all-to-all (uniform, or seeded and imbalanced), and send/receive over TCP or RoCE queue pairs, with several ring channels, delay-only compute stages, and counted joins between them.
Workloads: AICB/SimAI training traces from a [workload.aicb] table, lowered onto the Spectrum-X fabric, with the MTU, switch buffer, ECN ramp, PFC thresholds, and DCQCN parameters taken from SimAI.conf and the link rates and delays from the [topology.spectrum_x] table: SimAI's dense GPT-13B b4 baseline on 128 GPUs, a Qwen3-30B-A3B-like MoE (TP2, EP32) smoke trace on 128 GPUs, and the 1,024-GPU flagship trace. The Workloads page states how Days AGO's iteration time compares with SimAI's on the b4 baseline and the MoE smoke trace.
07Quick start
Run one scenario on every backend.
From the repository root. Every run uses the same small TCP smoke fixture.
01Scalar reference run
cargo run --release --bin days -- \
configs/benchmarks/tcp/fattree_k4_tcp_cubic_f16_smoke.toml --engine scalar
02Multicore CPU run
cargo run --release --bin days -- \
configs/benchmarks/tcp/fattree_k4_tcp_cubic_f16_smoke.toml \
--engine cpu --workers 2 --repetitions 1
03GPU run on Apple Metal
cargo run --release --features metal --bin days -- \
configs/benchmarks/tcp/fattree_k4_tcp_cubic_f16_smoke.toml --engine metal
04GPU run on NVIDIA
cargo run --release --features cuda --bin days -- \
configs/benchmarks/tcp/fattree_k4_tcp_cubic_f16_smoke.toml --engine cuda
Every engine ends with a record=days_result line that carries the complete state's byte length and its FNV-1a fingerprint. If two runs have equal fingerprints, their results are byte-identical.
--engine metal and --engine cuda need their Cargo feature, and asking for either without it is an error. CUDA builds need a CUDA 13 toolkit. Install guide →
08Lineage
Legacy Days
Days began as an actor-model simulator on Nexosim coroutines, published at IEEE INFOCOM 2026. Its network elements were already processes with private state that communicate by messages. The new executor keeps that model and replaces the engine underneath it.
Legacy Days (up to version 0.4.3) is frozen in legacy/ as the days-legacy crate. It receives no new features, but CI still builds, tests, and runs it:
cargo run --release -p days-legacy --bin days-legacy -- configs/simple.toml
TCP experiment: the new CPU pool is 71.3× faster than legacy Days single-threaded and 21.2× faster than its 24-worker mode, on native clocks.
Per event: on UDP, the serial oracle spends about 360 ns per event, against about 1.3 µs for legacy Days single-threaded on the same work. That puts legacy Days 3.1–3.6× behind at the same machine and clock.
Determinism: legacy Days' multi-threaded mode returns different packet counts from run to run, so its clocks are reported but its counts are not.
09FAQ
Questions researchers ask
Is Days faster than GeDES?
It depends on the workload, and we report both sides. On TCP run to completion, Days (CUDA) is 3,918× faster on native clocks, because GeDES steps through every slot of idle simulated time. In the densest TCP phase, the two are statistically even. On UDP at 30% and 60% load, GeDES is 1.06× and 1.07× faster on the RTX 4090's native clock. On the GB10, GeDES leads at 10% through 60%. On the process wall, Days is faster at every load on the RTX 4090 host.
Which backend should I use?
Use Scalar to debug and as the reference. Use CPU for everything else. Use CUDA when rounds are wide: in our measurements the NVIDIA GPUs overtake their host CPUs near 10,000 active processes. Metal gives the same answer, but at no width we tested did it beat its own M5 Max CPU. Because every backend returns the same bytes, choosing one is purely a question of speed, and the cost model estimates it.
What does byte-identical buy me?
A bug seen on one backend reproduces at the same instant on every backend. A regression either changes the state or it doesn't, so no statistical judgment call is involved. CI can pin the complete final state of every scenario. And you can measure another simulator's approximation against an exact reference at the same scale.
Can I run DCQCN on a GPU?
Yes. Mellanox-form DCQCN, RoCE queue pairs with Go-back-N, PFC on switch links and host links, and the ECN ramp run on Metal and CUDA, and so do collectives, compute stages, and stage notifies. Every device run returns the same bytes as Scalar. An image that holds any of those mechanisms runs the mechanisms build of the round kernel, reported as round_kernel=mechanisms in the record=days_device line; an image with none of them, such as a plain TCP scenario, keeps the plain build. Metal and CUDA return no diagnostic planes, so collective traces come from Scalar or CPU runs and LeanGuard certificates from Scalar runs. What a backend cannot run is refused at validation with a message naming the backend. There is never a silent fallback.
Can I run an AICB or SimAI training trace?
Yes. A [workload.aicb] table makes an AICB trace the scenario's traffic on the Spectrum-X fabric. Days AGO parses the trace, forms SimAI's communicator groups, plans each rank's schedule as SimAI's workload loop runs it, and derives the MTU, the switch buffer, the ECN ramp per link rate, the PFC thresholds and headroom, and the DCQCN controller and window from SimAI.conf. The GPU count, link rates, and delays come from the scenario's [topology.spectrum_x] table, which must equal a pinned SimAI topology file; the few transport settings SimAI keeps out of the file (the ACK size, NACK-only recovery, the data priority, SimAI's ECMP) are fixed by the adapter. Two fidelities are available: simai, SimAI as it runs, with pipeline parallelism forced to 1 and SimAI's own groups, and megatron, with per-stage groups and pipeline send/receive. Expert routing is uniform or seeded imbalanced. The committed scenarios cover SimAI's dense GPT-13B b4 baseline on 128 GPUs and a Qwen3-30B-A3B-like MoE smoke trace (TP2, EP32); the 1,024-GPU flagship scenario names a trace that is not committed. Four reduced traces run to completion on Scalar, and CPU, Metal, and CUDA must equal them; b4 and the smoke trace are lowered in full and run to a cutoff past their first cross-host collectives, which every backend must match to that cutoff. The Workloads page gives Days AGO's and SimAI's iteration times on the b4 baseline and the MoE smoke trace, with the attribution of the difference, and the nine recorded divergences from SimAI that every run prints.
What does LeanGuard certify?
LeanGuard is the certificate side of the verification tree. A Scalar run under full observation writes exact-integer transition records for TCP Reno and CUBIC, the ECN ramp, Mellanox-form DCQCN, RoCE queue pairs with host-link PFC, switch-link PFC, WFQ, strict priority, DRR, WRR, rate sources, collectives and stage joins, send/receive, and all-to-all, and a Lean checker replays each record against an executable reference. CI builds the checkers, audits the DaysExecutor axioms, and runs every checker on committed accept fixtures and on mutations each must reject. Many of the accept fixtures are regenerated by Rust tests that fail on any difference; for the TCP, switch-link PFC, scheduler, WFQ, and AQM fixtures that tests/leanguard_certificates.rs writes, a two-worker CPU run must also write the same bytes. The coverage matrix lists what each checker certifies and its recorded limits. FIFO scheduling and constant traffic have no checker, and every certificate comes from a Scalar run, because device runs return no diagnostic planes.
Are the proofs about the code I run?
They are about a Lean model of the executor, in which each definition is annotated with the executor source location it formalizes. The link from model to binary is conformance testing: every backend must reproduce the serial oracle's complete state byte for byte, and nothing is timed unless it does.
What happened to the old Days?
It is frozen in legacy/ as days-legacy and still runs. Its paper is here. The new executor keeps its process model and is 21–71× faster on the TCP experiment.