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 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}. The bold parts are specific to this generated test. The rest of the code is the same for all tests. 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 MongoDB Atlas Stream Processing Now Supports Session Windows! We're excited to announce that MongoDB Atlas Stream Processing now supports Session Windows ! This powerful feature lets you build streaming pipelines that analyze and process related events that occur together over time, grouping them into meaningful sessions based on periods of activity. For instance, you can now track all of a customer's interactions during a shopping journey, treating it as a single session that ends when they're inactive for a specified period of time. Whether you're analyzing user behavior, monitoring IoT device activities, or tracking system operations, Atlas Stream Processing's Session Windows make it easy to transform your continuous data streams into actionable insight, and make the data available wherever you need to use it. What are Session Windows? Session Windows are a powerful way to analyze naturally occurring activity patterns in your data by grouping related events that happen close together in time. Think of how users interact with websites or apps--they tend to be active for a period, then take breaks, then return for another burst of activity. Session Windows automatically detect these patterns by identifying gaps in activity, allowing you to perform aggregations and transformations on these meaningful periods of activity. As an example, imagine you're an e-commerce company looking to better understand what your customers do during each browsing session to help improve conversions. With Atlas Stream Processing, you can build a pipeline that: Collects all the product pages a user visits during their browsing session Records the name, category, and price of each item viewed, plus whether items were added to a cart Automatically considers a session complete after 15 minutes of user inactivity Sends the session data to cloud storage to improve recommendation engines With this pipeline, you provide your recommendation engine with ready-to-use data about your user sessions to improve your recommendations in real time. Unlike fixed time-based windows ( tumbling or hopping ), Session Windows adapt dynamically to each user's behavior patterns. How does it work? Session Windows work similarly to the hopping and tumbling windows Atlas Stream Processing already supports, but with a critical difference: while those windows open and close on fixed time intervals, Session Windows dynamically adjust based on activity patterns. To implement a Session Window, you specify three required components: partitionBy : This is the field or fields that group your records into separate sessions. For instance, if tracking user sessions, use unique user IDs to ensure each user's activity is processed separately. gap : This is the period of inactivity that signals the end of a session. For instance, in the above example, we consider a user's session complete when they go 15 minutes without clicking on a link in the website or app. pipeline : These are the operations you want to perform on each session's data. This may include counting the number of pages a user visited, recording the page they spent the most time on, or noting which pages were visited multiple times. You then add this Session Window stage to your streaming aggregation pipeline, and Atlas Stream Processing continuously processes your incoming data, groups events into sessions based on your configuration, and applies your specified transformations. The results flow to your designated output destinations in real-time, ready for analysis or to trigger automated actions. A quick example Let's say you want to build the pipeline that we mentioned above to track user sessions, notify them if they have items in their cart but haven't checked out, and move their data downstream for analytics. You might do something like this: 1. Configure your source and sink stages This is where you define the connections to any MongoDB or external location you intend to receive data from (source) or send data to (sink). // Set your source to be change streams from the pageViews, cartItems, and orderedItems collections let sourceCollections = { $source: { connectionName: "ecommerce", "db": "customerActivity", "coll": ["pageViews", "cartItems", "orderedItems"] } } // Set your destination (sink) to be the userSessions topic your recommendation engine consumes data from let emitToRecommendationEngine = { $emit: { connectionName: "recommendationEngine", topic: "userSessions", } }; // Create a connection to your sendCheckoutReminder Lambda function that sends a reminder to users to check out if they have items in their cart when the session ends let sendReminderIfNeeded = { $externalFunction: { "connectionName": "operations", "as": "sendCheckoutReminder", "functionName": "arn:aws:lambda:us-east-1:123412341234:function:sendCheckoutReminder" } } 2. Define your Session Window logic This is where you specify how data will be transformed in your stream processing pipeline. // Step 1. Create a stage that pulls only the fields you care about from the change logs. // Every document will have a userId and itemId as all collections share that field. Fields not present will be null. let extractRelevantFields = { $project: { userId: "$fullDocument.userId", itemId: "$fullDocument.itemId", category: "$fullDocument.category", cost: "$fullDocument.cost", viewedAt: "$fullDocument.viewedAt", addedToCartAt: "$fullDocument.addedToCartAt", purchasedAt: "$fullDocument.purchasedAt" } }; // Step 2. By setting _id to $userId this group all the documents by the userId. Fields not present in any records will be null. let groupSessionData = { $group: { _id: "$userId", itemIds: { $addToSet: "$itemId" }, categories: { $addToSet: "$category" }, costs: { $addToSet: "$cost" }, viewedAt: { $addToSet: "$viewedAt" }, addedToCartAt: { $addToSet: "$addedToCartAt" }, purchasedAt: { $addToSet: "$purchasedAt" } } }; / / Step 3. Create a session window that closes after 15 minutes of inactivity. The pipeline specifies all operations to be performed on documents sharing the same userId within the window. let createSession = { $sessionWindow: { partitionBy: "$_id", gap: { unit: "minute", size: 15}, pipeline: [ groupSessionData ] }}; 3. Create and start your stream processor The last step is simple: create and start your stream processor. // Create your pipeline array. The session data will be sent to the external function defined in sendReminderIfNeeded, and then it will be emitted to the recommendation engine Kafka topic. finalPipeline = [ sourceCollections, extractRelevantFields, createSession, sendReminderIfNeeded, emitToUserSessionTopic ]; // Create your stream processor sp.createStreamProcessor("userSessions", finalPipeline) // Start your stream processor sp.userSessions.start() And that's it! Your stream processor now runs continuously in the background with no additional management required. As users navigate your e-commerce website, add items to their carts, and make purchases, Atlas Stream Processing automatically: Tracks each user's activity in real-time Groups events into meaningful sessions based on natural usage patterns Closes sessions after your specified period of inactivity (15 minutes) Triggers reminders for users with abandoned carts Delivers comprehensive session data to your analytics systems All of this happens automatically at scale without requiring ongoing maintenance or manual intervention. Session Windows provide powerful, activity-based data processing that adapts to users' behavioral patterns rather than forcing their actions into arbitrary time buckets. Ready to get started? Log in or sign up for Atlas today to create stream processors. You can learn more about Session Windows or get started using our tutorial . May 29, 2025 Next - 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