This paper (NSDI'25) applies lightweight formal methods (hence the pun "smart casual" in contrast to formal attire) to the Confidential Consortium Framework (CCF). CCF is an open-source platform for trustworthy cloud applications, used in Microsoft's Azure Confidential Ledger service. The authors combine formal specification, model checking, and automated testing to validate CCF's distributed protocols, specifically its custom consensus protocol.

Background

CCF uses trusted execution environments (TEEs) and state machine replication. Its consensus protocol is based on Raft but has major modifications: signature transactions (Merkle tree root over the whole log  signed by the leader), optimistic acknowledgments, and partition leader step-down. CCF also avoids RPCs, using a uni-directional messaging layer. These changes add complexity, requiring formal verification. At the time of writing, CCF's implementation spans 63 kLoC in C++.

The authors define five requirements for CCF verification: verifying safety properties, documenting system behavior, increasing confidence in implementation, integrating with the codebase, and evolving with the system. They use TLA+ for formal specification and model checking. TLA+ specifies system behavior using temporal logic, verifying safety and liveness properties via model checking and simulation. However, verifying the protocol does not guarantee the implementation conforms to it.

Bridging this gap requires conformance checking, which can be done in two ways: test-case generation from the spec or trace validation of the implementation. MongoDB's VLDB'20 paper titled "eXtreme Modelling in Practice" explored both approaches, and is worth a look. The last four years brought significant progress in the applicability of both methods. I think deterministic simulations getting mature and gaining popularity helped both approaches.  

Ok, the first approach, test-case generation, uses spec executions to create tests, which are then run against the implementation. Conformance is verified by comparing the implementation's results to those of the spec. This approach requires a highly controllable and observable implementation, effectively eliminating all non-determinism. This is most applicable and effective for single-node implementation components. Recently, at MongoDB Research, we leveraged our distributed transactions specs to generate test cases for the WiredTiger storage component testing. This compositional spec work, led by Will Schultz, will be submitted for publication soon.

This current Microsoft paper focuses on the second approach, trace validation, which works in reverse. It begins with an implementation trace and verifies whether that trace is permitted by a spec execution. This method presents its own challenges, often requiring the spec to be sufficiently detailed to align with the implementation. Consequently, it typically necessitates a "medium-level" spec rather than a more abstract, high-level one.

Distributed Consensus Specification

The TLA+ consensus specification models CCF's protocol with 17 actions and 13 variables. (TLA+ specifications from the project are available on GitHub.) The authors extend the spec for simulation and model checking to explore a wide range of behaviors. Simulation weights actions to increase coverage of rare but critical scenarios.

Trace validation checks if implementation traces match the system’s specification. Since collecting traces from a live production distributed system is difficult, the authors use traces from existing CCF tests. CCF had extensive unit, functional, and end-to-end tests before this work. Consensus testing used a scenario driver that serialized execution deterministically and mocked unrelated components, allowing controlled network faults and observability.

Trace validation verifies whether the behaviors in a trace (T) intersect with those allowed by the spec (S), ensuring T ∩ S ≠ ∅. TLC (TLA's explicit state model checker) constructs S, but cannot generate T from a trace. To address this, the authors wrote a new TLA+ spec, "Trace," reusing the spec actions but constraining them to observed events. The actions are only enabled iff the current event in the trace matches an action, and the actions are parameterized by the values taken from the trace.

The paper reports that aligning spec actions with trace events was still challenging and they had to address granularity mismatches. Invalid traces could still result from incorrect logging, faulty mappings, or genuine spec-implementation mismatches. Unlike model checking, failed validation provided no counterexample, but behaviors in T helped diagnose the issue.

State-space explosion made validating traces computationally expensive. To address this, the authors used depth-first search (DFS) in TLC instead of breadth-first search (BFS). This significantly improving performance. For example, validating a consistency trace took under a second with DFS, compared to an hour with BFS.

Client Consistency Specification

The client consistency spec models interactions between clients and CCF, verifying guarantees like linearizability for read-write transactions and serializability for read-only transactions. TLA+ formalizes these guarantees, and trace validation ensures the implementation adheres to them. This process mirrored the distributed consensus verification effort, so details are omitted. After seeing the method applied to consensus, CCF engineers applied the method themselves with minimal involvement from formal methods specialists. The effort took about one engineer-week spread over two weeks.

Here's a bug they found: Linearizability requires transaction execution to respect real-time ordering. The OBSERVEDROINV property states that committed read-only transactions must reflect all prior committed read-write transactions. Model checking found a 12-step counterexample in four seconds: a read-only transaction was processed by an old but active leader that had not logged recent write transactions from the new leader. This scenario requires a falsely replaced leader still handling requests before retiring. They chose not to change the behavior, as serializability suffices for most applications, but the spec helps clarify guarantees for developers.

Here is an interactive exploration of this bug using the Spectacle (nee tla-web) tool. (For some reason, the trace exploration works only after you press "Reset" first.)

Results

The verification process found bugs in election quorum tallying, commit index advancement, and premature node retirement. These bugs were detected through model checking, simulation, and trace validation. Table 2 lists the most serious consensus protocol bugs found. These affected both safety and liveness and were detected at various verification stages.

One notable bug is the Commit advance on AE-NACK. The spec required a leader’s matchIndex to remain unchanged after receiving an AE-NACK, but the implementation allowed it to decrease. This came from aggressively applying an optimization from the Raft paper. A one-line code change aligned the spec with the implementation, but subsequent simulation found a 34-state counterexample violating a key correctness property. Manual translation of this counterexample into a 150 LoC functional test confirmed that the implementation could advance its commit index incorrectly. Further refinement of the spec revealed that matchIndex should never decrease except after leader elections. Adding this property allowed model checking to find a shorter counterexample. The authors report that the combination of functional testing and model checking allowed a quick and confident fix.

Many bugs were first identified during spec development and alignment with the implementation. Writing the consensus and consistency specs forced deeper thinking about protocol invariants. This process also enabled bug discoveries that would have been difficult to confirm otherwise, especially in complex reconfiguration and failure-handling scenarios.

This is a response to some of the feedback I received from the Postgres community about my recent benchmark results for vector indexes using MariaDB and Postgres (pgvector). The work here isn't sponsored and required ~2 weeks days of server time and a few more hours of my time (yes, I contribute to the PG community).

tl;dr

• index create is ~4X faster when using ~4 parallel workers. I hope that parallel DDL comes to more open source DBMS.
• parallel query does not help pgvector
• increasing work_mem does not help pgvector
• pgvector gets less QPS than MariaDB because it uses more CPU to compute the distance metric

Submitted to the Department of State, which is requesting comments on a proposed change which would align US passport gender markers with executive order 14168.

Executive order 14168 is biologically incoherent and socially cruel. All passport applicants should be allowed to select whatever gender markers they feel best fit, including M, F, or X.

In humans, neither sex nor gender is binary at any level. There are several possible arrangements of sex chromosomes: X, XX, XY, XXY, XYY, XXX, tetrasomies, pentasomies, etc. A single person can contain a mosaic of cells with different genetics: some XX, some XYY. Chromosomes may not align with genitalia: people with XY chromosomes may have a vulva and internal testes. People with XY chromosomes and a small penis may be surgically and socially reassigned female at birth—and never told what happened. None of these biological dimensions necessarily align with one’s internal concept of gender, or one’s social presentation.

The executive order has no idea how biology works. It defines “female” as “a person belonging, at conception, to the sex that produces the large reproductive cell”. Zygotes do not produce reproductive cells at all: under this order none of us have a sex. Oogenesis doesn’t start until over a month into embryo development. Even if people were karyotyping their zygotes immediately after conception so they could tell what “legal” sex they were going to be, they could be wrong: which gametes we produce depends on the formation of the genital ridge.

All this is to say that if people fill out these forms using this definition of sex, they’re guessing at a question which is both impossible to answer and socially irrelevant. You might be one of the roughly two percent of humans born with an uncommon sexual development and not even know it. Moreover, the proposed change fundamentally asks the wrong question: gender markers on passports are used by border control agents, and are expected to align with how those agents read the passport holder’s gender. A mismatch will create needless intimidation and hardship for travelers.

Of course most of us will not have our identities challenged under this order. That animus is reserved for trans people, for gender-non-conforming people, for anyone whose genetics, body, dress, voice, or mannerisms don’t quite fit the mold. Those are the people who will suffer under this order. That cruelty should be resisted.

Entrepreneurs think and act differently from managers and strategists.

This 2008 paper argues that entrepreneurs use effectual reasoning, the polar opposite of causal reasoning taught in business schools. Causal reasoning starts with a goal and finds the best way to achieve it. Effectual reasoning starts with available resources and lets goals emerge along the way. Entrepreneurs are explorers, not generals. Instead of following fixed plans, they experiment and adapt to seize whatever opportunities the world throws at them.

Consider this example from the paper. A causal thinker starts an Indian restaurant by following a fixed plan: researching the market, choosing a prime location, targeting the right customers, securing funding, and executing a well-designed strategy. The effectual entrepreneur doesn’t start with a set goal. She starts with what she has (her skills, knowledge, and network), and she experiments. She might begin by selling homemade lunches to friends’ coworkers. If that works, she expands. If not, she watches what excites her customers. Maybe they care less about the food and more about her cultural insights and life experiences. She doesn’t force the restaurant idea. She unasks the question and asks a new one: What do people really want from me? (This is what Airbnb did with its "Experiences". Instead of just renting out rooms, hosts began offering cooking classes, city tours, and adventures, things people didn’t know they wanted until they saw them.) 

Key principles of effectual reasoning

The author, Prof. Saras D. Sarasvathy, interviewed 30 seasoned entrepreneurs and identified key principles of effectual reasoning.

The first is affordable loss. Forget maximizing returns. Entrepreneurs focus on what they can afford to lose. Instead of wasting time on market research, they test ideas in the real world. They fail cheap, fail fast, and learn faster.

The second is partnerships over competition. Entrepreneurs don’t assume a market exists for their idea. They build networks of collaborators who help shape the business. This lowers risk, opens doors, and provides instant feedback. This contrasts with the corporate world, which focuses on outmaneuvering rivals.

The third is leveraging surprises. Managers hate surprises. Entrepreneurs love them. The unexpected isn’t an obstacle, it’s an opening. A pivot. A new market. A better business.

So, effectual reasoning flips traditional business thinking on its head. Most strategies assume that predicting the future gives control. Entrepreneurs believe the opposite: take action, and you shape the future. Rather than waiting for ideal conditions, they start with what they have and improvise.

Discussion

Here is what I make of this. Some people are born entrepreneurs. Maybe you can teach it. Maybe you can’t. Some minds thrive in uncertainty and make it up as they go. Others crave a plan, a map, a well-paved road. 

It’s the old fox-versus-hedgehog dilemma from Grand Strategy. The fox knows many things. The hedgehog knows one big thing.

A smart friend of mine (Mahesh Balakrishnan, who has a related Managing Skunks post here) put it perfectly. On his dream software team, he wants either Jeeps or Ferraris. Jeeps go anywhere. No roads, no directions—just point them at a problem, and they’ll tear through it. That’s effectual reasoning. Ferraris, on the other hand, need smooth roads and a clear destination. But once they have that, they move fast. He doesn’t want Toyota Corollas. Corollas are slow. Worse, they still need roads.

So here’s my corollary (admire my beautiful pun).

If you got to be a causal thinker, be a Ferrari. Not a Corolla.

Postamble

You can tell Steve Jobs is the textbook "effectual thinker" just from this quote.

“The thing I would say is, when you grow up, you tend to get told that the world is the way it is, and your life is just to live your life inside the world. Try not to bash into the walls too much. Try to have a nice family life, have fun, save a little money. But life, that's a very limited life. Life can be much broader once you discover one simple fact, and that is: Everything around you that you call life was made up by people that were no smarter than you. And you can change it. You can influence it. You can build your own things that other people can use. And the minute that you understand that you can poke life, and actually something will, you know, if you push in, something will pop out the other side, that you can change it. You can mold it. That's maybe the most important thing is to shake off this erroneous notion that life is there and you're just going to live in it, versus embrace it. Change it. Improve it. Make your mark upon it. I think that's very important. And however you learn that, once you learn it, you'll want to change life and make it better. Because it's kind of messed up in a lot of ways. Once you learn that, you'll never be the same again.”

sysbench is a great tool for benchmarks and I appreciate all of the work the maintainer (Alexey Kopytov) put into it as that is often a thankless task. Today I struggled to figure out how to load Lua scripts from something other than the default location that was determined when sysbench was compiled. It turns out that LUA_PATH is the thing to set, but the syntax isn't what I expected.

My first attempt was this, because the PATH in LUA_PATH implies directory names. But that failed.
  LUA_PATH="/mnt/data/sysbench.lua/lua" sysbench ... oltp_insert run

It turns out that LUA_PATH uses special semantics and this worked:
  LUA_PATH="/mnt/data/sysbench.lua/lua/?.lua" sysbench ... oltp_insert run

The usage above replaces the existing search path. The usage below prepends the new path to the existing (compiled in) path:

  LUA_PATH="/mnt/data/sysbench.lua/lua/?.lua;;" sysbench ... oltp_insert run

A few quick notes for other folks who are geoblocking the UK. I just set up a basic geoblock with Nginx on Debian. This is all stuff you can piece together, but the Maxmind and Nginx docs are a little vague about the details, so I figure it’s worth an actual writeup. My Nginx expertise is ~15 years out of date, so this might not be The Best Way to do things. YMMV.

First, register for a free MaxMind account; you’ll need this to subscribe to their GeoIP database. Then set up a daemon to maintain a copy of the lookup file locally, and Nginx’s GeoIP2 module:

apt install geoipupdate libnginx-mod-http-geoip2

Create a license key on the MaxMind site, and download a copy of the config file you’ll need. Drop that in /etc/GeoIP.conf. It’ll look like:

AccountID XXXX
LicenseKey XXXX
EditionIDs GeoLite2-Country

The package sets up a cron job automatically, but we should grab an initial copy of the file. This takes a couple minutes, and writes out /var/lib/GeoIP/GeoLite2-Country-mmdb:

geoipupdate

The GeoIP2 module should already be loaded via /etc/nginx/modules-enabled/50-mod-http-geoip2.conf. Add a new config snippet like /etc/nginx/conf.d/geoblock.conf. The first part tells Nginx where to find the GeoIP database file, and then extracts the two-letter ISO country code for each request as a variable. The map part sets up an $osa_geoblocked variable, which is set to 1 for GB, otherwise 0.

geoip2 /var/lib/GeoIP/GeoLite2-Country.mmdb {
  $geoip2_data_country_iso_code country iso_code;
}

map $geoip2_data_country_iso_code $osa_geoblocked {
  GB      1;
  default 0;
}

Write an HTML file somewhere like /var/www/custom_errors/osa.html, explaining the block. Then serve that page for HTTP 451 status codes: in /etc/nginx/sites-enabled/whatever, add:

server {
  ...
  # UK OSA error page
  error_page 451 /osa.html;
  location /osa.html {
    internal;
    root /var/www/custom_errors/;
  }

  # When geoblocked, return 451
  location / {
    if ($osa_geoblocked = 1) {
      return 451;
    }
  }
}

Test your config with nginx -t, and then service nginx reload. You can test how things look from the UK using a VPN service, or something like locabrowser.

This is, to be clear, a bad solution. MaxMind’s free database is not particularly precise, and in general IP lookup tables are chasing a moving target. I know for a fact that there are people in non-UK countries (like Ireland!) who have been inadvertently blocked by these lookup tables. Making those people use Tor or a VPN sucks, but I don’t know what else to do in the current regulatory environment.

I have been working on databases since 1996. In some cases I just worked on the product (Oracle & Informix), in others I consider myself a member of the community (MySQL, Postgres & RocksDB). And for MongoDB I used to be in the community.

I worked on Informix XPS in 1996. I chose Informix because I could live in Portland OR and walk to work. I was fresh out of school, didn't know much about DBMS, but got a great starter project (star query optimization). The company wasn't in great shape so I left by 1997 for Oracle. I never used Informix in production and didn't consider myself as part of the Informix community.

I was at Oracle from 1997 to 2005. The first 3 years were in Portland implementing JMS for the app server team and the last 5 years at Oracle HQ working on query execution.  I fixed many bugs, added support for ieee754 types, rewrote sort and maintained the sort and bitmap index row sources. The people there were great and I learned a lot but I did not enjoy the code base and left for a startup. I never used Oracle in production and don't consider myself as part of the Oracle community.

I lead the MySQL engineering teams at Google for 4 years and at Facebook/Meta for 10 years. I was very much immersed in production and have been active in the community since 2006. The MySQL teams got much done at both Google (GTID, semi-sync, crash-safe replication, rewrote the InnoDB rw lock) and Facebook/Meta (MyRocks and too many other things to mention). Over the years at FB/Meta my job duties got in the way of programming so I used performance testing as a way to remain current. I also filed many bugs might still be in the top-10 for bug reports. While Oracle has been a great steward for the MySQL project I have been critical about the performance regressions from older MySQL to newer MySQL. I hope that eventually stops because it will become a big problem.

I contributed some code to RocksDB, mostly for monitoring. I spent much more time doing performance QA for it, and filing a few bugs. I am definitely in the community.

I don't use Postgres in production but have spent much time doing performance QA for it over the past ~10 years. A small part of that was done while at Meta, I had a business case, and was able to use some of their HW and my time. But most of this has been a volunteer effort -- more than 100 hours of my time and 10,000+ hours of server time. Some of those server hours are in public clouds (Google, Hetzner) so I am also spending a bit on this. I found a few performance bugs. I have not found large performance regressions over time which is impressive. I have met many of the contributors working on the bits I care about, and that has been a nice benefit.

I used to be a member of the MongoDB community. Like Postgres, I never supported it in production but I spent much time doing performance QA with it. I wrote mostly positive blog posts, filed more than a few bugs and even won the William Zola Community Award. But I am busy enough with MySQL, Postgres and RocksDB so I haven't tried to use it for years. Regardless, I continue to be impressed by how fast they pay down tech debt, with one exception (no cost-based optimizer).