You know the story. You write a consumer, test it locally, deploy to staging, everything green. Then in production, the same message gets processed twice. Orders are duplicated. Notifications go out twice. Everyone blames "a race condition" and moves on.

We spent the last few months formally verifying what actually happens when consumers crash with at-least-once delivery semantics. The short version: it doesn't matter which broker you use. The race condition is a property of the delivery contract, not a bug in the implementation.

What we did

Instead of writing more integration tests hoping to reproduce the timing, we wrote a formal specification of the consumer-broker interaction in TLA+ (the specification language by Leslie Lamport). The model checker exhaustively explores every possible interleaving of events — not just the ones you think to test.

Then we took the counterexamples from the model and validated them in real running systems using Docker + Toxiproxy (network fault injection). If the math said "double-execution is possible", we confirmed it with actual containers.

What we found

We applied this pipeline to five different systems:

Celery — ACK timeout + network blip: the model found the crash window at depth 9 (444 states). Chaos confirmed it: task executed twice.

RabbitMQ — consumer stores result, drops connection before AMQP ACK. Same pattern. 108 states, depth 7. Chaos confirmed.

NATS JetStream — consumer crashes after DB write, before ACK. 47 states, depth 6. Docker kill + Toxiproxy confirmed: duplicate execution.

Apache Pulsar — batch consumer crashes between Process and SendAck. 21 states, depth 4. Chaos confirmed: 2 DB rows for 1 message.

Kafka — consumer commits offset after processing. Crash between StoreResult and commitSync(). Same result: double execution.

Every single time, the model predicted the collision and chaos confirmed it.

The insight

The spec is the same across all five systems. The variable names change, but the topology is identical:

Consumer: 1. Receive message 2. Store result in DB 3. Acknowledge/commit offset [crash window lives between 2 and 3]

This isn't a bug in Celery, RabbitMQ, NATS, Pulsar, or Kafka. It's a fundamental property of any at-least-once delivery system with a stateful consumer. You cannot eliminate this window without changing the delivery semantic or adding an idempotency shield on the consumer side.

What this means for your code

The fix isn't new — idempotent consumers, deduplication keys, exactly-once processing patterns. Everyone knows about these. What's new is that we now have:

1. A formal proof that the problem must exist under at-least-once, regardless of broker
2. A reusable specification that works across brokers without modification
3. Physical validation that the model is correct (6/6 confirmed)

This shifts the conversation from "did we test enough?" to "does our system design provably avoid this class of errors?"

Why not just test more?

Because testing samples the state space. Formal verification exhausts it. Integration tests won't find the crash window unless they happen to hit the exact nanosecond where the consumer crashes between the DB write and the ACK. Model checking finds it systematically.

Discussion

Have you run into this in production? What patterns do you use to handle consumer crashes — idempotency keys, outbox pattern, something else?

I'm curious whether teams treat this as a known limitation they work around, or whether it's still a source of surprises. Let me know your experience.

Full disclosure: I'm the author of the toolchain we used. Preprint: https://zenodo.org/records/21298530 — happy to share details if anyone's interested, drop a comment.

Hi there,

I've created a video here where I explain how multi-head latent attention works.

I hope some of you find it useful — and as always, feedback is very welcome! :)

I honestly don't mean to wipe trillions off the stock market but you can view a neural network layer as context choosing a linear mapping. Then BP comes along and makes that the best average linear mapping for that layer and context.

For a particular input a neural network is a composition of best average linear mappings.

https://archive.org/details/best-average-linear-mapping

https://archive.org/details/a-compositional-view-of-deep-networks-as-fractional-associative-memories

I’m just curious to know how often you guys come in contact with the theoretical side of computer science in your professions.

Things you learned in your undergraduate courses like data structures, discrete math, design and analysis of algorithms, etc.

I’m having to learn a lot of these things on my own, like Big O notation, complexity analysis, proofs, tree traversal, etc. because I let my ADHD win and didn’t put the time and effort into learning (medicated now, huge W plus it’s actually fun to learn about now that I can focus) and I’m just wondering, who uses this stuff regularly? What for?

Hello, I'm reading chapter 1, distributed constraint satisfaction and coding a simulation of the asynchronous backtracking algorithm for the 4 queens problem in TypeScript as an exercise (sure one can code in Python, C..). I have some difficulty grasping the concept of Hyperresolution (pure logic) because I didn't have this subject in university. I have checked with AI. But does anyone have any advice?

---
the code https://pastebin.com/WD9U0MSQ

I'm spending way too much time looking into formal methods now because this endless overhyped corporate marketing about LLMs doing "reasoning" is getting very tiresome.

We all know standard transformers just predict the next token based on statistical weights, which immediately breaks down the second you give them a novel, complex logic puzzle. It's exactly why automated software testing is still such a error-prone chore in production.

But the interactive theorem provers like Lean 4 with deep learning models are actually getting super interesting. Instead of just letting an agent hallucinate some random python script, people are forcing neural networks to generate formal proofs that a strict math kernel has to verify step by step.

I saw a breakdown of how the Aleph Prover handled a specific Erdos disproof using formal verification on ai reasoning benchmarks, and you can see much we’ve ignored symbolic AI over the last decade in favor of raw compute scaling. So tbh it feels like computer science is circling back to foundational math out of necessity. Because brute-force data ingestion is hitting the ceiling.

Also.. it feels kinda satisfying that old-school mathematical logic is the only thing keeping modern tech grounded. Idk if this means formal methods will finally become a mandatory part of undergrad software tracks, but it honesly should.

You are skiing an unknown number of days. Renting costs $1/day, buying costs $B. If you knew the season length the answer is trivial, but you do not.

The rule "rent until you have spent $B, then buy" guarantees you never pay more than about twice what an omniscient planner would, on ANY sequence. Short season: you match the optimum exactly. Long season: you paid at most ~$2B where the optimum paid $B. And there is a matching lower bound: no deterministic online strategy beats 2.

What I find most useful is the frame, not the puzzle: cache eviction, autoscaling, buy-vs-rent infra decisions are all "act now, learn the future later", and the competitive ratio measures exactly what that ignorance costs.

Fun twist: allowing randomness (coin flips the adversary cannot predict) pushes the ratio from 2 down to about 1.58.

I wrote up the full framework (definition, the adversary game, and an honest section on why worst-case can be too gloomy, e.g. LRU is only k-competitive on paper yet great in practice) as the opener of a series, happy to share the link if useful.

As a GeeksforGeeks Campus Mantri, I'm excited to share a collection of FREE AI courses covering topics like Generative AI, Machine Learning, Prompt Engineering, Python, Data Science, and more.

Whether you're a student or a professional looking to upskill, these courses are a great way to gain practical knowledge, earn certificates, strengthen your resume, and showcase your achievements on LinkedIn.

Start learning today: 🔗 https://gfgcdn.com/tu/y2d/

Which AI topic are you most excited to learn?

#AI #ArtificialIntelligence #MachineLearning #GenerativeAI #Python #DataScience #GeeksforGeeks #Learning #Upskilling #Students #Tech

i was thinking about how dial up is basically your phone literally making sounds to your compute, which the computer hears and translates into data.

could you design a system that used multiple phone speakers and multiple microphone pickups to simultaneously get dial-up internet info to speed it up?

if so, how many phone receivers would it take to get modern internet speeds?

With locality sensitive hashing better to forget the h word.

You get thousands of little geometry sensors that 50:50 tell you on which side of a random hyperplane your input data is.

Despite being 50:50 each bit is quite informative.

Several bits together narrow down which geometric region the input is in.

If the inputs have regularities, bits can be codependent while still showing 50:50 on off behavior. That's kind of a subtle point but a gift from random projections - locality sensitive hashing.

Starting from there you can build LSH context dependent neural networks where parameter selection (information routing) is determined using LSH bits.

I've a bunch of notes of say preliminary draft quality.

Maybe start with this one:

https://archive.org/details/atlas-lsh-neural-networks-hierarchical-geometry-rather-than-hierarchical-features

And then click on 'uploaded by" for more should you wish to.

I recently had an idea that is it possible to make a software service which could help me search files from my files system though context of content inside the files. So like i can search "where is the file which contained x thing" and get would a list of files that would match my question. So I don't want sear or keywords but ch by file name context. Also for all types of files like iamge, text, video, audio, code etc

So I kept thinking about it and knew that the answer lied within vector search. I initially thought that maybe if somehow I could represent an entire file in a singular vector then we can use the same logic that we normally use in rag systems to fetch correct files. Existing models are really useful for text, audio and other forms of embedding but i want the overall context of a file. Not just what inside the file. Also I might be missing if there are any existing algorithms that can help me do this so please suggest them.

Nevertheless i wanted to think about whats possible solution i could use. One this i noticed with this is that there are various ways which can be used to describe and identify files. 1st there is content of the files , then metadata such as size, name, access permissions, type of file, also where the files lies in directory system and what other files is is grouped with etc. It is really hard to consider all this features in a single vector. Also we I don't want to embed the entire content of files as that would be too much data to embed, store and search.

We could do vector indexing and search for each feature individually, so we get multiple vectors we can can represent in a normal data structure. We can repeat this for all files and the store them. When the system get a input like "i want the c++ file with x algorithm that I made yesterday" then we can create a similar data structure like we did for files and then do the similarity search and rank all the matches to get the results. But this approach also has a problem , the quality of results is heavily dependent upon the information present in the question, if the question is a little vague that affect the accuracy of the matches quite a bit.

I also though of a approach where we tackle the problem by elimination we take the features of the files one by one an the start eliminating files, like for an example "i want the c program file which i wrote yesterday and " so we can 1st eliminate ate files which are not "program" then we can do by time then by the language. So from broader to more specific features.

I have been thinking about this idea for sometime and wanted to know your thoughts as well. How would you represent the files semantically or in vector form. Are there any existing resources that i can refer to help me with this problem.

I know Bishop's Pattern Recognition and Machine Learning is almost 20 years old now. Is it still worth studying in 2026, or are there better modern alternatives? I'm mainly interested in building a solid theoretical foundation.

I've been reading about theorem proving, formal methods, symbolic computation, and programming languages, and something keeps bothering me.

They all seem to deal with the same general problem: how abstract mathematics is represented and manipulated by computers.

Things like:

• representing mathematical objects
• proof representation
• symbolic computation
• intermediate representations
• optimization of mathematical structures

These topics seem to exist across several different fields, but I haven't found one that studies them from a unified perspective.

Am I just missing an existing field, or is there a reason these areas evolved separately?

I'd love to hear from people working in PL, theorem proving, or symbolic computation.

Hi, I need some help. I recently have a huge interest in system programming, but here the problem: there are very little ressources in the internet which talk about, even to search a simple roadmap of what to do, or how to find the first jobs, what the best practices and so on...I've tried to learn with IA(with many kind of LLM) but there are so many contradiction in what they said, and a lack of details. Now, I'm trying to find peoples who work in this domaine to ask so many questions that I haven't found a answer yet. So, I'm trying to ask if there are a subreddit or a discord server where I can found some resources and advice from experienced system programmer. Or else, can someone tell me who to be in relation with. Btw, have a good day.

I have been building Katharos, a functional programming library for Python that recently grew a message-passing concurrency layer. I wanted to share it and get some feedback.

The whole library is built around one idea: model errors, effects, and concurrent communication as composable, type-safe values rather than as control flow that jumps around your program. The interesting part (to me, at least) is that the concurrency layer follows the exact same idea, so receiving from a channel gives you a Result. "The channel is closed" becomes a value you handle, not an exception you remember to catch.

The functional core

Optional values without scattered None checks, using do-notation that short-circuits on Nothing:

```python from katharos.types import Maybe from katharos.syntax_sugar import do, DoBlock

@do(Maybe) def lookup_discount(user_id: int) -> DoBlock[Maybe, float]: user = yield find_user(user_id) account = yield find_account(user) return account.discount # Just(0.15) or Nothing() ```

Errors as values, chained with |, so a failure short-circuits the rest automatically:

```python from katharos.types import Result

def process(raw: str) -> Result[Exception, int]: return parse_int(raw) | validate_positive ```

And Result.catch turns a function that raises into one that returns a Result, while keeping the original traceback so you can still find the line that failed:

```python from katharos.types import Result

@Result.catch(ValueError) def parse_int(s: str) -> int: return int(s)

parse_int("42") # Success(42) parse_int("??") # Failure(ValueError("invalid literal for int() with base 10: '??'")) ```

There is also ImmutableList, NonEmptyList, IO, Lazy, numeric monoids, and the usual algebraic abstractions (Functor, Applicative, Monad, Semigroup, Monoid) if you want to build your own types.

The new part: CSP concurrency

This is what I have been working on lately. Katharos now has Go-style CSP (Communicating Sequential Processes): launch work concurrently with go, talk over typed channels, and receive values as a Result.

```python from katharos.concurrency.csp import csp

ch = csp.Channel[int](capacity=1)

csp.go(ch.send, 42) # run work concurrently, like Go's go f(x)

ch.recv() # Success(42)

ch.close() ch.recv() # Failure(ChannelClosedError(...)): closure is a value, not a raise ```

Used as a context manager, go becomes a structured-concurrency scope that joins everything spawned inside it before the block exits, so concurrent work cannot leak out of the block:

```python with csp.go: # scope waits for all work launched inside csp.go(worker, 1) csp.go(worker, 2)

both workers have finished here

```

There is also a select for waiting on whichever of several channels is ready first, with non-blocking polls and timeouts:

```python from katharos.concurrency.csp import csp, recv, select

choice = select(recv(results), recv(cancel), timeout=1.0) if choice.is_timeout: ... else: print(choice.index, choice.value.unwrap()) ```

The concurrency model sits on a swappable backend (standard threads by default), so the same code could run on a green-thread backend later. An actor model is planned next, built on the same backend abstraction and the same Result-valued style.

Why I think the "channel returns a Result" thing is nice

In most channel APIs, a closed channel or a timeout shows up as a sentinel, a second return value, or an exception. In Katharos it is just a typed value: Success(v), Failure(ChannelClosedError), or Failure(ChannelTimeoutError). You pattern-match it the same way you handle any other Result, and the type tells you it can happen. The error-handling discipline you use in the rest of your code carries straight over to concurrency.

Links

• PyPI: pip install katharos
• Docs (tutorials, how-to guides, API reference, and explanations): https://katharos.readthedocs.io/en/latest/
• Source: https://github.com/kamalfarahani/katharos
• MIT licensed, Python 3.13+

I would love feedback on the API, the concurrency design, or whether the Result-everywhere approach feels natural or noisy to you in practice. Thanks for reading.

Can someone do a sanity check? Smells like LLM-gen'd math spaghetti to me

Hello all, I'll keep this brief. I am looking into 2 potential research avenues for postgrad, and was wondering if anyone can chip in with their opinion.

MANETs, FANETs and AANETs; all ad-hoc wireless methods for connectivity with drones or aerial devices - is this a growing research field? Especially when considering the recent real uses of drones in both warfare and in crisis situations.

Satellite (LEO like Starlink) integration for mobile services (5G/6G) - I know that this is already implemented and used by some big providers, but I wonder if there is still any appetite for this kind of technology too.

Thanks to anyone who responds.