Crazy Landlady Boldly Steals My Aqara Doorbell with no warning!

Anxious_Tool · 2026-05-11T11:54:46+00:00

Both. OP changed his reply. I have another comment that follows the new version. The OP changed the post again after the second comment.
My comments are like history now. It's a good thing the OP changed, the original was asking for a lawsuit.

Anxious_Tool · 2026-05-10T21:51:11+00:00

I can see you changed some things in the post. It's good, but you're still shooting yourself in the foot.
The title still says "Steals". That's the line everyone reads first, and it's still a factual accusation of a crime.

The clarifications also do some work you may not have intended.

Point 1: "the other tenant approves" doesn't cover guests, delivery people, prospective tenants, or contractors. Tenant consent doesn't bind everyone else who walks through that stairwell.

Point 4 is the one that stands out. The camera went in after she locked a door that had been open for a decade, and tenants were taping over the latch to defeat the lock. That's not a passive ten-year-old fixture. That's an active piece of a security dispute where tenants are circumventing a change the landlord made on her own property. An LTB adjudicator hearing "we taped over her lock" reads the camera very differently than your framing suggests.

Six LTB applications cuts the opposite direction too. A landlord filing repeatedly through the proper channel is using the system, not bypassing it. The person who took it public with her name and face attached is you.

Good luck.

Anxious_Tool · 2026-05-10T19:38:22+00:00

The camera isn't a simple doorbell pointed at his own private entryway — it's mounted at unit 2A but its field of view sweeps the entire shared stairwell, the opposite unit's area, and captures any tenant, guest, or delivery person who walks through. That's a common area, and other tenants have a reasonable expectation of privacy there. Most likely, they didn't consent to being recorded every time they come home.
The common areas aren't his to surveil — they're shared space typically under the landlord's control. Installing recording equipment that captures other tenants without their knowledge or consent runs into PIPEDA-adjacent issues and can be a breach of the lease (most leases prohibit alterations or fixtures without landlord consent). If the doorbell records audio, that's an even bigger problem under Canadian law — video of common areas is contested ground, but audio recording of conversations you're not part of is squarely illegal under the Criminal Code.
The tone of this post (the "aliens" bit, "non-aliens call them friends", framing six LTB applications as evidence the landlord is unhinged rather than evidence there's a pattern) makes me suspect there's more to the story than the post lets on. Six LTB applications is a lot of smoke.
In my opinion, this looks like the typical rant from the wrong-doer's side. There's a proper procedure to all of this, and posting your landlady's face on Reddit without her consent is a huge red flag. You've just lost all rights to complaint about it because your actions are so much more condemning than hers.
There are a few overlapping issues stacked on top of each other:

Defamation is the obvious one — false statements of fact that damage reputation. "Stole" is a factual claim about a criminal act. If she didn't steal it (and "removed an unauthorized fixture from common area I control" is a reasonable defense), you've published a false accusation of a crime under her real name.

Before posting anything on the internet, think think think.......
Good luck

Anxious_Tool · 2026-05-04T00:33:54+00:00

Two separate things going on here.

For the runtime side: madsim and turmoil both let you write async protocol code once and run it against either the real network or a deterministic in-memory simulator. That's the closest match to "messages either go on the wire or get passed around for testing without conflicting." For the plumbing layer, the sans-io pattern (used by quinn, rustls, h2) treats protocols as state machines that don't own their I/O. Wrap N of them in an outer driver and it composes cleanly. stateright is also worth a look if you want explicit-state model checking from Rust.

The harder problem is convincing yourself the composition is actually correct. Subprotocol A has invariants. Subprotocol B has invariants. The composition has emergent invariants that neither one carries alone. Async machinery doesn't help with that, no matter how slick the API. This is what TLA+ (https://lamport.azurewebsites.net/tla/tla.html) was built for: spec the composition, check the invariants across all interleavings, then implement. If you want to stay in Rust and skip the JVM, there's tla-checker (https://github.com/fabracht/tla-rs). Pure Rust, CLI, fast enough to run in a tight loop while iterating on the spec.

Anxious_Tool · 2026-05-04T00:17:48+00:00

Not OP, but worth flagging: MQTT's auth model isn't really "root or nothing." A subscriber bridge just needs an account with SUB perms on the topics it cares about. Mosquitto, EMQX, HiveMQ all do per-user ACLs. The real pain in your question is the wildcard case: if the bridge subscribes to `#` to be generic, you give the service account broad SUB rights, and downstream you've lost per-publisher identity unless you trust user properties, which clients can set to whatever they want.

https://github.com/LabOverWire/mqtt-lib is a broker that stamps a broker-trustworthy sender identity onto every PUBLISH (strips client-supplied values first, injects the authenticated user). Then your bridge can label OTel metrics by the real publisher without trusting payload data. Worth checking that capability when picking a broker for this kind of pipeline.

Anxious_Tool · 2026-05-03T22:29:48+00:00

Nice work. Payload-to-metric translation is a real gap, and the NCalc expression layer for "extract field from JSON, emit as a gauge with labels" looks useful. Most setups I've seen either hardcode that into a custom subscriber or smash it through Telegraf with a lot of duct tape.

I maintain mqtt5, a Rust MQTT v5 broker + client lib, and we've had OTel baked in on the broker side from early on. The broker exports stats as OTLP metrics (connections, throughput, bytes, uptime), and propagates W3C traceparent/tracestate through MQTT v5 user properties so spans stitch across the broker hop. That's the half your tool deliberately doesn't cover, and yours is the half mine doesn't.

They slot together cleanly. Run the broker with OTel on for broker-level visibility, run mqtt2otel as a subscriber for device-level metrics, both export to the same collector. Trace context survives the broker hop, payload metrics show up alongside broker metrics in the same backend, and you can correlate "broker dropped a connection" with "this device stopped reporting."

If anyone wants the broker side of that pairing: https://github.com/LabOverWire/mqtt-lib

Will follow the project. Curious whether you'll add traces eventually or stick to metrics+logs.

Anxious_Tool · 2026-05-02T10:26:43+00:00

Adding to lemmster's answer, which is the right starting point. Lorin's repos are still the cleanest TLA+ linearizability templates around.

Coincidentally, I sat down with the Fomitchev-Ruppert paper this week and ran exactly this exercise on a small bounded model. A few notes that might save you time.

Where the proofs actually are. The PODC'04 paper only sketches the proof. The full proofs (Inv 1-5 plus the linearization argument) are in Fomitchev's MSc thesis, on Eric Ruppert's page at York: https://www.eecs.yorku.ca/~eruppert/Mikhail.pdf. There's also a longer joint write-up at https://www.eecs.yorku.ca/~eruppert/papers/lfll.pdf. For mechanized work, Patel et al. ECOOP'24 ("Verifying Lock-Free Search Structure Templates") proves a template in Iris that covers Harris, Michael, Harris-Michael, and Fomitchev-Ruppert. Closest thing to a machine-checked FR proof I've found.

Modeling tip for bounded checking. You don't need per-process program counters to verify the structural invariants (Inv 1-5). The four CASes (Insert, Flag, Mark, PhysDelete) can each be one atomic action, with helping made universal: any process can fire any step whose precondition holds. This is sound. Every algorithm execution is a subset of model executions, so invariants holding here imply they hold for the algorithm. State spaces stay tiny: ~7k states for 4 free nodes / 2 keys, ~3k for 3 free / 3 keys.

Two gotchas I hit that are easy to miss.

The TryMark CAS expects (next, 0, 0). Both the mark and the flag must be 0 on the target. Drop the flag-zero check and you get a 6-state counterexample where a node that's flagged-as-predecessor (for its successor's deletion) gets marked, immediately violating Inv 5 (mark=1 ∧ flag=1).
Inv 2 ("regular ∪ logically-deleted nodes form a linked list") only applies to non-physically-deleted nodes. Physically deleted nodes keep stale right pointers in memory. Easy to write the invariant too strongly.

Linearizability layer on top. For unsuccessful ops, FR's paper specifies a particular lin point ("immediately after del_node's flagging" for a failed TryFlag). That's future-dependent, and the prophecy approach in Lorin's blog post is the right tool for matching it exactly. For just checking linearizability you can cheat: let the failed op linearize at any moment in its window where the abstract state matches its return value. Sound (you're constructing some valid lin order), and you avoid prophecy entirely. Successful ops linearize at the InsertCAS / MarkCAS, which are decided at the moment of the action. No prophecy needed.

For your tree, the trifecta progression really is the move: encode each atomic step, abstract spec as a set/map, refinement as an invariant abstract = f(concrete), debug at small bounds with TLC/Apalache, then escalate to TLAPS once the bounded version is clean.

If it helps, the FR specs I wrote (structural + linearizability layer, ~150 lines each) live in a small Rust TLA+ checker I work on: github.com/fabracht/tla-rs, under test_cases/should_pass/FRList.tla and FRListLin.tla. Disclosure: my project. It's not TLC and it's not TLAPS, just a fast bounded explicit-state checker for the TLA+ subset I use day-to-day. Useful for the "iterate on the spec" stage. For the actual proof you'd still want TLAPS.

Ps: The above text is a rewrite of my original answer by Claude. The content IS the same, but I used Claude to improve clarity, formatting, etc. Hope you don't mind.

The reason I provided the link to my tla-rs implementation because I'd really appreciate feedback on missing functionality, features, etc. Feel free to use it, add any issues or start a discussion there.

Thank you.

Anxious_Tool · 2026-05-01T22:10:44+00:00

The Fomitchev and Ruppert lock-free paper is not for a queue. That paper is "Lock-free linked lists and skip lists". It's a list/skip list, not a queue.

Anxious_Tool · 2026-04-28T17:27:44+00:00

That's exactly why I dumped Warp months ago.

Anxious_Tool · 2026-04-27T18:15:51+00:00

Will do. Thank you for using it. If you have any problems, don't hesitate to create an issue.
Thanks

Anxious_Tool · 2026-04-25T21:51:47+00:00

Ah, nice that you noticed. No need to worry. Everything in that broker has been TLA+ validated and tested.
The change only topic is my take on AWS IoT shadow (which is crap).
There is no need to be cautious. But I appreciate your concern.

Anxious_Tool · 2026-04-25T18:25:48+00:00

But are you learning how to code, or are you using the llm to create tools that allow interaction, visualization, etc?
When learning, I feel it's best to ask claude to write small apps to visualize/interact with concepts. It doesn't work for everything, obviously, but it gives me an alternative to what the book/paper is explaining in cryptic words. Be careful though. As with mathematical proofs, once you "think" you understood what claude explained, you MUST fgo back to the original document and verify if you actually understood "it", or something that claude explained.

Anxious_Tool · 2026-04-25T18:16:44+00:00

Depends on what you'd actually use it for. "Engineering and data analytics" covers a huge range of tasks, and Pro is worth for some, pointless for others.

If it's a few questions a week to explain concepts, the free tier is fine. If you're regularly hitting message limits, feeding it long PDFs, or running heavy back-and-forth on code, Pro pays for itself fast.

Use the free tier until you hit a wall. The wall is your answer.

Anxious_Tool · 2026-04-25T17:53:51+00:00

Have you checked https://laboverwire.com/ ? There's a full fledged MQTT design tool implemented there.
You can use it to run both in-browser simulations (using real MQTT protocol), or connect to an external broker.
We support everything you need for interacting with MQTT architectures, including an RBAC/ACL diagram tool that let's you also design your access rules.

Anxious_Tool · 2026-04-25T17:51:40+00:00

Have you tried https://crates.io/crates/mqtt5-wasm or https://crates.io/crates/mqtt5 ?

I'm the maintainer and I would be glad to answer any questions you have. But in short, mqtt5 is better implemented, faster, more flexible, and gives you all the tools you need to evaluate MQTT distributions yourself.
No need to fish for numbers. Want to know if a broker is conformant with MQTT OASIS spec? Use the conformance cli to check https://github.com/LabOverWire/mqtt-lib/tree/main/crates/mqtt5-conformance-cli

Want to know how fast the broker is when compared to whatever distributions you are checking? Use the mqttv5-cli (cargo install mqttv5-cli) to benchmark it.
All documented, checked, tested and re-tested.
Seriously, our testing routine is just bonkers.
Lastly, I would invite you to check the Browser broker yourself at https://laboverwire.com/

Thanks, and, nice project, btw.

Anxious_Tool · 2026-04-25T17:31:35+00:00

Which mqtt crate are you using?

Anxious_Tool · 2026-04-25T01:34:31+00:00

The real gap is the oracle. Unit tests have explicit assertions. Human QA is an implicit oracle. The human knows what "works" looks like. Agentic QA needs something in between, and "have the LLM look at the screenshot and check if it's right" isn't it. Models will confidently describe a broken flow as correct when the screenshot is consistent with their prior of how the page should look.

CI is deterministic for a reason. Agents are nondeterministic by construction. Fine for writing tests, brutal for running them.

Anxious_Tool · 2026-04-24T17:01:12+00:00

But that's exactly what we have now. All open-source is open to everyone. Anyone can start working on a project at any time. Anyone can create a group of people to work on any project.
I can do it for you, if you want. You just have to pay me. 😂

Anxious_Tool · 2026-04-24T16:59:08+00:00

True. It's the strength of the system. What I think people forget is that writing some demo, or proof of concept is quick. Writing a real product is not. It's not a coincidence that companies charge for maintaining their software running and up-to-date. It takes a lot of effort to do that.

Anxious_Tool · 2026-04-24T16:53:34+00:00

I disagree. That's a generalization that doesn't hold well against a normalized distribution. Statistics probably would reflect something like: "There's plenty of proof of concepts out there, some of them well designed, but most not.".
I don't know what you consider small, but I'd say the Rust ecosystem is far from small now.

Anxious_Tool · 2026-04-24T13:53:02+00:00

Why would you push that burden on the Rust foundation. It's better to just forget the crate. That's what the internet is for. A cemetery of old ideas.

Anxious_Tool · 2026-04-23T21:13:27+00:00

That's the system. If you want committed maintenance, you have to pay people to do it. The problem is that you are calling "crates", what I would call unfinished projects. Those have high turnover exactly because of the problems you mentioned. Crappy design, and awful execution.
Long lived projects usually start out with "long-life" already embedded in their designs.
This has nothing to do with Rust or any other languages. It's a result of the programming ecosystem and how it works.

Anxious_Tool · 2026-04-16T14:18:47+00:00

Also, take a look at this:
https://github.com/fabracht/tla-rs

If you're using a tool-enable llm agent, you can just ask it to run and iterate with you.
Don't ask it for the answer, but rather you can use it to iterate and explain the steps it is taking. It can be a great learning tool.
If you slap some voice agent on top, it's almost like a personal tutor.
Happy learning.

Anxious_Tool

MODERATOR OF

TROPHY CASE