How we continuously validate formal specifications in production
Comments on “How we continuously validate formal specifications in production”
Claim-checked. Scored by all three judges, and its checkable claims were compared with the sources it cites. How far stories are checked
Datadog's engineering blog describes FETCh, a tool that turns TLA+ specifications into Rust runtime monitors fed by production telemetry, so drift between a formal model and the running system gets detected. Applied to Husky's routing, it found no violations in the router, but flagged conflicting placements that had been stored for about a year and could crash backfill recovery. Datadog reports roughly 2% CPU overhead in sidecars. These figures are self-reported, and the tool supports only a subset of TLA+.
Why it ranked
No. 15 of 109 with a score of 0.66. The panel rated it highest on new information (0.94) and technical depth (0.90), lowest on audience breadth (0.54). Placed No. 15, No. 27 by score alone: the placement terms moved other stories past it.
- AI judgeJudge 2claude-haiku-5-5
- Detailed engineering write-up of runtime-monitoring TLA+ specs in production, with a concrete bug found; substantive but niche in audience reach, with an unverifiable self-reported result.
- AI judgeJudge 3gpt-5.6-luna
- A detailed, evidence-backed engineering account of converting TLA+ specifications into production runtime monitors, including architecture, scaling tradeoffs, concrete code, overhead measurements, and a real bug discovered. Broadly useful, though specialized and company-specific.
Each judge wrote its line after answering the rubric, with the site and the author still hidden. Every answer behind this is in the table under Score.
Score
0.66total under rubric v2.3
- Significance0.60
- Reader interest0.82
- Audience breadth0.54
- Practical relevance0.66
- Substantiated0.81
- Technical depth0.90
- New information0.94
- Counts against: Promotional0.11
- Counts against: Overclaim0.17
Each judge’s answer per question (0–1), their mean and spread, and what the question adds to the score (weight × mean).
| Question | Judge 1 | Judge 2 | Judge 3 | Mean | Spread | Weight | Contribution (weight times mean) |
|---|---|---|---|---|---|---|---|
| SignificanceHow much does this change what people in tech know or can do? | 0.55 | 0.45 | 0.79 | 0.60 | 0.34 | +0.24 | +0.143 |
| Reader interestWould a well-informed senior engineer or tech founder want to read this today, and likely pass it on? | 0.73 | 0.80 | 0.93 | 0.82 | 0.20 | +0.26 | +0.213 |
| Audience breadthHow many people who build technology does it concern? | 0.56 | 0.40 | 0.66 | 0.54 | 0.26 | +0.13 | +0.070 |
| Practical relevanceHow useful is it to someone who builds software or tech products? | 0.67 | 0.50 | 0.82 | 0.66 | 0.32 | +0.22 | +0.146 |
| SubstantiatedHow well is it backed? Consider whether it is the primary source, and whether its main claims come with data, code, a demo, a reproducible method or citations. | 0.82 | 0.70 | 0.91 | 0.81 | 0.21 | +0.05 | +0.041 |
| Technical depthHow technically substantive is it? | 0.95 | 0.80 | 0.94 | 0.90 | 0.15 | +0.05 | +0.045 |
| New informationDoes it contain information absent from the stories covered in the last 7 days (list provided)? | 0.89 | 0.95 | 0.97 | 0.94 | 0.08 | +0.05 | +0.047 |
| PromotionalIs it mainly marketing with little substance (a press release, ad or sponsored post with no real information)? A launch post that carries real news is not promotional. | 0.07 | 0.20 | 0.06 | 0.11 | 0.14 | −0.19 | −0.021 |
| OverclaimDo the headline or conclusions claim more than the body supports? | 0.20 | 0.20 | 0.10 | 0.17 | 0.10 | −0.11 | −0.018 |
| Sum of contributions | +0.665 | ||||||
| Claim-check penalty | 0.000 | ||||||
| Total, as published | 0.665 | ||||||
Spread is the highest minus the lowest judge answer. marks a spread above 0.40: the judges disagree, and the story is marked contested.
The badge for this ranking, for the author's page or anyone's: one line of HTML, and it links back here.
<a href="https://rubric.hrih.si/editions/2026-11-06/15/"><img src="https://rubric.hrih.si/badge/2026-11-06/15.svg" alt="Ranked #15 on Rubric, 6 Nov 2026" width="238" height="28"></a>Claim check
Claim check: 1 matches source · 7 no source given. Each claim is compared with the source the article itself cites; a flag is published only when both checkers agree.
No source givenDate
A change to Husky's placement logic allowed conflicting placements to persist in production for about a year.
The article gives no link or citation for it.
The article says “a change to its placement logic allowed conflicting placements to persist in production for about a year”
The source says No source to compare with.
No source givenNumber
In the sidecar running alongside the routing service, FETCh's p90 overhead was about 2% CPU and less than 0.2% memory across thousands of pods processing tens of millions of events per second.
The article gives no link or citation for it.
The article says “we measured p90 overhead of about 2% CPU and less than 0.2% memory across thousands of pods processing tens of millions of events per second”
The source says No source to compare with.
No source givenNumber
Batch validation of placement overlap processed several days of data containing several million placements in around an hour using 1 CPU and a few gigabytes of memory.
The article gives no link or citation for it.
The article says “Batch validation of placement overlap processed several days of data containing several million placements in around an hour by using 1 CPU and a few gigabytes of memory”
The source says No source to compare with.
No source givenNumber
Datadog estimates that fewer than 0.01% of placements conflict.
The article gives no link or citation for it.
The article says “We estimate that fewer than 0.01% of placements conflict”
The source says No source to compare with.
No source givenNumber
The routing service conformed to Router.tla, with no violations detected in the monitored traffic, while the PlacementStorage.tla monitor detected conflicting placements stored in the database.
The article gives no link or citation for it.
The article says “The routing service conformed to Router.tla: We detected no violations in the monitored traffic”
The source says No source to compare with.
No source givenCausal conclusion
Two conflicting placements are enough to crash Husky's backfill system, which does not tolerate placement conflicts when recovering from placement data loss.
The article gives no link or citation for it.
The article says “Even at that rate, two conflicting placements are enough to cause our backfill system to crash”
The source says No source to compare with.
No source givenCausal conclusion
The conflicting placements came from special cases added a year earlier that intentionally skipped deduplication to improve balancing, but were still persisted.
The article gives no link or citation for it.
The article says “A year earlier, we had added special cases in which we intentionally skipped deduplication and allowed conflicting placements to improve balancing”
The source says No source to compare with.
Matches sourceQuote
TLA+ was developed by Leslie Lamport and supports model checking and machine-checked mathematical proofs.
The cited source says the same thing.
The article says “TLA+, a formal specification language developed by Leslie Lamport, supports model checking and machine-checked mathematical proofs”
The source says “TLA+ is a formal specification language developed by Leslie Lamport”
Source cited by the article: en.wikipedia.org/wiki/TLA%2B
Also covered by
No other coverage was clustered with this story.
Elsewhere
Elsewhere: HN —
Recorded for context only, checked 6 Nov 2026, 05:47 UTC. It played no part in the ranking.