https://www.mongodb.com/blog/post/engineering/conformance-checking-at-mongodb-testing-our-code-matches-our-tla-specs Conformance Checking at MongoDB: Testing That Our Code Matches Our TLA+ Specs A. Jesse Jiryu Davis June 2, 2025 | Updated: June 3, 2025 Some features mentioned below have been sunset since this paper was originally written. Visit our docs to learn more. At MongoDB, we design a lot of distributed algorithms--algorithms with lots of concurrency and complexity, and dire consequences for mistakes. We formally specify some of the scariest algorithms in TLA+, to check that they behave correctly in every scenario. But how do we know that our implementations conform to our specs? And how do we keep them in sync as the implementation evolves? This problem is called conformance checking. In 2020, my colleagues and I experimented with two MongoDB products, to see if we could test their fidelity to our TLA+ specs. Here's a video of my presentation on this topic at the VLDB conference. (It'll be obvious to you that I recorded it from my New York apartment in deep Covid lockdown.) Below, I write about our experience with conformance checking from 2025's perspective. I'll tell you what worked for us in 2020 and what didn't, and what developments there have been in the field in the five years since our paper. Agile modelling Our conformance-checking project was born when I read a paper from 2011--"Concurrent Development of Model and Implementation"--which described a software methodology called eXtreme Modelling. The authors argued that there's a better way to use languages like TLA+, and I was convinced. They advocated a combination of agile development and rigorous formal specification: 1. Multiple specifications model aspects of the system. 2. Specifications are written just prior to the implementation. 3. Specifications evolve with the implementation. 4. Tests are generated from the model, and/or trace-checking verifies that test traces are legal in the specification. 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 than the implementation code, and state-space explosion dooms model checking. The author abandons the spec and concludes that TLA+ is impractical. In the eXtreme Modelling style, a big system is modeled by a collection of small specs, each focusing on an aspect of the whole. This was the direction MongoDB was already going, and it seemed right to me. In eXtreme Modelling, the conformance of the spec and implementation is continuously tested. The authors propose two conformance checking techniques. To understand these, let's consider what a TLA+ spec is: it's a description of an algorithm as a state machine. The state machine has a set of variables, and each state is an assignment of specific values to those variables. The state machine also has a set of allowed actions, which are transitions from one state to the next state. You can make a state graph by drawing states as nodes and allowed actions as edges. A behavior is any path through the graph. This diagram shows the whole state graph for some very simple imaginary spec. One of the spec's behaviors is highlighted in green. Figure 1. A formal spec's state graph, with one behavior highlighted. Diagram depicting a spec's state graph, with part of the diagram highlighted in green and labeled initial state. The spec has a set of behaviors B[spec], and the implementation has a set of behaviors B[impl]. An implementation refines a spec if B[impl] [?] B[spec]. If the converse is also true, if B[spec] [?] B[impl], then this is called bisimulation, and it's a nice property to have, though not always necessary for a correctly implemented system. You can test each direction: * Test-case generation: For every behavior in B[spec], generate a test case that forces the implementation to follow the same sequence of transitions. If there's a spec behavior the implementation can't follow, then B[spec] [?] B[impl], and the test fails. * Trace-checking: For every behavior in B[impl], generate a trace: a log file that records the implementation's state transitions, including all implementation variables that match spec variables. If the behavior recorded in the trace isn't allowed by the spec, then B[impl] [?] B[spec] and the test fails. Figure 2. Two ways to test that the spec's behaviors are the same as the implementation's. Non-conforming behaviors are highlighted in red. Diagram showing the test between the spec and implementation behaviors. On the left is the spec behavior, with a portion highlighted in red indicating that this behavior only appears in the spec. Between the two diagrams are arrows that highlight the test case generation and trace checking which analyze the two versions. On the right is the diagram for the implementation, which has a portion highlighted in red that indicates a behavior that only appears in the implementation version. Both techniques can be hard, of course. For test-case generation, you must somehow control every decision the implementation makes, squash all nondeterminism, and force it to follow a specific behavior. If the spec's state space is huge, you have to generate a huge number of tests, or choose an incomplete sample. Trace-checking, on the other hand, requires you to somehow map the implementation's state back to the spec's, and log a snapshot of the system state each time it changes--this is really hard with multithreaded programs and distributed systems. And you need to make the implementation explore a variety of behaviors, via fault-injection and stress-testing, and so on. Completeness is usually impossible. We found academic papers that demonstrated both techniques on little example applications, but we hadn't seen them tried on production-scale systems like ours. I wanted to see how well they work, and what it would take to make them practical. I recruited my colleagues Judah Schvimer and Max Hirschhorn to try it with me. Judah and I tried trace-checking the MongoDB server (in the next section), and Max tried test-case generation with the MongoDB Mobile SDK (the remainder of this article). Figure 3. We tried two conformance checking techniques on two MongoDB products. Diagram showing that for this project trace-checking was run on MongoDB server and test-case generation was run on MongoDB Mobile SDK. Trace-checking the MongoDB server For the trace-checking experiment, the first step Judah and I took was to choose a TLA+ spec. MongoDB engineers had already written and model-checked a handful of specs that model different aspects of the MongoDB server (see this presentation and this one). We chose RaftMongo.tla, which focuses on how servers learn the commit point, which I'll explain now. MongoDB is typically deployed as a replica set of cooperating servers, usually three of them. They achieve consensus with a Raft-like protocol. First, they elect one server as the leader. Clients send all writes to the leader, which appends them to its log along with a monotonically increasing logical timestamp. Followers replicate the leader's log asynchronously, and they tell the leader how up-to-date they are. The leader keeps track of the commit point--the logical timestamp of the newest majority-replicated write. All writes up to and including the commit point are committed, all the writes after it are not. The commit point must be correctly tracked even when leaders and followers crash, messages are lost, a new leader is elected, uncommitted writes are rolled back, and so on. RaftMongo.tla models this protocol, and it checks two invariants: A safety property, which says that no committed write is ever lost, and a liveness property, which says that all servers eventually learn the newest commit point. Figure 4. MongoDB replica set servers and their logs. Diagram showing the MongoDB replica set servers and their logs. At the bottom is a follower, with logs 1-5. In the middle is another follower, with logs 1-4. And at the top is a leader with logs 1-6 and log 5 labeled as the commit point. Judah and I wanted to test that MongoDB's C++ implementation matched our TLA+ spec, using trace-checking. Here are the steps: 1. Run randomized tests of the implementation. 2. Collect execution traces. 3. Translate the execution traces into TLA+. 4. Check the trace is permitted by the spec. Figure 5. The trace-checking workflow. Diagram showing the trace-checking workflow. It starts top left with a JavaScript test which runs through the nodes. This then flows into the log files and then into the combined log. From there, through TLA+ generator, it flows to the trace.tla. This connects to the TLC model checking, which then provides a pass or fail result. The MongoDB server team has hundreds of integration tests handwritten in JavaScript, from which we chose about 300 for this experiment. We also have randomized tests; we chose one called the "rollback fuzzer" which does random CRUD operations while randomly creating and healing network partitions, causing uncommitted writes to be logged and rolled back. We added tracing code to the MongoDB server and ran each test with a three-node replica set. Since all server processes ran on one machine and communicated over localhost, we didn't worry about clock synchronization: we just merged the three logs, sorting by timestamp. We wrote a Python script to read the combined log and convert it into a giant TLA+ spec named Trace.tla with a sequence of states for the whole three-server system. Trace.tla asserted only one property: "This behavior conforms to RaftMongo.tla." Here's some more detail about the Python script. At each moment during the test, the system has some state V, which is the values of the state variables for each node. The script tries to reconstruct all the changes to V and record them in Trace.tla. It begins by setting V to a hardcoded initial state V0, and outputs it as the first state of the sequence: \* Each TLA+ tuple is \* <> \* We know the first state: all nodes are followers with empty logs. Trace == << <<"Init", \* action name <<"Follower","Follower","Follower">>, \* role per node <<1, 1, 1>>, \* commitPoint per node <<<<...>>,<<...>>,<<...>>>>, \* log per node "">>, \* trace log location (empty) \* ... more states will follow ... The script reads events from the combined log and updates V. Here's an example where Node 1 was the leader in state Vi, then Node 2 logs that it became leader. The script combines these to produce Vi+1 where Node 2 is the leader and Node 1 is now a follower. Note, this is a lie. Node 1 didn't actually become a follower in the same instant Node 2 became leader. Foreshadowing! This will be a problem for Judah and me. Figure 6. Constructing the next state from a trace event. Image of three tables that breakdown the construction of the next state from a trace event. Anyway, the Python script appends a state to the sequence in Trace.tla: Trace == << \* ... thousands of events ... <<"BecomePrimary", \* action name for debugging <<"Follower","Leader","Follower">>, \* role per node <<1, 1, 1>>, \* commitPoint per node <<<<...>>,<<...>>,<<...>>>>, \* log per node \* trace log location, for debugging: "/home/emptysquare/RollbackFuzzer/node2.log:12345">>, \* ... thousands more events ... >> We used the Python script to generate a Trace.tla file for each of the hundreds of tests we'd selected: handwritten JavaScript tests and the randomized "rollback fuzzer" test. Now we wanted to use the model-checker to check that this state sequence was permitted by our TLA+ spec, so we know our C++ code behaved in a way that conforms to the spec. Following a technique published by Ron Pressler, we added these lines to each Trace.tla: VARIABLES log, role, commitPoint \* Instantiate our hand-written spec, RaftMongo.tla. Model == INSTANCE RaftMongo VARIABLE i \* the trace index \* Load one trace event. Read == /\ log = Trace[i][4] /\ role = Trace[i][5] /\ commitPoint = Trace[i][6] ReadNext == /\ log' = Trace[i'][4] /\ role' = Trace[i'][5] /\ commitPoint' = Trace[i'][6] Init == i = 1 /\ Read Next == \/ i < Len(Trace) /\ i' = i + 1 /\ ReadNext \/ UNCHANGED <> \* So that we don't get a deadlock error in TLC TraceBehavior == Init /\ [][Next]_<> \* To verify, we check the spec TraceBehavior in TLC, with Model!SpecBehavior \* as a temporal property. We run the standard TLA+ model-checker ("TLC"), which tells us if this trace is an allowed behavior in RaftMongo.tla. But this whole experiment failed. Our traces never matched our specification. We didn't reach our goal, but we learned three lessons that could help future engineers. What disappointment taught us Lesson one: It's hard to snapshot a multithreaded program's state. Each time a MongoDB node executes a state transition, it has to snapshot its state variables in order to log them. MongoDB is highly concurrent with fairly complex locking within each process--it was built to avoid global locking. It took us a month to figure out how to instrument MongoDB to get a consistent snapshot of all these values at one moment. We burned most of our budget for the experiment, and we worried we'd changed MongoDB too much (on a branch) to test it realistically. The 2024 paper "Validating Traces of Distributed Programs Against TLA+ Specifications" describes how to do trace-checking when you can only log some of the values (see my summary at the bottom of this page). We were aware of this option back in 2020, and we worried it would make trace-checking too permissive; it wouldn't catch every bug. Lesson two: The implementation must actually conform to the spec. This is obvious to me now. After all, conformance checking was the point of the project. In our real-life implementation, when an old leader votes for a new one, first the old leader steps down, then the new leader steps up. The spec we chose for trace-checking wasn't focused on the election protocol, though, so for simplicity, the spec assumed these two actions happened at once. (Remember I said a few paragraphs ago, "This is a lie"?) Judah and I knew about this discrepancy--we'd deliberately made this simplification in the spec. We tried to paper over the difference with some post-processing in our Python script, but it never worked. By the end of the project, we decided we should have backtracked, making our spec much more complex and realistic, but we'd run out of time. The eXtreme Modelling methodology says we should write the spec just before the implementation. But our spec was written long after most of the implementation, and it was highly abstract. I can imagine another world where we knew about eXtreme Modelling and TLA+ at the start, when we began coding MongoDB. In that world, we wrote our spec before the implementation, with trace-checking in mind. The spec and implementation would've been structured similarly, and this would all have been much easier. Lesson three: Trace-checking should extend easily to multiple specs. Judah and I put in 10 weeks of effort without successfully trace-checking one spec, and most of the work was specific to that spec, RaftMongo.tla. Sure, we learned general lessons (you're reading some of them) and wrote some general code, but even if we'd gotten trace-checking to work for one spec we'd be practically starting over with the next spec. Our original vision was to gather execution traces from all our tests, and trace-check them against all of our specifications, on every git commit. We estimated that the marginal cost of implementing trace-checking for more specs wasn't worth the marginal value, so we stopped the project. Practical trace-checking If we started again, we'd do it differently. We'd ensure the spec and implementation conform at the start, and we'd fix discrepancies by fixing the spec or the implementation right away. We'd model easily observed events like network messages, to avoid snapshotting the internal state of a multithreaded process. I still think trace-checking is worthwhile. I know it's worked for other projects. In fact MongoDB is sponsoring a grad student Finn Hackett, whom I'm mentoring, to continue trace-checking research. Let's move on to the second half of our project. Test-case generation for MongoDB Mobile SDK The MongoDB Mobile SDK is a database for mobile devices that syncs with a central server (since we wrote the paper, MongoDB has sunsetted the product). Mobile clients can make changes locally. These changes are periodically uploaded to the server and downloaded by other clients. The clients and the server all use the same algorithm to resolve write conflicts: Operational Transformation, or OT. Max wanted to test that the clients and server implement OT correctly, meaning they resolve conflicts the same way, eventually resulting in identical data everywhere. Originally, the clients and server shared one C++ implementation of OT, so we knew they implemented the same algorithm. But in 2020, we'd recently rewritten the server in Go, so testing their conformance became urgent. Figure 7. MongoDB mobile SDK. Diagram showing how mobile C++ flows into and from the server Go. My colleague Max Hirschhorn used test-case generation to check conformance. This technique goes in the opposite direction from trace-checking: trace-checking starts with an implementation and checks that its behaviors are allowed by the spec, but test-case generation starts with a spec and checks that its behaviors are in the implementation. But first, we needed a TLA+ spec. Before this project, the mobile team had written out the OT algorithm in English and implemented it in C++. Max manually translated the algorithm from C++ to TLA+. In the mobile SDK, clients can do 19 kinds of operations on data; six of these can be performed on arrays, resulting in 21 array merge rules, which are implemented in about 1000 lines of C++. Those 21 rules are the most complex, and Max focused his specification there. He used the model-checker to verify that his TLA+ spec ensured all participants eventually had the same data. This translation was a gruelling job, but the model-checker caught Max's mistakes quickly, and he finished in two weeks. There was one kind of write conflict that crashed the model-checker: if one participant swapped two array elements, and another moved an element, then the model-checker crashed with a Java StackOverflowError. Surprisingly, this was an actual infinite-recursion bug in the algorithm. Max verified that the bug was in the C++ code. It had hidden there until he faithfully transcribed it into TLA+ and discovered it with the model-checker. He disabled the element-swap operation in his TLA+ spec, and the mobile team deprecated it in their implementation. To test conformance, Max used the model-checker to output the entire state graph for the spec. He constrained the algorithm to three participants, all editing a three-element array, each executing one (possibly conflicting) write operation. With these constraints, the state space is a DAG, with a finite number of behaviors (paths from an initial state to a final state). There are 30,184 states and 4913 behaviors. Max wrote a Go program to parse the model-checker's output and write out a C++ unit test for each behavior. Here's an example unit test. (It's edited down from three participants to two.) At the start, there's an array containing {1, 2, 3}. One client sets the third element of an array to 4 and the second client removes the second element from the array. The test asserts that both clients agree the final array is {1, 4}. TEST(Transform_Array) { size_t num_clients = 2; TransformArrayFixture fixture{test_context, num_clients, {1, 2, 3}}; fixture.transaction(0, [](TableRef array) { array->set_int(0, 2, 4); }); fixture.transaction(1, [](TableRef array) { array->remove(1); }); fixture.sync_all_clients(); fixture.check_array({1, 4}); fixture.check_ops(0, {ArrayErase{1}}); fixture.check_ops(1, {ArraySet{1, 4}}); } These 4913 tests immediately achieved 100% branch coverage of the implementation, which we hadn't accomplished with our handwritten tests (21%) or millions of executions with the AFL fuzzer (92%). Retrospective Max's test-case generation worked quite well. He discovered a bug in the algorithm, and he thoroughly checked that the mobile SDK's Operational Transformation code conforms to the spec. Judah's and my trace-checking experiment didn't work: our spec and code were too far apart, and adding tracing to MongoDB took too long. Both techniques can work, given the right circumstances and strategy. Both techniques can fail, too! We published our results and lessons as a paper in VLDB 2020, titled "eXtreme Modelling in Practice." In the subsequent five years, I've seen some progress in conformance checking techniques. Test-case generation: * Model Checking Guided Testing for Distributed Systems. The "Mocket" system generates tests from a TLA+ spec, and instruments Java code (with a fair amount of human labor) to force it to deterministically follow each test, and check that its variables have the same values as the spec after each action. The authors tested the conformance of three Java distributed systems and found some new bugs. Their technique is Java-specific but could be adapted for other languages. * Multi-Grained Specifications for Distributed System Model Checking and Verification. The authors wrote several new TLA+ specs of Zookeeper, at higher and lower levels of abstraction. They checked conformance between the most concrete specs and the implementation, with a technique similar to Mocket: a human programmer instruments some Java code to map Java variables to spec variables, and to make all interleavings deterministic. The model-checker randomly explores spec behaviors, while the test framework checks that the Java code can follow the same behaviors. * SandTable: Scalable Distributed System Model Checking with Specification-Level State Exploration. This system is not language-specific: it overrides system calls to control nondeterminism and force the implementation to follow each behavior of the spec. It samples the spec's state space to maximize branch coverage and event diversity while minimizing the length of each behavior. As in the "Multi-Grained" paper, the SandTable authors wisely developed new TLA+ specs that closely matched the implementations they were testing, rather than trying to use existing, overly abstract specs like Judah and I did. * Plus, my colleagues Will Schultz and Murat Demirbas are publishing a paper in VLDB 2025 that uses test-case generation with a new TLA+ spec of MongoDB's WiredTiger storage layer, the paper is titled "Design and Modular Verification of Distributed Transactions in MongoDB." Trace-checking: * Protocol Conformance with Choreographic PlusCal. The authors write new specs in an extremely high-level language that compiles to TLA+. From their specs they generate Go functions for trace-logging, which they manually add to existing Go programs. They check that the resulting traces are valid spec behaviors and find some bugs. * Validating Traces of Distributed Programs Against TLA+ Specifications. Some veteran TLA+ experts demonstrate in detail how to trace-log from a Java program and validate the traces with TLC, the TLA+ model-checker. They've written small libraries and added TLC features for convenience. This paper focuses on validating incomplete traces: if you can only log some of the variables, TLC will infer the rest. * Smart Casual Verification of the Confidential Consortium Framework. The authors started with an existing implementation of a secure consensus protocol. Their situation was like mine in 2020 (new specs of a big old C++ program) and so was their goal: to continuously check conformance and keep the spec and implementation in sync. Using the new TLC features announced in the "Validating Traces" paper above, they toiled for months, brought their specs and code into line, found some bugs, and realized the eXtreme Modelling vision. * Finn Hackett is a PhD student I'm mentoring, he's developed a TLA+-to-Go compiler. He's now prototyping a trace-checker to verify that the Go code he produces really conforms to its source spec. We're doing a summer project together with Antithesis to thoroughly conformance-check the implementation's state space. I'm excited to see growing interest in conformance checking, because I think it's a serious problem that needs to be solved before TLA+ goes mainstream. The "Validating Traces" paper announced some new trace-checking features in TLC, and TLC's developers are discussing a better way to export a state graph for test-case generation. I hope these research prototypes lead to standard tools, so engineers can keep their code and specs in sync. Join our MongoDB Community to learn about upcoming events, hear stories from MongoDB users, and connect with community members from around the world. - Previous Mongoose Now Natively Supports QE and CSFLE Mongoose 8.15.0 has been released, which adds support for the industry-leading encryption solutions available from MongoDB. With this update, it's simpler than ever to create documents leveraging MongoDB Queryable Encryption (QE) and Client-Side Level Field Encryption (CSFLE), keeping your data secure when it is in use. Read on to learn more about approaches to encrypting your data when building with MongoDB and Mongoose. What is Mongoose? Mongoose is a library that enables elegant object modeling for Node.js applications working with MongoDB. Similar to an Object-Relational Mapper (ORM), the Mongoose Object Document Mapper (ODM) simplifies programmatic data interaction through schemas and models. It allows developers to define data structures with validation and provides a rich API for CRUD operations, abstracting away many of the complexities of the underlying MongoDB driver. This integration enhances productivity by enabling developers to work with JavaScript objects instead of raw database queries, making it easier to manage data relationships and enforce data integrity. What is QE and CSFLE? Securing sensitive data is paramount. It must be protected at every stage--whether in transit, at rest, or in use. However, implementing in-use encryption can be complex. MongoDB offers two approaches to make it easier: Queryable Encryption (QE) and Client-Side Level Field Encryption (CSFLE). QE allows customers to encrypt sensitive application data, store it securely in an encrypted state in the MongoDB database, and perform equality and range queries directly on the encrypted data. An industry-first innovation, QE eliminates the need for costly custom encryption solutions, complex third-party tools, or specialized cryptography knowledge. It employs a unique structured encryption schema, developed by the MongoDB Cryptography Research Group , that simplifies the encryption of sensitive data while enabling equality and range queries to be performed directly on data without having to decrypt it. The data remains encrypted at all stages, with decryption occurring only on the client side. This architecture supports solidified strict access controls, where MongoDB and even an organization's own database administrators (DBAs) don't have access to sensitive data. This design enhances security by keeping the server unaware of the data it processes, further mitigating the risk of exposure and minimizing the potential for unauthorized access. Adding QE/CSFLE auto-encryption support for Mongoose The primary goal of the Mongoose integration with QE and CSFLE is to provide idiomatic support for automatic encryption, simplifying the process of creating encrypted models. With native support for QE and CSFLE, Mongoose allows developers to define encryption options directly within their schemas without the need for separate configurations. This first-class API enables developers to work within Mongoose without dropping down to the driver level, minimizing the need for significant code changes when adopting QE and CSFLE. Mongoose streamlines configuration by automatically generating the encrypted field map. This ensures that encrypted fields align perfectly with the schema and simplifies the three-step process typically associated with encryption setup, shown below. Mongoose also keeps the schema and encrypted fields in sync, reducing the risk of mismatches. Developers can easily declare fields with the encrypt property and configure encryption settings, using all field types and encryption schemes supported by QE and CSFLE. Additionally, users can manage their own encryption keys, enhancing control over their encryption processes. This comprehensive approach empowers developers to implement robust encryption effortlessly while maintaining operational efficiency. Pre-integration experience const kmsProviders = { local: { key: Buffer.alloc(96) }; const keyVaultNamespace = 'data.keys'; const extraOptions = {}; const encryptedDatabaseName = 'encrypted'; const uri = ''; const encryptedFieldsMap = { 'encrypted.patent': { encryptedFields: EJSON.parse('', { relaxed: false }), } }; const autoEncryptionOptions = { keyVaultNamespace, kmsProviders, extraOptions, encryptedFieldsMap }; const schema = new Schema({ patientName: String, patientId: Number, field: String, patientRecord: { ssn: String, billing: String } }, { collection: 'patent' }); const connection = await createConnection(uri, { dbName: encryptedDatabaseName, autoEncryption: autoEncryptionOptions, autoCreate: false, // If using createEncryptedCollection, this is false. If manually creating the keyIds for each field, this is true. }).asPromise(); const PatentModel = connection.model('Patent', schema); const result = await PatentModel.find({}).exec(); console.log(result); This example demonstrates the manual configuration required to set up a Mongoose model for QE and CSFLE, requiring three different steps to: Define an encryptedFieldsMap to specify which fields to encrypt Configure autoEncryptionOptions with key management settings Create a Mongoose connection that incorporates these options This process can be cumbersome, as it requires explicit setup for encryption. New experience with Mongoose 8.15.0 const schema = new Schema({ patientName: String, patientId: Number, field: String, patientRecord: { ssn: { type: String, encrypt: { keyId: '', queries: 'equality' } }, billing: { type: String, encrypt: { keyId: '', queries: 'equality' } }, } }, { encryptionType: 'queryableEncryption', collection: 'patent' }); const connection = mongoose.createConnection (); const PatentModel = connection.model('Patent', schema); const keyVaultNamespace = 'client.encryption'; const kmsProviders = { local: { key: Buffer.alloc(96) }; const uri = ''; const keyVaultNamespace = 'data.keys'; const autoEncryptionOptions = { keyVaultNamespace, kmsProviders, extraOptions: {} }; await connection.openUri(uri, { autoEncryption: autoEncryptionOptions}); const result = await PatentModel.find({}).exec(); console.log (result); This "after experience" example showcases how the integration of QE and CSFLE into Mongoose simplifies the encryption setup process. Instead of the previous three-step approach, developers can now define encryption directly within the schema. In this implementation, fields like ssn and billing are marked with an encrypt property, allowing for straightforward configuration of encryption settings, including the keyId and query types. The connection to the database is established with a single call that includes the necessary auto-encryption options, eliminating the need for a separate encrypted fields map and complex configurations. This streamlined approach enables developers to work natively within Mongoose, enhancing usability and reducing setup complexity while maintaining robust encryption capabilities. Learn more about QE/CSFLE for Mongoose We're excited for you to build secure applications with QE/CSFLE for Mongoose. Here are some resources to get started with: Learn how to set up use Mongoose with MongoDB through our tutorial. Check out our documentation to learn when to choose QE vs. CSFLE . Read Mongoose CSFLE documentation . June 2, 2025 Next - Luna AI and MongoDB Throw Lifeline to Product Teams Product and engineering leaders face a constant battle: making crucial real-time decisions amidst a sea of fragmented, reactive, and disconnected progress data. The old ways--chasing updates, endlessly pinging teams on Slack, digging through Jira, and enduring endless status meetings--simply aren't cutting it. This struggle leaves product and engineering leads wasting precious hours on manual updates, while critical risks silently slip through the cracks. This crucial challenge is precisely what Luna AI , powered by its robust partnership with MongoDB , is designed to overcome. Introducing Luna AI: Your intelligent program manager Luna AI was founded to tackle this exact problem, empowering product and engineering leaders with the visibility and context they need, without burying their PMs in busy work. Imagine having an AI program manager dedicated to giving you clear insights into goals, roadmap ROI, initiative progress, and potential risks throughout the entire product lifecycle. Luna AI makes this a reality by intelligently summarizing data from your existing tools like Jira and Slack. It can even automatically generate launch and objective and key result (OKR) status updates, create your roadmap, and analyze your Jira sprints, drastically reducing the need for manual busywork. From concept to command center: The evolution of Luna AI Luna AI's Co-founder, Paul Debahy, a seasoned product leader with experience at Google, personally felt the pain of fragmented data during his time as a CPO. Inspired by Google's internal LaunchCal, which provided visibility into upcoming launches, Luna AI initially began as a launch management tool. However, a key realization quickly emerged: Customers primarily needed help "managing up." This insight led to a pivotal shift, focusing Luna AI on vertical management--communicating status, linking execution to strategy, and empowering leaders, especially product leaders, to drive decisions. Today, Luna AI has evolved into a sophisticated AI-driven insights platform. Deep Jira integration and advanced LLM modules have transformed it from a simple tracker into a strategic visibility layer. Luna AI now provides essential capabilities like OKR tracking, risk detection, resource and cost analysis, and smart status summaries. Luna AI believes product leadership is increasingly strategic, aiming to be the system of record for outcomes, not just tasks. Its mission: to be everyone's AI program manager, delivering critical strategy and execution insights for smarter decision-making. The power under the hood: Building with MongoDB Atlas Luna AI's robust technology stack includes Node.js, Angular, and the latest AI/LLM models. Its infrastructure leverages Google Cloud and, crucially, MongoDB Atlas as its primary database. When selecting a data platform, Luna AI prioritized flexibility, rapid iteration, scalability, and security. Given the dynamic, semi-structured data ingested from diverse sources like Jira, Slack, and even meeting notes, a platform that could handle this complexity was essential. Key requirements included seamless tenant separation, robust encryption, and minimal operational overhead. MongoDB proved to be the perfect fit for several reasons. The developer-friendly experience was a major factor, as was the flexible schema of its document database, which naturally accommodated Luna AI's complex and evolving data model. This flexibility was vital for tracking diverse information such as Jira issues, OKRs, AI summaries, and Slack insights, enabling quick adaptation and iteration. MongoDB also offered effortless support for the startup's multi-tenant architecture. Scaling with MongoDB Atlas has been smooth and fast, according to Luna AI. Atlas effortlessly scaled as the company added features and onboarded workspaces ranging from startups to enterprises. The monitoring dashboard has been invaluable, offering insights that helped identify performance bottlenecks early. In fact, index suggestions from the dashboard directly led to significant improvements to speed. Debahy even remarked, "Atlas's built-in insights make it feel like we have a DB ops engineer on the team." Luna AI relies heavily on Atlas's global clusters and automated scaling . The monitoring and alerting features provide crucial peace of mind, especially during launches or data-intensive tasks like Jira AI epic and sprint summarization. The monitoring dashboard was instrumental in resolving high-latency collections by recommending the right indexes. Furthermore, in-house backups are simple, fast, and reliable, with painless restores offering peace of mind. Migrating from serverless to dedicated instances was seamless and downtime-free. Dedicated multi-tenant support allows for unlimited, isolated databases per customer. Auto-scaling is plug-and-play, with Atlas handling scaling across all environments. Security features like data-at-rest encryption and easy access restriction management per environment are also vital benefits. The support team has consistently been quick, responsive, and proactive. A game-changer for startups: The MongoDB for Startups program Operating on a tight budget as a bootstrapped and angel-funded startup, Luna AI found the MongoDB for Startups program to be a true game changer. It stands out as one of the most founder-friendly programs the company has encountered. The Atlas credits completely covered the database costs, empowering the team to test, experiment, and even make mistakes without financial pressure. This freedom allowed them to scale without worrying about database expenses or meticulously tracking every compute and resource expenditure. Access to technical advisors and support was equally crucial, helping Luna AI swiftly resolve issues ranging from load management to architectural decisions and aiding in designing a robust data model from the outset. The program also opened doors to a valuable startup community, fostering connections and feedback. Luna AI's vision: The future of product leadership Looking ahead, Luna AI is focused on two key areas: Building a smarter, more contextual insights layer for strategy and execution. Creating a stakeholder visibility layer that requires no busy work from product managers. Upcoming improvements include predictive risk alerts spanning Jira, Slack, and meeting notes. They are also developing ROI-based roadmap planning and prioritization, smart AI executive status updates, deeper OKR traceability, and ROI-driven tradeoff analysis. Luna AI firmly believes that the role of product leadership is becoming increasingly strategic. With the support of programs like MongoDB for Startups, they are excited to build a future where Luna AI is the definitive system of record for outcomes. Ready to empower your product team? Discover how Luna AI helps product teams thrive. Join the MongoDB for Startups program to start building faster and scaling further with MongoDB! June 3, 2025