.. TODO:: document here the examples about plugins
+=======================
+Model-Checking Examples
+=======================
+
+The model-checker can be used to exhaustively search for issues in the
+tested application. It must be activated at compile time, but this
+mode is rather experimental in SimGrid (as of v3.22). You should not
+enable it unless you really want to formally verify your applications:
+SimGrid is slower and maybe less robust when MC is enabled.
+
+ - **Failed assert**
+ In this example, two actors send some data to a central server,
+ which asserts that the messages are always received in the same order.
+ This is obviously wrong, and the model-checker correctly finds a
+ counter-example to that assertion.
+ |br| `examples/s4u/mc-failed-assert/s4u-mc-failed-assert.cpp <https://framagit.org/simgrid/simgrid/tree/master/examples/s4u/mc-failed-assert/s4u-mc-failed-assert.cpp>`_
+
.. |br| raw:: html
<br />
