/sesh/null

The first thing I did at @tryramp was set up distributed tracing, structured logging, and metrics for Inspect, our background coding agent. We now have full visibility in to everything the system is doing: the browser, CF workers/DOs, @modal sandboxes, database calls, etc. Most importantly, Inspect now has visibility in to itself. It can self-triage runtime errors it encounters and create PRs to fix them. Every morning, it reviews the past 24 hours of its own @datadoghq dashboard, identifies systemic issues, new errors, and long tail latencies, and has a summary + PR waiting for me at 9am.

Really enjoyed this conversation with @swyx. Hope you enjoy the podcast.

Our self-improving system leverages Shinka Evolve from @SakanaAILabs underneath. “On a second workload—100 different group-by tag combinations on the same metric—the improvement reached 541% over the baseline. The pattern mirrors ShinkaEvolve’s dynamics: Most generations explore incrementally, but occasional mutations discover qualitatively different algorithms” x.com/nerdsane/statu…

@datadoghq as MCP app in your cursor. Amazing work from @hydrosquall and team. More to come

If you want LLMs to show charts/#dataviz of live data instead of text alone, now they can via the @datadoghq x @cursor_ai MCP app!

Datadog has been working on the verifiability of agentic coding loop with observability driven harnesses. They are working on BitsEvolve, inspired from Google Deepmind's AlphaEvolve, an evolutionary algorithm that mutates the code, evaluate each variant against a benchmark and iterate. Here are some interesting blog posts that describe their approach and progress .. 1. Closing the verification loop: Observability-driven harnesses for building with agents (datadoghq.com/blog/ai/harnes…) 2. From hand-tuned Go to self-optimizing code: Building BitsEvolve (datadoghq.com/blog/engineeri…) 3. Closing the verification loop, Part 2: Fully autonomous optimization (datadoghq.com/blog/ai/fully-…)

2️⃣ Closing the verification loop, Part 2: Fully autonomous optimization datadoghq.com/blog/ai/fully-…

We had AI agents build Functional equivalents of Redis and Kafka from scratch in a few days with formal verification, deterministic simulation testing, and TLA+ specs. Then we let them optimize a live production service. Autonomously! What we're seeing looks like the early industrialization of software engineering. And at its core: observability is becoming the control layer for agent-produced software. In late 2025, while working on BitsEvolve—our LLM-backed evolutionary optimizer— we (like many around reported) suddenly started to notice a step-function improvement in model capabilities and saw an opportunity to raise our ambition levels. We wanted to see exactly how far we could push agent-driven systems engineering to whole distributed systems. So we built a functional equivalent of Redis and Kafka with different design decisions and trade-offs and shadow tested them with our workloads. We are humbled to report from a first hand account that the capabilities have reached a state that is now possible to transition toward self-evolving architectures that continuously measure, adapt, and optimize themselves. At the core of this shift, observability is emerging as the explicit feedback control mechanism for agent-produced software. We have documented our methodology and the resulting codebases (redis-rust & Helix) in a two-part technical series, detailing how we could safely empower AI agents to build, test, and optimize complex distributed systems. Part 1: We utilize "harness-first engineering" to build complex infrastructure. By defining strict system invariants upfront and building rigorous automated harnesses—using deterministic simulation testing, formal specifications (TLA+), and observability-driven feedback loops—we enable AI agents to autonomously iterate against these constraints. Part 2: We then extended this verification framework directly into active environments. Using BitsEvolve, we implemented fully autonomous optimization for our time-series aggregation service. The system actively proposes algorithmic improvements, formally verifies safety properties, shadow-evaluates against live traffic, and hot-swaps improved WebAssembly modules. By enabling the LLM to discover and deploy structural algorithmic changes (such as shifting from O(N) iterations to O(1) lookups), we achieved performance improvements of up to 5x on targeted workloads. People involved in no particular order - @atalwalkar @Keleesssss Arun Parthiban Jai Menon Ming Chen Vyom Shah. If you are curious and want to compare notes on how we can raise the bar by pushing the rigor in agent built software, please give a read and hit us up with your thoughts. Links in comments

1️⃣ Closing the verification loop: Observability-driven harnesses for building with agents datadoghq.com/blog/ai/harnes…

@GeoffreyHuntley @yenkel Here’s an example of you want to play with - github.com/nerdsane/redis…

In Loom, yeah: TLA+ and model checkers. In Latent Patterns, just QuickCheck is good enough for now. I need to do some more engineering to perform mutation testing and get into the realm of DST. But at this stage, all the engineering foundations are in place, that make it sound enough to launch. So I'm moving on to other aspects of the business now, like sales automation, marketing, and all that.

Lots more things Are Database than you think - Git - Datadog: 800 db's in a UI trenchcoat - Temporal: basically Stored Procedures - Notion: vaguely remember @sliminality's "database monetizing as a productivity app" quote - Honeycomb: @mipsytipsy spent 2 years Building Database

Big

Kept — a sci-fi world set in 2043 - a black mirrorish application of mechanistic interpretability towards a concept called continuations. deep-sci-fi.world/world/3f2e61e8… #DeepSciFi

@smehmood They are very creative -

Guess we’re all calling them “claws” from now on

💯 agree on these takeaways (specifically this) “AI, used right, should produce better software, provided humans actually spend more energy on architecture, design, and innovation.”

I'm optimistic that formal verification is the solution to our current situation where LLMs are writing our code and nobody's reading it. Formal methods can give us a world where we write succinct specs and agent-generated code is proven to comply. But we have a long way to go. There are several open challenges that stand between our situation today and that future, but none appear insurmountable. I’ve written a brief overview of what I consider to be the big open problems, and some of the directions that researchers are taking today to address them: from verifying mathematics to building standard libraries of verified code that can be built upon. Here are a few highlights: 1) A Brief History of Formal Verification Verification is fundamentally about understanding what your program can or can’t do, and verifying it with a proof. In order to verify, you must first have a specification that you are verifying your program against. Most of you leverage some formal verification day to day: namely, some of the compiler errors in statically-typed languages like C++ and Java are verification errors. Static type checking is the version of formal verification programmers are most familiar with. Type systems (and related formal verification tools) have gotten quite impressive, and they are becoming a lot more relevant in constraining the behavior of AI coding models. 2) Rust Type checking represents a middle ground for verification. The hard part is choosing the right balance: reject too many good programs and it becomes hard to program in this language as the programmer has to “guess what the type checker will permit”. Recently the language that has brought the most interesting advances from type systems to the real world is Rust. Its ownership type language and associated type checker is known as the “borrow checker”. The borrow checker is conservative, and “fighting with the borrow checker” is part and parcel of everyone’s Rust experience. This gives us the following lesson: we can prove more interesting things, but at a larger burden to the developer. Finding elegant middle points is hard, and Rust represents a real design breakthrough in navigating that tradeoff. 3) Mechanically verified math Recently, groups of mathematical researchers have recently been writing mathematical proofs in a specialized programming language called a proof assistant. This language, LEAN, comes with a powerful type checker capable of certifying complex mathematical proofs. LEAN is exciting, but working in LEAN can be frustrating - because of the nontermination properties of the type checker’s search, such languages rely heavily on programmer annotation. And this is why more complex type systems have stayed relatively academic: the Rust borrow checker sits at a genuinely elegant point in the design space: complex enough to reason about a complex property like memory references, yet simple enough to not need too much extra annotation. But this is a critically important point: Mathematical proofs and type checking aren’t just analogous: they are the literal same task. They are different only in the degree of complexity along two axes: the complexity of the underlying objects, and the complexity of the properties we are proving. 4) There is still a long way to go for proof assistants While the world I describe is exciting, bluntly, we’re not anywhere close to that world yet. Proofs break easily when programs are modified, the standard library of proofs is too small, and specifications seldom capture everything about the program’s behavior. Overall there’s a long way to go before these techniques reach a mainstream programming language with broad adoption. But, AI is a huge accelerant to proof assistants. Much of the energy towards AI-assisted mathematics is coming from AI researchers who see it as a very promising domain for building better reasoning models. Verified math is a domain rich in endless lemmas, statements, and proofs, all of which can be used as “ground truth” - which means we can use them as strong reward signals in our post-training workflows. There are several startups being built by seasoned foundation model researchers - Harmonic, Math Inc - that are based on this premise. I’m no expert here, but it sure seems to me that formally verified code would lead to a clear domain of tasks that have strong verifiable rewards ripe for use in reinforcement learning to build better agents period. I’m excited about the efforts to use verified mathematics in reinforcement learning. But I’d love to see even more experiments in bringing verification to the agentic coding world. This is an exciting time in programming languages and formal methods research. There’s only one way out of the increasingly unwieldy mountain of LLM generated code: We must prove. We will prove.

@narayanarjun @AmplifyPartners I agree and I’m optimistic too - in January I personally spent several hours building full systems with verification harnesses. Two empirical public examples from me and my team - github.com/nerdsane/redis… github.com/jm424/helix/tr… We have a few more internal Datadog examples.

@DominikTornow @resonatehqio I did similar experiments one with Redis and other with Kafka with different design decisions. Poured all energy into specification and verification. We deployed and tested both in a non production environment at @datadoghq github.com/nerdsane/redis… github.com/jm424/helix

We asked Claude to build a durable execution platform from scratch The pit of success?! The agent harness. All of our effort went into specification and verification The result?! A correct and complete @resonatehqio server

Now @Keleesssss can finally say our prognosis has reached mainstream 😄

redis-rust, a casual reimplementation experiment of Redis in Rust with different trade-offs and heavy reliance on formal and semi-formal methods was a transformational experience for me. github.com/nerdsane/redis…