+
+Version 3.31 (expected spring 2021)
+-----------------------------------
+
+On the model checking front, the long awaited big bang finally occurred, greatly simplifying future evolution.
+
+A formal verification with Mc SimGrid implies two processes: a verified application that is an almost regular SimGrid simulation, and a checker that
+is an external process guiding the verified application to ensure that it explores every possible execution scenario. When formal verification was
+initially introduced in SimGrid 15 years ago, both processes were intertwined in the same system process but the mandated system tricks made it
+impossible to use classical debugging tools such as gdb or valgrind on that Frankenstein process. Having more than one heap in your process is not
+usually supported.
+
+The design was simplified in v3.12 (2015) by splitting the application and the checker in separate system process. But both processes remained tightly
+coupled: when the checker needed some information (for example the mailbox implied in a send operation to compute whether this operation `commutes
+with another one <https://en.wikipedia.org/wiki/Partial_order_reduction>`_), the checker was directly reading the memory of the other system process.
+This was efficient and nice in C, but it prevented us from using C++ features such as opaque ``std::function`` data types. As such, it hindered the
+ongoing SimDAG++ code reorganization toward SimGrid4, where all activity classes should be homogeneously written in modern C++.
+
+This release introduces a new design, where the simcalls are given object-oriented Observers that can serialize the relevant information over the wire.
+This information is used on the checker side to build Transition objects, representing the application simcalls. This explanation may not be crystal
+clear, but the checker code is now much easier to work with as the formal logic is not spoiled with system-level tricks to retrieve the needed information.
+
+Future work on the model checker include: support for mutexes (that are still not handled), implementation of another exploration algorithm based on UDPOR
+(`The Anh Pham's thesis <https://tel.archives-ouvertes.fr/tel-02462074/document>`_ was defended in 2019), and robustness improvement using the `MPI Bug
+Initiative <https://hal.archives-ouvertes.fr/hal-03474762>`_ tests. Many things that were long dreamed of now become technically possible in this code base.
+
+.. |br| raw:: html
+
+ <br />