6 ms·

Conformance checking at MongoDB: Testing that our code matches our TLA+ specs

110 points by todsacerdoti 1y ago

usernamed7 1y ago
[flagged]
- compton93 1y ago
  I consulted on a project that was using MongoDB even though it was obvious from the concept that an RDBMS would be better, however I went in with an open mind and gave MongoDB a red hot crack. It straight up ignored indexes with no explainable reason why. We had a support contract and they just gave us the run around.
  - usernamed7 1y ago
    yeah i've had similar experience but never had indexes get ignored! 100% not surprised though.
- random3 1y ago
  [flagged]
- nailer 1y ago
  To be fair, about a decade they did stop losing data, but they did play with everyone's data for about a decade first. https://stackoverflow.com/questions/10560834/to-what-extent-are-lost-data-criticisms-still-valid-of-mongodb https://stackoverflow.com/questions/10560834/to-what-extent-...
  - usernamed7 1y ago
    lord knows i've been through this... glad it's something they finally solved for.
- deleted 1y ago
  [deleted]
- merek 1y ago
  Where? I see the following > I was excited about this vision. Too often, an engineer tries to write one huge TLA+ spec for the whole system. It's too complex and detailed, so it's not much easier to understand ...
  - usernamed7 1y ago
    looks like the article was updated after the version I read.
magicalhippo 1y ago
About 15 years ago or so, webscale was everything and MongoDB was webscale[1][2] hence being used everywhere. Has it become a legacy product, or are there still good reasons for using it in a new project in 2025? [1]: https://www.youtube.com/watch?v=b2F-DItXtZs https://www.youtube.com/watch?v=b2F-DItXtZs [2]: https://news.ycombinator.com/item?id=1636198 https://news.ycombinator.com/item?id=1636198
- Magmalgebra 1y ago
  > or are there still good reasons for using it in a new project in 2025 it's not clear there ever was. Most of the big users I'm aware of, like Stripe, don't seem to have needed it and regretted the decision. Big data didn't become a thing in the way people expected[0]. If you really did need the scalability of Mongo you'd choose a NewSql database like TiDB[1]. [0] https://motherduck.com/blog/big-data-is-dead/ https://motherduck.com/blog/big-data-is-dead/ [1] https://docs.pingcap.com/ https://docs.pingcap.com/
  - threeseed 1y ago
    a) Big data is more than just the size of the data. It's about how you treat that data i.e. instead of doing expensive and brittle up-front RDBMS modelling you instead dump it all into a data lake and figure out how to handle the data at run-time. And it is still the standard pattern in almost all companies today. b) Nobody was choosing MongoDB solely for performance. If it was you would choose some in-memory K/V store. It was about it being the only well supported document store that was also fast and scalable. c) Stripe’s DocDB is an extension of MongoDB Community: https://stripe.com/blog/how-stripes-document-databases-supported-99.999-uptime-with-zero-downtime-data-migrations https://stripe.com/blog/how-stripes-document-databases-suppo...
    - guappa 1y ago
      That's not how software works. In my experience using mongodb just means that now every single bug in the code creates messed up data for a few months/years and then when that data pops up the software crashes :D
amazingamazing 1y ago
interesting article - I wonder why TLA+ isn't more popular. seems useful, but I guess it's hard to iterate fast with it.
- windows2020 1y ago
  It's the complete opposite of asking an LLM to make an app, which is all the rage.
- ketzo 1y ago
  I think it’s just fairly rare that formal verification is valuable to a business. Obviously all software benefits from correctness — but we all know that software certainly doesn’t need to be bug-free to make money! And if the benefits of formal verification don’t outweigh the (non-trivial!) costs — and critically, outweigh them in a business-person-legibile way — then people won’t put up the time and effort.
- shoo 1y ago
  Mike Dodds' article "What Works (and Doesn't) Selling Formal Methods" offers some insight - two points were: (i) many potential applications of formal methods in business do not result in an attractive cost-benefit outcome, relative to mainstream software development approaches, especially in being able to produce enough benefit for a small input of time / resources. (ii) anecdote: one business that needs to produce software that complies with certain validation/quality targets - say achieved with a baseline method using a lot of manual QA and without formal methods - does not get a business benefit to investing in increased validation, they just need enough enough validation to clear the compliance bar or rank slightly ahead of the competition. if formal methods could assist them in achieving the same level of validation to meet their compliance obligations with less cost than their baseline development and QA processes then they might have much more appetite to invest in formal methods. https://www.galois.com/articles/what-works-and-doesnt-selling-formal-methods https://www.galois.com/articles/what-works-and-doesnt-sellin... corresponding HN thread from earlier this week: https://news.ycombinator.com/item?id=44131324 https://news.ycombinator.com/item?id=44131324
- cmrdporcupine 1y ago
oggy 1y ago
Funny to see this posted on HN, just last week I finished writing a blog post about a project I did for checking that code matches the TLA+ specs so I have to shamelessly plug it :) [1] I was aware of the MongoDB paper, but I ended up actually doing exactly what they suggested wouldn't work: I instrumented Rust programs to log traces and checked them against the specification. Even though the models were largely also post-factum models as in their case (i.e., the code was there first, and models were built later on), this worked for us since the models really were aimed at capturing the implementation's behavior. Our target implementation is possibly smaller than what they had to deal with, though (it's only around 5kLoC of Rust smart contracts) so that's a factor. My technique was slightly different, though. First, I ended up ignoring the initial states, because tests would often manually create fixtures that would serve as a starting point. So I only ended up checking that trace steps obey the transition predicate, which is weaker, but hey, all this is best-effort only anyways. Second, I ended up using the Apalache tool instead of TLC; the reason being that my transitions were sometimes of the form "there exists a number between 1 and N". While model checking you would pick a small N, but in the test runs where the traces come from the N was sometimes huge. TLC ends up enumerating all the possibilities between 1 and N, whereas Apalache translates the whole thing into an SMT formula which is generally trivial to check. Apalache also has the side benefit of requiring type annotations (and providing a type checker) which makes the models a lot easier to refactor when the code changes. I also ended up creating a small library for helping instrument Rust programs to collect such logs. The idea here was to minimize the amount of logging statements in the production code, to keep it out of the way of the people working on the code base who aren't familiar with TLA. It's somewhat specific to our code base, and there's a fair amount of unsafe nastiness that works only because our code is of certain shape, but in case someone's interested, it's open source: https://github.com/dfinity/ic/tree/master/rs/tla_instrumentation https://github.com/dfinity/ic/tree/master/rs/tla_instrumenta.... I wasn't aware of the 2024 paper they reference though, so curious to see what approach they took. [1] https://www.mongodb.com/blog/post/engineering/conformance-checking-at-mongodb-testing-our-code-matches-our-tla-specs https://www.mongodb.com/blog/post/engineering/conformance-ch...
- jiryu 1y ago
  That's a really cool technique oggy, I don't think I've heard of anything exactly like it. If you haven't told the TLA+ community about it yet, I'm sure they'd like to learn about your approach, either on the mailing list[1] or at the next TLA+ conference[2] in 2026. [1] https://groups.google.com/g/tlaplus https://groups.google.com/g/tlaplus [2] https://conf.tlapl.us/home/ https://conf.tlapl.us/home/

110 points by todsacerdoti 1y ago

usernamed7 1y ago

[flagged]

compton93 1y ago
I consulted on a project that was using MongoDB even though it was obvious from the concept that an RDBMS would be better, however I went in with an open mind and gave MongoDB a red hot crack. It straight up ignored indexes with no explainable reason why. We had a support contract and they just gave us the run around.
- usernamed7 1y ago
  yeah i've had similar experience but never had indexes get ignored! 100% not surprised though.
random3 1y ago
[flagged]
nailer 1y ago
To be fair, about a decade they did stop losing data, but they did play with everyone's data for about a decade first. https://stackoverflow.com/questions/10560834/to-what-extent-are-lost-data-criticisms-still-valid-of-mongodb https://stackoverflow.com/questions/10560834/to-what-extent-...
- usernamed7 1y ago
  lord knows i've been through this... glad it's something they finally solved for.
deleted 1y ago
[deleted]
merek 1y ago
Where? I see the following > I was excited about this vision. Too often, an engineer tries to write one huge TLA+ spec for the whole system. It's too complex and detailed, so it's not much easier to understand ...
- usernamed7 1y ago
  looks like the article was updated after the version I read.

magicalhippo 1y ago

About 15 years ago or so, webscale was everything and MongoDB was webscale[1][2] hence being used everywhere. Has it become a legacy product, or are there still good reasons for using it in a new project in 2025? [1]: https://www.youtube.com/watch?v=b2F-DItXtZs https://www.youtube.com/watch?v=b2F-DItXtZs [2]: https://news.ycombinator.com/item?id=1636198 https://news.ycombinator.com/item?id=1636198

Magmalgebra 1y ago
> or are there still good reasons for using it in a new project in 2025 it's not clear there ever was. Most of the big users I'm aware of, like Stripe, don't seem to have needed it and regretted the decision. Big data didn't become a thing in the way people expected[0]. If you really did need the scalability of Mongo you'd choose a NewSql database like TiDB[1]. [0] https://motherduck.com/blog/big-data-is-dead/ https://motherduck.com/blog/big-data-is-dead/ [1] https://docs.pingcap.com/ https://docs.pingcap.com/
- threeseed 1y ago
  a) Big data is more than just the size of the data. It's about how you treat that data i.e. instead of doing expensive and brittle up-front RDBMS modelling you instead dump it all into a data lake and figure out how to handle the data at run-time. And it is still the standard pattern in almost all companies today. b) Nobody was choosing MongoDB solely for performance. If it was you would choose some in-memory K/V store. It was about it being the only well supported document store that was also fast and scalable. c) Stripe’s DocDB is an extension of MongoDB Community: https://stripe.com/blog/how-stripes-document-databases-supported-99.999-uptime-with-zero-downtime-data-migrations https://stripe.com/blog/how-stripes-document-databases-suppo...
  - guappa 1y ago
    That's not how software works. In my experience using mongodb just means that now every single bug in the code creates messed up data for a few months/years and then when that data pops up the software crashes :D

amazingamazing 1y ago

interesting article - I wonder why TLA+ isn't more popular. seems useful, but I guess it's hard to iterate fast with it.

windows2020 1y ago
It's the complete opposite of asking an LLM to make an app, which is all the rage.
ketzo 1y ago
I think it’s just fairly rare that formal verification is valuable to a business. Obviously all software benefits from correctness — but we all know that software certainly doesn’t need to be bug-free to make money! And if the benefits of formal verification don’t outweigh the (non-trivial!) costs — and critically, outweigh them in a business-person-legibile way — then people won’t put up the time and effort.
shoo 1y ago
Mike Dodds' article "What Works (and Doesn't) Selling Formal Methods" offers some insight - two points were: (i) many potential applications of formal methods in business do not result in an attractive cost-benefit outcome, relative to mainstream software development approaches, especially in being able to produce enough benefit for a small input of time / resources. (ii) anecdote: one business that needs to produce software that complies with certain validation/quality targets - say achieved with a baseline method using a lot of manual QA and without formal methods - does not get a business benefit to investing in increased validation, they just need enough enough validation to clear the compliance bar or rank slightly ahead of the competition. if formal methods could assist them in achieving the same level of validation to meet their compliance obligations with less cost than their baseline development and QA processes then they might have much more appetite to invest in formal methods. https://www.galois.com/articles/what-works-and-doesnt-selling-formal-methods https://www.galois.com/articles/what-works-and-doesnt-sellin... corresponding HN thread from earlier this week: https://news.ycombinator.com/item?id=44131324 https://news.ycombinator.com/item?id=44131324
cmrdporcupine 1y ago

oggy 1y ago

Funny to see this posted on HN, just last week I finished writing a blog post about a project I did for checking that code matches the TLA+ specs so I have to shamelessly plug it :) [1] I was aware of the MongoDB paper, but I ended up actually doing exactly what they suggested wouldn't work: I instrumented Rust programs to log traces and checked them against the specification. Even though the models were largely also post-factum models as in their case (i.e., the code was there first, and models were built later on), this worked for us since the models really were aimed at capturing the implementation's behavior. Our target implementation is possibly smaller than what they had to deal with, though (it's only around 5kLoC of Rust smart contracts) so that's a factor. My technique was slightly different, though. First, I ended up ignoring the initial states, because tests would often manually create fixtures that would serve as a starting point. So I only ended up checking that trace steps obey the transition predicate, which is weaker, but hey, all this is best-effort only anyways. Second, I ended up using the Apalache tool instead of TLC; the reason being that my transitions were sometimes of the form "there exists a number between 1 and N". While model checking you would pick a small N, but in the test runs where the traces come from the N was sometimes huge. TLC ends up enumerating all the possibilities between 1 and N, whereas Apalache translates the whole thing into an SMT formula which is generally trivial to check. Apalache also has the side benefit of requiring type annotations (and providing a type checker) which makes the models a lot easier to refactor when the code changes. I also ended up creating a small library for helping instrument Rust programs to collect such logs. The idea here was to minimize the amount of logging statements in the production code, to keep it out of the way of the people working on the code base who aren't familiar with TLA. It's somewhat specific to our code base, and there's a fair amount of unsafe nastiness that works only because our code is of certain shape, but in case someone's interested, it's open source: https://github.com/dfinity/ic/tree/master/rs/tla_instrumentation https://github.com/dfinity/ic/tree/master/rs/tla_instrumenta.... I wasn't aware of the 2024 paper they reference though, so curious to see what approach they took. [1] https://www.mongodb.com/blog/post/engineering/conformance-checking-at-mongodb-testing-our-code-matches-our-tla-specs https://www.mongodb.com/blog/post/engineering/conformance-ch...

jiryu 1y ago
That's a really cool technique oggy, I don't think I've heard of anything exactly like it. If you haven't told the TLA+ community about it yet, I'm sure they'd like to learn about your approach, either on the mailing list[1] or at the next TLA+ conference[2] in 2026. [1] https://groups.google.com/g/tlaplus https://groups.google.com/g/tlaplus [2] https://conf.tlapl.us/home/ https://conf.tlapl.us/home/