From 0c6517fd643402677bbe121c804689e7a76ebeb2 Mon Sep 17 00:00:00 2001
From: Russoul <ruslan.feizerakhmanov@iohk.io>
Date: Tue, 5 May 2026 16:04:05 +0400
Subject: [PATCH 1/9] Get rid of TextFree IR

---
 .../cardano-recon-framework.cabal             |  1 -
 .../Internal/IR/HomogeneousFormula/FinFree.hs | 43 +++++++-------
 .../IR/HomogeneousFormula/TextFree.hs         | 58 -------------------
 3 files changed, 23 insertions(+), 79 deletions(-)
 delete mode 100644 bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula/TextFree.hs

diff --git a/bench/cardano-recon-framework/cardano-recon-framework.cabal b/bench/cardano-recon-framework/cardano-recon-framework.cabal
index be8a47c79f0..2fdf0d3ee6c 100644
--- a/bench/cardano-recon-framework/cardano-recon-framework.cabal
+++ b/bench/cardano-recon-framework/cardano-recon-framework.cabal
@@ -98,7 +98,6 @@ library
                     , Cardano.ReCon.LTL.Internal.Subst
                     , Cardano.ReCon.LTL.Internal.IR.HomogeneousFormula
                     , Cardano.ReCon.LTL.Internal.IR.HomogeneousFormula.FinFree
-                    , Cardano.ReCon.LTL.Internal.IR.HomogeneousFormula.TextFree
                     , Cardano.ReCon.Presburger.Internal.CooperQE
                     , Cardano.ReCon.Presburger.Internal.IR.AffineDNF
                     , Cardano.ReCon.Presburger.Internal.IR.CompNF
diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula/FinFree.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula/FinFree.hs
index b58f3dada69..06fade63350 100644
--- a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula/FinFree.hs
+++ b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula/FinFree.hs
@@ -9,15 +9,18 @@ module Cardano.ReCon.LTL.Internal.IR.HomogeneousFormula.FinFree (
 
 import           Cardano.ReCon.Common.Types (BinRel (..))
 import           Cardano.ReCon.LTL.Formula (IntTerm (..), IntValue, TextTerm (..), VariableIdentifier)
-import           Cardano.ReCon.LTL.Internal.IR.HomogeneousFormula.TextFree (Extended (..))
 import           Cardano.ReCon.LTL.Internal.Subst (substIntTerm)
-import qualified Cardano.ReCon.LTL.Internal.IR.HomogeneousFormula.TextFree as TextFree
+import qualified Cardano.ReCon.Presburger.Decide as PD
+import qualified Cardano.ReCon.Presburger.Formula as P
 
 import           Data.Functor ((<&>))
 import           Data.Set (Set)
 import qualified Data.Set as Set
 import           Data.Text (Text)
 
+-- | An extended value: either a concrete value or a placeholder distinct from all concrete values.
+data Extended a = Val a | Placeholder deriving (Show, Ord, Eq)
+
 -- | `HomogeneousFormula` with all finite-domain quantifiers already eliminated.
 --   Only infinite-domain (unbounded) quantifiers remain.
 data FinFree =
@@ -114,42 +117,42 @@ substText v x (PropTextExists x' phi) | x /= x' = PropTextExists x' (substText v
 substText _ _ (PropTextExists x' phi)            = PropTextExists x' phi
 
 -- ---------------------------------------------------------------------------
--- Lowering to TextFree
+-- Lowering to Presburger.Formula
 -- ---------------------------------------------------------------------------
 
--- | Lower a `FinFree` to `TextFree` by eliminating all text quantifiers and
+-- | Lower a `FinFree` to 'P.Formula' by eliminating all text quantifiers and
 --   evaluating ground `PropTextEq` atoms.
 --
 --   Text universals unfold to a conjunction (⊤ for empty domain);
 --   text existentials unfold to a disjunction (⊥ for empty domain).
 --
---   @'eval' = 'TextFree.eval' . 'lower'@
-lower :: FinFree -> TextFree.TextFree
-lower (Or phi psi)      = TextFree.Or (lower phi) (lower psi)
-lower (And phi psi)     = TextFree.And (lower phi) (lower psi)
-lower (Not phi)         = TextFree.Not (lower phi)
-lower (Implies phi psi) = TextFree.Implies (lower phi) (lower psi)
-lower Top               = TextFree.Top
-lower Bottom            = TextFree.Bottom
-lower (PropIntForall x phi) = TextFree.PropIntForall x (lower phi)
-lower (PropIntExists x phi) = TextFree.PropIntExists x (lower phi)
-lower (PropIntBinRel rel lhs rhs) = TextFree.PropIntBinRel rel lhs rhs
+--   @'eval' = 'PD.eval' . 'lower'@
+lower :: FinFree -> P.Formula
+lower (Or phi psi)      = P.Or (lower phi) (lower psi)
+lower (And phi psi)     = P.And (lower phi) (lower psi)
+lower (Not phi)         = P.Not (lower phi)
+lower (Implies phi psi) = P.Implies (lower phi) (lower psi)
+lower Top               = P.Top
+lower Bottom            = P.Bottom
+lower (PropIntForall x phi) = P.IntForall x (lower phi)
+lower (PropIntExists x phi) = P.IntExists x (lower phi)
+lower (PropIntBinRel rel lhs rhs) = P.IntBinRel rel lhs rhs
 -- Ground text equations are folded directly to ⊤/⊥:
 lower (PropTextEq (TextConst lhs) rhs)
-  | lhs == rhs = TextFree.Top
-  | otherwise  = TextFree.Bottom
+  | lhs == rhs = P.Top
+  | otherwise  = P.Bottom
 lower (PropTextEq (TextVar x) _) = error $ "lower: free text variable " <> show x
 -- ⟦∀x ∈ Text. φ⟧ ≡ φ[☐/x] ∧ φ[v₁/x] ∧ ...  (⊤ when dom is empty)
 lower (PropTextForall x phi) =
   let vals = Set.toList (textValues x phi)
-  in foldr TextFree.And TextFree.Top
+  in foldr P.And P.Top
        (lower (substText Placeholder x phi) : (vals <&> \v -> lower (substText (Val v) x phi)))
 -- ⟦∃x ∈ Text. φ⟧ ≡ φ[☐/x] ∨ φ[v₁/x] ∨ ...  (⊥ when dom is empty)
 lower (PropTextExists x phi) =
   let vals = Set.toList (textValues x phi)
-  in foldr TextFree.Or TextFree.Bottom
+  in foldr P.Or P.Bottom
        (lower (substText Placeholder x phi) : (vals <&> \v -> lower (substText (Val v) x phi)))
 
 -- | Evaluate the `FinFree` onto `Bool`.
 eval :: FinFree -> Bool
-eval = TextFree.eval . lower
+eval = PD.eval . lower
diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula/TextFree.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula/TextFree.hs
deleted file mode 100644
index 97fed563e62..00000000000
--- a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula/TextFree.hs
+++ /dev/null
@@ -1,58 +0,0 @@
-module Cardano.ReCon.LTL.Internal.IR.HomogeneousFormula.TextFree (
-    TextFree(..)
-  , Extended(..)
-  , eval
-  ) where
-
-import           Cardano.ReCon.Common.Types (BinRel (..))
-import           Cardano.ReCon.Integer.Polynomial.Term (IntTerm)
-import           Cardano.ReCon.LTL.Formula (VariableIdentifier)
-import qualified Cardano.ReCon.Presburger.Decide as PD
-import qualified Cardano.ReCon.Presburger.Formula as P
-
--- | An extended value: either a concrete value or a placeholder distinct from all concrete values.
-data Extended a = Val a | Placeholder deriving (Show, Ord, Eq)
-
--- | `FinFree` with all text quantifiers and `PropTextEq` atoms eliminated.
---   Only integer operations remain.
-data TextFree =
-   ------------ Connective -------------
-     Or TextFree TextFree
-   | And TextFree TextFree
-   | Not TextFree
-   | Implies TextFree TextFree
-   | Top
-   | Bottom
-   -------------------------------------
-
-   ----------- Event property ----------
-   | PropIntForall  VariableIdentifier TextFree
-   | PropIntExists  VariableIdentifier TextFree
-   | PropIntBinRel  BinRel IntTerm IntTerm
-   deriving (Show, Eq, Ord)
-   -------------------------------------
-
--- ---------------------------------------------------------------------------
--- Translation to Presburger arithmetic
--- ---------------------------------------------------------------------------
-
-toPresburger :: TextFree -> P.Formula
-toPresburger (Or phi psi)      = P.Or      (toPresburger phi) (toPresburger psi)
-toPresburger (And phi psi)     = P.And     (toPresburger phi) (toPresburger psi)
-toPresburger (Not phi)         = P.Not     (toPresburger phi)
-toPresburger (Implies phi psi) = P.Implies (toPresburger phi) (toPresburger psi)
-toPresburger Top               = P.Top
-toPresburger Bottom            = P.Bottom
-toPresburger (PropIntForall x phi)       = P.IntForall x (toPresburger phi)
-toPresburger (PropIntExists x phi)       = P.IntExists x (toPresburger phi)
-toPresburger (PropIntBinRel rel lhs rhs) = P.IntBinRel rel lhs rhs
-
-
--- ---------------------------------------------------------------------------
--- Evaluation
--- ---------------------------------------------------------------------------
-
--- | Evaluate a `TextFree` formula by translating to Presburger arithmetic
---   and deciding via quantifier elimination.
-eval :: TextFree -> Bool
-eval = PD.eval . toPresburger

From b4ea0d74d0dfe834b3f676b8c6d507e08fc06c10 Mon Sep 17 00:00:00 2001
From: Russoul <ruslan.feizerakhmanov@iohk.io>
Date: Tue, 5 May 2026 16:27:46 +0400
Subject: [PATCH 2/9] Implement a `ContinuousFormula` for filtering events by
 formula conformance

---
 .../cardano-recon-framework.cabal             |   1 +
 .../Cardano/ReCon/LTL/ContinuousFormula.hs    | 113 ++++++++++++++++++
 .../src/Cardano/ReCon/LTL/Formula.hs          |   3 +
 .../LTL/Internal/IR/HomogeneousFormula.hs     |   2 +-
 4 files changed, 118 insertions(+), 1 deletion(-)
 create mode 100644 bench/cardano-recon-framework/src/Cardano/ReCon/LTL/ContinuousFormula.hs

diff --git a/bench/cardano-recon-framework/cardano-recon-framework.cabal b/bench/cardano-recon-framework/cardano-recon-framework.cabal
index 2fdf0d3ee6c..95d8fe5ff75 100644
--- a/bench/cardano-recon-framework/cardano-recon-framework.cabal
+++ b/bench/cardano-recon-framework/cardano-recon-framework.cabal
@@ -72,6 +72,7 @@ library
                     , Cardano.ReCon.Common.Parser
 
                     , Cardano.ReCon.LTL.Check
+                    , Cardano.ReCon.LTL.ContinuousFormula
                     , Cardano.ReCon.LTL.Formula
                     , Cardano.ReCon.LTL.Formula.Parser
                     , Cardano.ReCon.LTL.Formula.Prec
diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/ContinuousFormula.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/ContinuousFormula.hs
new file mode 100644
index 00000000000..3a3edac510e
--- /dev/null
+++ b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/ContinuousFormula.hs
@@ -0,0 +1,113 @@
+module Cardano.ReCon.LTL.ContinuousFormula (
+    ContinuousFormula(..)
+  , interp
+  , eval) where
+
+import           Cardano.ReCon.Common.Types (BinRel (..), IntValue, VariableIdentifier)
+import           Cardano.ReCon.Integer.Polynomial.Term (IntTerm (..))
+import           Cardano.ReCon.LTL.Formula (Event (..), OnMissingKey (..), PropConstraint (..),
+                   TextTerm, TextValue)
+import           Cardano.ReCon.LTL.Internal.IR.HomogeneousFormula (HomogeneousFormula)
+import qualified Cardano.ReCon.LTL.Internal.IR.HomogeneousFormula as H
+
+import           Control.Monad.Reader (Reader, asks)
+import           Data.Map.Strict (lookup)
+import           Data.Set (Set)
+import qualified Data.Set as Set
+import qualified Data.Text as Text
+import           Prelude hiding (lookup)
+
+-- | Default name: φ.
+--
+--   The continuous counterpart of 'Formula': all temporal connectives are
+--   absent.  A 'ContinuousFormula' is evaluated against a /single/ event
+--   (or time unit) rather than a sequence, making it a purely propositional /
+--   first-order assertion about the present moment.
+data ContinuousFormula ty =
+
+   -------------- Atomic ---------------
+     -- | ty c̄
+     Atom ty (Set PropConstraint)
+   -------------------------------------
+
+   ------------ Connective -------------
+     -- | φ ∨ ψ
+   | Or (ContinuousFormula ty) (ContinuousFormula ty)
+     -- | φ ∧ ψ
+   | And (ContinuousFormula ty) (ContinuousFormula ty)
+     -- | ¬ φ
+   | Not (ContinuousFormula ty)
+     -- | φ ⇒ ψ
+   | Implies (ContinuousFormula ty) (ContinuousFormula ty)
+     -- | ⊤
+   | Top
+     -- | ⊥
+   | Bottom
+   -------------------------------------
+
+   ----------- Event property ----------
+     -- | ∀x ∈ ℤ. φ  —  x ranges over all integers
+   | PropIntForall  VariableIdentifier (ContinuousFormula ty)
+     -- | ∀x ∈ Text. φ  —  x ranges over all strings
+   | PropTextForall VariableIdentifier (ContinuousFormula ty)
+     -- | ∀x ∈ v̄. φ  —  x ranges over the given integers
+   | PropIntForallN  VariableIdentifier (Set IntValue)  (ContinuousFormula ty)
+     -- | ∀x ∈ v̄. φ  —  x ranges over the given strings
+   | PropTextForallN VariableIdentifier (Set TextValue) (ContinuousFormula ty)
+     -- | ∃x ∈ ℤ. φ  —  x ranges over all integers
+   | PropIntExists  VariableIdentifier (ContinuousFormula ty)
+     -- | ∃x ∈ Text. φ  —  x ranges over all strings
+   | PropTextExists VariableIdentifier (ContinuousFormula ty)
+     -- | ∃x ∈ v̄. φ  —  x ranges over the given integers
+   | PropIntExistsN  VariableIdentifier (Set IntValue)  (ContinuousFormula ty)
+     -- | ∃x ∈ v̄. φ  —  x ranges over the given strings
+   | PropTextExistsN VariableIdentifier (Set TextValue) (ContinuousFormula ty)
+     -- | t rel t  (integer)
+   | PropIntBinRel BinRel IntTerm IntTerm
+     -- | t = v  (text)
+   | PropTextEq TextTerm TextValue
+   -------------------------------------
+   deriving (Show, Eq, Ord)
+
+-- | Decide (e ⊧ φ).
+eval :: (Event event ty, Eq ty) => ContinuousFormula ty -> event -> Reader OnMissingKey Bool
+eval phi e = H.eval <$> interp phi e
+
+-- | Algorithm for (e ⊧ φ): checks each 'Atom' against the event type and
+--   substitutes property constraints with the event's concrete values,
+--   yielding a 'HomogeneousFormula' ready for decision.
+interp :: (Event event ty, Eq ty) => ContinuousFormula ty -> event -> Reader OnMissingKey HomogeneousFormula
+interp phi e = go phi
+  where
+    go (Atom ty cs)
+      | ofTy e ty = foldr H.And H.Top <$> traverse (evalConstraint ty) (Set.toList cs)
+      | otherwise = pure H.Bottom
+    go (Or phi' psi)      = H.Or      <$> go phi' <*> go psi
+    go (And phi' psi)     = H.And     <$> go phi' <*> go psi
+    go (Not phi')         = H.Not     <$> go phi'
+    go (Implies phi' psi) = H.Implies <$> go phi' <*> go psi
+    go Top                = pure H.Top
+    go Bottom             = pure H.Bottom
+    go (PropIntForall  x phi')       = H.PropIntForall  x <$> go phi'
+    go (PropTextForall x phi')       = H.PropTextForall x <$> go phi'
+    go (PropIntForallN  x dom phi')  = H.PropIntForallN  x dom <$> go phi'
+    go (PropTextForallN x dom phi')  = H.PropTextForallN x dom <$> go phi'
+    go (PropIntExists  x phi')       = H.PropIntExists  x <$> go phi'
+    go (PropTextExists x phi')       = H.PropTextExists x <$> go phi'
+    go (PropIntExistsN  x dom phi')  = H.PropIntExistsN  x dom <$> go phi'
+    go (PropTextExistsN x dom phi')  = H.PropTextExistsN x dom <$> go phi'
+    go (PropIntBinRel rel t1 t2)     = pure $ H.PropIntBinRel rel t1 t2
+    go (PropTextEq t v)              = pure $ H.PropTextEq t v
+
+    evalConstraint ty (IntPropConstraint key t) =
+      case lookup key (intProps e ty) of
+        Just v  -> pure $ H.PropIntBinRel Eq t (IntConst v)
+        Nothing -> missingKey key
+    evalConstraint ty (TextPropConstraint key t) =
+      case lookup key (textProps e ty) of
+        Just v  -> pure $ H.PropTextEq t v
+        Nothing -> missingKey key
+
+    missingKey key = asks $ \case
+      BottomOnMissingKey -> H.Bottom
+      CrashOnMissingKey  -> error $ "Missing key: " <> Text.unpack key
diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Formula.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Formula.hs
index 65fd24774f0..6851c415d3e 100644
--- a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Formula.hs
+++ b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Formula.hs
@@ -111,6 +111,9 @@ data Formula event ty =
      --   φ |¹⁺ᵏ ψ ≡ ψ ∨ ¬ ψ ∧ φ ∧ (φ |ᵏ ψ)
      --   φ until ψ in the n units of time from now
    | UntilN Word (Formula event ty) (Formula event ty)
+   -------------------------------------
+
+   -------------- Atomic ---------------
      -- | ty c̄
    | Atom ty (Set PropConstraint)
    -------------------------------------
diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula.hs
index 594641d588c..a0084c83378 100644
--- a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula.hs
+++ b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula.hs
@@ -21,7 +21,7 @@ import           Data.Set (Set)
 import qualified Data.Set as Set
 import           Data.Text (Text)
 
--- | A `Formula` with no temporal operators.
+-- | A `Formula` with no temporal operators and no atoms.
 --   Equivalence of two `HomogeneousFormula`s is decidable.
 data HomogeneousFormula =
    ------------ Connective -------------

From 1e0e494d6e4ff022d27219995b569fa3ddf7cb8a Mon Sep 17 00:00:00 2001
From: Russoul <ruslan.feizerakhmanov@iohk.io>
Date: Wed, 6 May 2026 14:52:00 +0400
Subject: [PATCH 3/9] cardano-recon-framework: Add cardano-recon-grep and
 ContinuousFormula (v1.2.0)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- Add `ContinuousFormula` — temporal-operator-free fragment of `Formula`,
  with `retract :: Formula event ty -> Maybe (ContinuousFormula ty)` and
  `eval :: ... -> event -> Reader OnMissingKey Bool`
- Add `cardano-recon-grep` executable (Global Realisation Print): prints a
  JSON array of TraceMessages that realise all given continuous formulas
- Simplify `prettyTraceMessage` to use ToJSON directly (no field remapping)
- Format negative-outcome relevant events as a JSON array in `prettySatisfactionResult`
- Remove dead `Common.hs` (extractJsonProps)
- Add `docs/formula-languages.txt` ASCII diagram of the formula language hierarchy
- Add note to `docs/ltl-formula-syntax.txt` on the `data` prefix omission convention
- Bump version to 1.2.0; update CHANGELOG and README
---
 bench/cardano-recon-framework/CHANGELOG.md    |   7 ++
 bench/cardano-recon-framework/README.md       |  42 ++++++-
 .../app/Cardano/ReCon/Common.hs               |  16 ---
 .../app/Cardano/ReCon/TraceMessage.hs         |  30 ++---
 .../app/Cardano/ReConGrep.hs                  | 113 ++++++++++++++++++
 .../cardano-recon-framework.cabal             |  27 ++++-
 .../docs/formula-languages.txt                |  84 +++++++++++++
 .../docs/ltl-formula-syntax.txt               |   3 +
 .../Cardano/ReCon/LTL/ContinuousFormula.hs    |  31 ++++-
 9 files changed, 313 insertions(+), 40 deletions(-)
 delete mode 100644 bench/cardano-recon-framework/app/Cardano/ReCon/Common.hs
 create mode 100644 bench/cardano-recon-framework/app/Cardano/ReConGrep.hs
 create mode 100644 bench/cardano-recon-framework/docs/formula-languages.txt

diff --git a/bench/cardano-recon-framework/CHANGELOG.md b/bench/cardano-recon-framework/CHANGELOG.md
index 9d27d8aa8fc..335b65f53d6 100644
--- a/bench/cardano-recon-framework/CHANGELOG.md
+++ b/bench/cardano-recon-framework/CHANGELOG.md
@@ -1,5 +1,12 @@
 # Revision history for cardano-trace-ltl
 
+## 1.2.0 -- May 2026
+
+* Add `ContinuousFormula` — the temporal-operator-free fragment of `Formula`, with `retract` for
+  converting a `Formula` and `eval` for deciding it against a single event.
+* Add `cardano-recon-grep` executable — filters a JSON array of `TraceMessage`s by a list of
+  continuous formulas, emitting only the messages that satisfy all of them.
+
 ## 1.1.1 -- April 2026
 * Support atoms that refer to property keys at arbitrary depth
 * Replace the `crash-on-missing-key` build flag with a runtime CLI option `--on-missing-key <crash|bottom>` (default: `bottom`)
diff --git a/bench/cardano-recon-framework/README.md b/bench/cardano-recon-framework/README.md
index 0705ba7772c..95b3c18bd43 100644
--- a/bench/cardano-recon-framework/README.md
+++ b/bench/cardano-recon-framework/README.md
@@ -1,6 +1,8 @@
 # Cardano Re(altime) Con(formance) Framework
 
-## What it does
+## Applications
+
+### `cardano-recon` — LTL conformance checker
 
 The application CLI takes as input:
   - A yaml list of strings, where each string is a parseable Linear Temporal Logic formula.
@@ -14,7 +16,7 @@ The application CLI takes as input:
 The application traverses the events from the given log files and checks if each given formula is satisfied by them.
 If negative, reports as such and lists the events that have been relevant to the formula.
 
-## CLI Syntax
+#### CLI Syntax
 
 ```
 Usage: cardano-recon FILE --mode <offline|online> --duration INT FILES
@@ -44,5 +46,41 @@ Available options:
   -h,--help                Show this help text
 ```
 
+### `cardano-recon-grep` — Global Realisation Print
+
+A stateless utility that filters a JSON array of trace messages by interpreting a list of
+_continuous_ (temporal-operator-free) formulas against each message individually.
+Only messages that satisfy **all** given formulas are written to stdout as a pretty-printed
+JSON array.
+
+Inputs:
+  - A YAML list of continuous formula strings (same syntax as `cardano-recon`, but temporal
+    operators such as `□`, `◇`, `○`, and `|` are not permitted).
+    For further details about the formula language, consult the [language overview](docs/formula-languages.txt).
+  - A JSON file containing an array of `TraceMessage` objects (e.g. the relevant-events output
+    produced by `cardano-recon` on a negative formula outcome).
+  - An optional context variables YAML file for variable substitution in formulas.
+  - An `--on-missing-key` policy (default: `bottom`) controlling behaviour when a formula
+    references a property absent from a message.
+
+#### CLI Syntax
+
+```
+Usage: cardano-recon-grep --formulas FILE --traces FILE
+                            [--context FILE]
+                            [--on-missing-key <crash|bottom>]
+
+  Filter log events that satisfy all given continuous formulas
+
+Available options:
+  --formulas FILE          YAML file with a list of ContinuousFormulas
+  --traces FILE            JSON array of TraceMessages to filter
+  --context FILE           context variables YAML file
+  --on-missing-key <crash|bottom>
+                           behaviour when a formula atom references a missing
+                           event property key (default: bottom)
+  -h,--help                Show this help text
+```
+
 ## Build flags
   - _debug_ for enabling verbose tracing of formulas as they evolve (multiple traces per each temporal event).
diff --git a/bench/cardano-recon-framework/app/Cardano/ReCon/Common.hs b/bench/cardano-recon-framework/app/Cardano/ReCon/Common.hs
deleted file mode 100644
index 622051c7eca..00000000000
--- a/bench/cardano-recon-framework/app/Cardano/ReCon/Common.hs
+++ /dev/null
@@ -1,16 +0,0 @@
-module Cardano.ReCon.Common where
-
-import           Data.Aeson (Object, Value (..))
-import           Data.Aeson.Key (toText)
-import qualified Data.Aeson.KeyMap as KeyMap
-import qualified Data.Map as Map
-import           Data.Map.Strict (Map)
-import           Data.Text (Text)
-
--- | Extract scalar properties from a JSON object as Aeson Values, for display.
-extractJsonProps :: Object -> Map Text Value
-extractJsonProps = Map.delete "kind" . Map.mapMaybe f . Map.mapKeysMonotonic toText . KeyMap.toMap
-  where
-    f v@(Number _) = Just v
-    f v@(String _) = Just v
-    f _            = Nothing
diff --git a/bench/cardano-recon-framework/app/Cardano/ReCon/TraceMessage.hs b/bench/cardano-recon-framework/app/Cardano/ReCon/TraceMessage.hs
index 700e24a4be0..0521888e6f6 100644
--- a/bench/cardano-recon-framework/app/Cardano/ReCon/TraceMessage.hs
+++ b/bench/cardano-recon-framework/app/Cardano/ReCon/TraceMessage.hs
@@ -5,17 +5,15 @@ module Cardano.ReCon.TraceMessage where
 import           Cardano.Logging
 import           Cardano.Logging.Prometheus.TCPServer (TracePrometheusSimple (..))
 import qualified Cardano.Logging.Types.TraceMessage as Envelop
-import           Cardano.ReCon.Common (extractJsonProps)
 import           Cardano.ReCon.LTL.Formula (Formula, Relevance)
 import qualified Cardano.ReCon.LTL.Formula.Prec as Prec
 import           Cardano.ReCon.LTL.Formula.Pretty (prettyFormula)
 import           Cardano.ReCon.LTL.Satisfy (SatisfactionResult (..))
 import           Cardano.ReCon.Trace.Feed (TemporalEvent (..))
 
-import           Data.Aeson (Value (..), (.=))
+import           Data.Aeson ((.=))
 import           Data.Aeson.Encode.Pretty
 import           Data.List (find)
-import qualified Data.Map as Map
 import qualified Data.Set as Set
 import           Data.Text (Text)
 import qualified Data.Text as Text
@@ -59,13 +57,7 @@ red :: Text -> Text
 red text = "\x001b[31m" <> text <> "\x001b[0m"
 
 prettyTraceMessage :: Envelop.TraceMessage -> Text
-prettyTraceMessage Envelop.TraceMessage{..} =
-  toStrict $ toLazyText $ encodePrettyToTextBuilder  $
-    Map.insert "at" (String (showT tmsgAt))        $
-      Map.insert "namespace" (String tmsgNS)       $
-        Map.insert "host" (String tmsgHost)        $
-          Map.insert "thread" (String tmsgThread)  $
-            extractJsonProps tmsgData
+prettyTraceMessage = toStrict . toLazyText . encodePrettyToTextBuilder
 
 prettyTemporalEvent :: TemporalEvent -> Text -> Text
 prettyTemporalEvent (TemporalEvent _ msgs) ns =
@@ -75,32 +67,32 @@ prettySatisfactionResult :: Formula TemporalEvent Text -> SatisfactionResult Tem
 prettySatisfactionResult initial Satisfied = prettyFormula initial Prec.Universe <> " " <> green "(✔)"
 prettySatisfactionResult initial (Unsatisfied rel) =
   prettyFormula initial Prec.Universe <> red " (✗)" <> "\n"
-    <> Text.intercalate
-         "\n----------------------------------------------\n"
-         (fmap (uncurry prettyTemporalEvent) (Set.toList rel))
+    <> "[\n"
+    <> Text.intercalate "\n,\n" (fmap (uncurry prettyTemporalEvent) (Set.toList rel))
+    <> "\n]"
 
 instance LogFormatting TraceMessage where
   forMachine _ FormulaStartCheck{..} = mconcat
     [
-      "formula" .= String (prettyFormula formula Prec.Universe),
+      "formula" .= prettyFormula formula Prec.Universe,
       "index" .= index
     ]
   forMachine _ FormulaProgressDump{..} = mconcat
     [
-      "events_per_second" .= Number (fromIntegral eventsPerSecond),
-      "catch_up_ratio" .= Number (realToFrac catchupRatio),
+      "events_per_second" .= (fromIntegral eventsPerSecond :: Int),
+      "catch_up_ratio" .= (realToFrac catchupRatio :: Double),
       "index" .= index
     ]
   forMachine _ FormulaPositiveOutcome{..} = mconcat
     [
-      "formula" .= String (prettyFormula formula Prec.Universe),
+      "formula" .= prettyFormula formula Prec.Universe,
       "index" .= index
     ]
   forMachine _ FormulaNegativeOutcome{..} = mconcat
     [
-      "formula" .= String (prettyFormula formula Prec.Universe)
+      "formula" .= prettyFormula formula Prec.Universe
     ,
-      "relevance" .= String (showT relevance)
+      "relevance" .= showT relevance
     ,
       "index" .= index
     ]
diff --git a/bench/cardano-recon-framework/app/Cardano/ReConGrep.hs b/bench/cardano-recon-framework/app/Cardano/ReConGrep.hs
new file mode 100644
index 00000000000..9bb3999fc52
--- /dev/null
+++ b/bench/cardano-recon-framework/app/Cardano/ReConGrep.hs
@@ -0,0 +1,113 @@
+module Main(main) where
+
+import           Cardano.Logging.Types.TraceMessage (TraceMessage (..))
+import qualified Cardano.ReCon.LTL.ContinuousFormula as CF
+import           Cardano.ReCon.LTL.Formula (OnMissingKey (..))
+import           Cardano.ReCon.LTL.Formula.Parser (Context (..))
+import qualified Cardano.ReCon.LTL.Formula.Parser as Parser
+import           Cardano.ReCon.LTL.Formula.Yaml (YamlReadError, readFormulas, readPropValues)
+import           Cardano.ReCon.Trace.Event ()
+import           Cardano.ReCon.Trace.Feed (TemporalEvent (..))
+
+import           Control.Arrow ((>>>))
+import           Control.Monad (forM_, (>=>))
+import           Control.Monad.Reader (runReader)
+import           Data.Aeson (decodeStrict')
+import           Data.Aeson.Encode.Pretty (encodePrettyToTextBuilder)
+import qualified Data.ByteString.Char8 as BChar8
+import qualified Data.Text.IO as TIO
+import           Data.Text.Lazy (toStrict)
+import           Data.Text.Lazy.Builder (toLazyText)
+import           Data.Char (toLower)
+import qualified Data.Map.Strict as Map
+import           Data.Maybe (fromMaybe)
+import           Data.Time.Clock.POSIX (utcTimeToPOSIXSeconds)
+import           Data.Text (Text)
+import qualified Data.Text as Text
+import           Data.Traversable (for)
+import           GHC.IO.Encoding (setLocaleEncoding, utf8)
+import           Options.Applicative
+import           System.Exit (die)
+
+data CliOptions = CliOptions
+  { formulas     :: FilePath
+  , traces       :: FilePath
+  , context      :: Maybe FilePath
+  , onMissingKey :: OnMissingKey
+  }
+
+readOnMissingKey :: ReadM OnMissingKey
+readOnMissingKey = eitherReader $ fmap toLower >>> \case
+  "crash"  -> Right CrashOnMissingKey
+  "bottom" -> Right BottomOnMissingKey
+  _        -> Left "Expected either of: 'crash' or 'bottom'"
+
+parseCliOptions :: Parser CliOptions
+parseCliOptions = CliOptions
+  <$> option str
+        (  long "formulas"
+        <> metavar "FILE"
+        <> help "YAML file with a list of ContinuousFormulas")
+  <*> option str
+        (  long "traces"
+        <> metavar "FILE"
+        <> help "JSON array of TraceMessages to filter")
+  <*> option (optional str)
+        (  long "context"
+        <> value Nothing
+        <> metavar "FILE"
+        <> help "context variables YAML file")
+  <*> option readOnMissingKey
+        (  long "on-missing-key"
+        <> metavar "<crash|bottom>"
+        <> showDefaultWith (\case BottomOnMissingKey -> "bottom"; CrashOnMissingKey -> "crash")
+        <> value BottomOnMissingKey
+        <> help "behaviour when a formula atom references a missing event property key")
+
+opts :: ParserInfo CliOptions
+opts = info (parseCliOptions <**> helper)
+  (fullDesc <> progDesc "Print log events that realise all given continuous formulas (Global Realisation Print)")
+
+msgToEvent :: TraceMessage -> TemporalEvent
+msgToEvent msg = TemporalEvent { beg = round (utcTimeToPOSIXSeconds msg.tmsgAt * 1_000_000), messages = [msg] }
+
+prettyMsg :: TraceMessage -> Text
+prettyMsg = toStrict . toLazyText . encodePrettyToTextBuilder
+
+printArray :: [TraceMessage] -> IO ()
+printArray [] = TIO.putStrLn "[]"
+printArray (x : xs) = do
+  TIO.putStrLn "["
+  TIO.putStr (prettyMsg x)
+  forM_ xs $ \m -> do
+    TIO.putStr "\n,"
+    TIO.putStr (prettyMsg m)
+  TIO.putStrLn "\n]"
+
+main :: IO ()
+main = do
+  setLocaleEncoding utf8
+  options <- execParser opts
+  ctx <- Map.toList . fromMaybe Map.empty <$>
+    for options.context (readPropValues >=> dieOnYamlError)
+  rawFormulas <- readFormulas options.formulas
+                   (Context { interpDomain = ctx, varKinds = Map.empty })
+                   Parser.name
+                 >>= dieOnYamlError
+  cformulas <- mapM retractOrDie rawFormulas
+  content <- BChar8.readFile options.traces
+  msgs <- maybe (die "Failed to parse input as a JSON array of TraceMessages") pure
+            (decodeStrict' content :: Maybe [TraceMessage])
+  let matching = [ msg | msg <- msgs
+                       , let event = msgToEvent msg
+                       , all (\phi -> runReader (CF.eval phi event) options.onMissingKey) cformulas ]
+  printArray matching
+  where
+    dieOnYamlError :: Either YamlReadError a -> IO a
+    dieOnYamlError (Left err) = die (Text.unpack err)
+    dieOnYamlError (Right ok) = pure ok
+
+    retractOrDie phi = case CF.retract phi of
+      Just cf -> pure cf
+      Nothing -> die
+        "One of the formulas contains a temporal connective; filter mode only accepts continuous formulas"
diff --git a/bench/cardano-recon-framework/cardano-recon-framework.cabal b/bench/cardano-recon-framework/cardano-recon-framework.cabal
index 95d8fe5ff75..eae578820e1 100644
--- a/bench/cardano-recon-framework/cardano-recon-framework.cabal
+++ b/bench/cardano-recon-framework/cardano-recon-framework.cabal
@@ -4,7 +4,7 @@ description:        Cardano Re(altime) Con(formance) Framework based on Linear T
 category:           Cardano
                     Testing
 copyright:          2026 Intersect.
-version:            1.1.1
+version:            1.2.0
 license:            Apache-2.0
 license-files:      LICENSE
                     NOTICE
@@ -143,7 +143,6 @@ executable cardano-recon
     other-modules:
         Cardano.ReCon.TraceMessage
       , Cardano.ReCon.Cli
-      , Cardano.ReCon.Common
     other-extensions:
 
     -- Other library packages from which modules are imported.
@@ -167,6 +166,30 @@ executable cardano-recon
     -- Directories containing source files.
     hs-source-dirs:   app
 
+executable cardano-recon-grep
+    import:           common
+    main-is:          Cardano/ReConGrep.hs
+
+    ghc-options:      -O2
+                      -threaded
+                      -rtsopts
+                      "-with-rtsopts=-N2"
+
+    build-depends:
+        base
+      , text
+      , containers
+      , bytestring
+      , aeson
+      , aeson-pretty
+      , mtl
+      , time
+      , cardano-recon-framework
+      , trace-dispatcher ^>= 2.12
+      , optparse-applicative
+
+    hs-source-dirs:   app
+
 test-suite cardano-recon-test
   import: common
   type: exitcode-stdio-1.0
diff --git a/bench/cardano-recon-framework/docs/formula-languages.txt b/bench/cardano-recon-framework/docs/formula-languages.txt
new file mode 100644
index 00000000000..211dff71e85
--- /dev/null
+++ b/bench/cardano-recon-framework/docs/formula-languages.txt
@@ -0,0 +1,84 @@
+Formula Languages in Cardano ReCon
+====================================
+
+Languages are ordered from most to least expressive.
+Each language is a strict subset of the language above it.
+
+┌─────────────────────────────────────────────────────────────────────────┐
+│  Formula event ty                                                       │
+│  src/Cardano/ReCon/LTL/Formula.hs                                       │
+│                                                                         │
+│  temporal : ☐ᵏ φ   ♢ᵏ φ   ◯ φ   ◯ᵏ φ   φ |ᵏ ψ                           │
+│  atomic   : Atom ty cs                                                  │
+│  boolean  : ∧  ∨  ¬  ⇒  ⊤  ⊥                                            │
+│  FO       : ∀x∈ℤ  ∃x∈ℤ  ∀x∈{v̄}  ∃x∈{v̄}  ∀x∈Text  ∃x∈Text                │
+│  ground   : t rel t'  (int)       t = v  (text)                         │
+└────────────┬─────────────────────────────────────────┬──────────────────┘
+             │                                         │
+        retract                                   H.retract
+    (partial: fails                            (partial: fails on
+     on temporal ops)                           temporal ops or atoms)
+             │                                         │
+             ▼                                         │
+┌────────────────────────────────┐                     │
+│  ContinuousFormula ty          │                     │
+│  src/Cardano/ReCon/LTL/        │                     │
+│  ContinuousFormula.hs          │                     │
+│                                │                     │
+│  atomic  : Atom ty cs          │                     │
+│  boolean : ∧  ∨  ¬  ⇒  ⊤  ⊥    │                     │
+│  FO      : ∀x∈ℤ  ∃x∈ℤ          │                     │
+│            ∀x∈{v̄}  ∃x∈{v̄}      │                     │
+│            ∀x∈Text  ∃x∈Text    │                     │
+│  ground  : t rel t'   t = v    │                     │
+└────────────┬───────────────────┘                     │
+             │                                         │
+         interp(e)                           next(e) then rewrite
+      (resolve atoms                          ↺ repeated per event;
+       against event e)                       terminate at end of seq
+             │                                         │
+             └─────────────────────┬───────────────────┘
+                                   │
+                                   ▼
+┌─────────────────────────────────────────────────────────────────────────┐
+│  HomogeneousFormula                                                     │
+│  src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula.hs                │
+│                                                                         │
+│  boolean : ∧  ∨  ¬  ⇒  ⊤  ⊥                                             │
+│  FO      : ∀x∈ℤ  ∃x∈ℤ  ∀x∈{v̄}  ∃x∈{v̄}  ∀x∈Text  ∃x∈Text                 │
+│  ground  : t rel t'  (int)       t = v  (text)                          │
+└──────────────────────────────────┬──────────────────────────────────────┘
+                                   │
+                                 lower
+                         (unfold ∀x∈{v̄}, ∃x∈{v̄}
+                          into ∧ / ∨)
+                                   │
+                                   ▼
+┌─────────────────────────────────────────────────────────────────────────┐
+│  FinFree                                                                │
+│  src/Cardano/ReCon/LTL/Internal/IR/HomogeneousFormula/FinFree.hs        │
+│                                                                         │
+│  boolean : ∧  ∨  ¬  ⇒  ⊤  ⊥                                             │
+│  FO      : ∀x∈ℤ  ∃x∈ℤ  ∀x∈Text  ∃x∈Text                                 │
+│  ground  : t rel t'  (int)       t = v  (text)                          │
+└──────────────────────────────────┬──────────────────────────────────────┘
+                                   │
+                                 lower
+                         (decide ∀x∈Text, ∃x∈Text via
+                          value accumulation + substitution)
+                                   │
+                                   ▼
+┌─────────────────────────────────────────────────────────────────────────┐
+│  Presburger.Formula                                                     │
+│  src/Cardano/ReCon/Presburger/Formula.hs                                │
+│                                                                         │
+│  boolean : ∧  ∨  ¬  ⇒  ⊤  ⊥                                             │
+│  FO      : ∀x∈ℤ  ∃x∈ℤ                                                   │
+│  ground  : t rel t'  (int only)                                         │
+└──────────────────────────────────┬──────────────────────────────────────┘
+                                   │
+                                PD.eval
+                          (Cooper quantifier elimination)
+                                   │
+                                   ▼
+                                 Bool
diff --git a/bench/cardano-recon-framework/docs/ltl-formula-syntax.txt b/bench/cardano-recon-framework/docs/ltl-formula-syntax.txt
index fcf10643a60..007efcd1226 100644
--- a/bench/cardano-recon-framework/docs/ltl-formula-syntax.txt
+++ b/bench/cardano-recon-framework/docs/ltl-formula-syntax.txt
@@ -37,6 +37,9 @@ c ::= name = t                // property constraint, examples:
                               //   — slot = 1
                               //   — "host" = "macbook-pro"
                               //   — slot = x
+                              // Note: TraceMessage properties live inside the "data" JSON
+                              // object. The "data" prefix is omitted when writing names;
+                              // write `slot = 42`, not `data.slot = 42`.
 c̄ ::= {c, ..., c}             // set of property constraints, examples:
                               //   — {slot = x}
                               //   — {slot = 42, blockHash = "xyz"}
diff --git a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/ContinuousFormula.hs b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/ContinuousFormula.hs
index 3a3edac510e..0ca1b9acb9d 100644
--- a/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/ContinuousFormula.hs
+++ b/bench/cardano-recon-framework/src/Cardano/ReCon/LTL/ContinuousFormula.hs
@@ -1,12 +1,14 @@
 module Cardano.ReCon.LTL.ContinuousFormula (
     ContinuousFormula(..)
+  , retract
   , interp
   , eval) where
 
 import           Cardano.ReCon.Common.Types (BinRel (..), IntValue, VariableIdentifier)
 import           Cardano.ReCon.Integer.Polynomial.Term (IntTerm (..))
-import           Cardano.ReCon.LTL.Formula (Event (..), OnMissingKey (..), PropConstraint (..),
+import           Cardano.ReCon.LTL.Formula (Event (..), Formula, OnMissingKey (..), PropConstraint (..),
                    TextTerm, TextValue)
+import qualified Cardano.ReCon.LTL.Formula as F
 import           Cardano.ReCon.LTL.Internal.IR.HomogeneousFormula (HomogeneousFormula)
 import qualified Cardano.ReCon.LTL.Internal.IR.HomogeneousFormula as H
 
@@ -69,6 +71,33 @@ data ContinuousFormula ty =
    -------------------------------------
    deriving (Show, Eq, Ord)
 
+-- | Retract a 'Formula' into a 'ContinuousFormula', returning 'Nothing' if
+--   the formula contains any temporal connective.
+retract :: Formula event ty -> Maybe (ContinuousFormula ty)
+retract (F.Forall {})            = Nothing
+retract (F.ForallN {})           = Nothing
+retract (F.ExistsN {})           = Nothing
+retract (F.Next {})              = Nothing
+retract (F.NextN {})             = Nothing
+retract (F.UntilN {})            = Nothing
+retract (F.Atom ty cs)           = Just (Atom ty cs)
+retract (F.Or phi psi)           = Or      <$> retract phi <*> retract psi
+retract (F.And phi psi)          = And     <$> retract phi <*> retract psi
+retract (F.Not phi)              = Not     <$> retract phi
+retract (F.Implies phi psi)      = Implies <$> retract phi <*> retract psi
+retract F.Top                    = Just Top
+retract F.Bottom                 = Just Bottom
+retract (F.PropIntForall  x phi)        = PropIntForall  x     <$> retract phi
+retract (F.PropTextForall x phi)        = PropTextForall x     <$> retract phi
+retract (F.PropIntForallN  x dom phi)   = PropIntForallN  x dom <$> retract phi
+retract (F.PropTextForallN x dom phi)   = PropTextForallN x dom <$> retract phi
+retract (F.PropIntExists  x phi)        = PropIntExists  x     <$> retract phi
+retract (F.PropTextExists x phi)        = PropTextExists x     <$> retract phi
+retract (F.PropIntExistsN  x dom phi)   = PropIntExistsN  x dom <$> retract phi
+retract (F.PropTextExistsN x dom phi)   = PropTextExistsN x dom <$> retract phi
+retract (F.PropIntBinRel rel _ t1 t2)   = Just (PropIntBinRel rel t1 t2)
+retract (F.PropTextEq _ t v)            = Just (PropTextEq t v)
+
 -- | Decide (e ⊧ φ).
 eval :: (Event event ty, Eq ty) => ContinuousFormula ty -> event -> Reader OnMissingKey Bool
 eval phi e = H.eval <$> interp phi e

From 591fc8022866d08e06f17ca3da0ab84fb5f2f1e9 Mon Sep 17 00:00:00 2001
From: Russoul <ruslan.feizerakhmanov@iohk.io>
Date: Wed, 6 May 2026 15:27:08 +0400
Subject: [PATCH 4/9] cardano-recon-grep: support reading traces from stdin
 when --traces is omitted

---
 bench/cardano-recon-framework/README.md                | 10 +++++-----
 bench/cardano-recon-framework/app/Cardano/ReConGrep.hs | 10 ++++++----
 2 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/bench/cardano-recon-framework/README.md b/bench/cardano-recon-framework/README.md
index 95b3c18bd43..efa4132081a 100644
--- a/bench/cardano-recon-framework/README.md
+++ b/bench/cardano-recon-framework/README.md
@@ -57,8 +57,8 @@ Inputs:
   - A YAML list of continuous formula strings (same syntax as `cardano-recon`, but temporal
     operators such as `□`, `◇`, `○`, and `|` are not permitted).
     For further details about the formula language, consult the [language overview](docs/formula-languages.txt).
-  - A JSON file containing an array of `TraceMessage` objects (e.g. the relevant-events output
-    produced by `cardano-recon` on a negative formula outcome).
+  - A JSON array of `TraceMessage` objects, read from a file (`--traces FILE`) or from stdin
+    if `--traces` is omitted (e.g. piped from `cardano-recon` on a negative formula outcome).
   - An optional context variables YAML file for variable substitution in formulas.
   - An `--on-missing-key` policy (default: `bottom`) controlling behaviour when a formula
     references a property absent from a message.
@@ -66,15 +66,15 @@ Inputs:
 #### CLI Syntax
 
 ```
-Usage: cardano-recon-grep --formulas FILE --traces FILE
+Usage: cardano-recon-grep --formulas FILE [--traces FILE]
                             [--context FILE]
                             [--on-missing-key <crash|bottom>]
 
-  Filter log events that satisfy all given continuous formulas
+  Print log events that realise all given continuous formulas (Global Realisation Print)
 
 Available options:
   --formulas FILE          YAML file with a list of ContinuousFormulas
-  --traces FILE            JSON array of TraceMessages to filter
+  --traces FILE            JSON array of TraceMessages to filter (default: stdin)
   --context FILE           context variables YAML file
   --on-missing-key <crash|bottom>
                            behaviour when a formula atom references a missing
diff --git a/bench/cardano-recon-framework/app/Cardano/ReConGrep.hs b/bench/cardano-recon-framework/app/Cardano/ReConGrep.hs
index 9bb3999fc52..4e795883581 100644
--- a/bench/cardano-recon-framework/app/Cardano/ReConGrep.hs
+++ b/bench/cardano-recon-framework/app/Cardano/ReConGrep.hs
@@ -14,6 +14,7 @@ import           Control.Monad (forM_, (>=>))
 import           Control.Monad.Reader (runReader)
 import           Data.Aeson (decodeStrict')
 import           Data.Aeson.Encode.Pretty (encodePrettyToTextBuilder)
+import qualified Data.ByteString as BS
 import qualified Data.ByteString.Char8 as BChar8
 import qualified Data.Text.IO as TIO
 import           Data.Text.Lazy (toStrict)
@@ -31,7 +32,7 @@ import           System.Exit (die)
 
 data CliOptions = CliOptions
   { formulas     :: FilePath
-  , traces       :: FilePath
+  , traces       :: Maybe FilePath
   , context      :: Maybe FilePath
   , onMissingKey :: OnMissingKey
   }
@@ -48,10 +49,11 @@ parseCliOptions = CliOptions
         (  long "formulas"
         <> metavar "FILE"
         <> help "YAML file with a list of ContinuousFormulas")
-  <*> option str
+  <*> option (optional str)
         (  long "traces"
+        <> value Nothing
         <> metavar "FILE"
-        <> help "JSON array of TraceMessages to filter")
+        <> help "JSON array of TraceMessages to filter (default: stdin)")
   <*> option (optional str)
         (  long "context"
         <> value Nothing
@@ -95,7 +97,7 @@ main = do
                    Parser.name
                  >>= dieOnYamlError
   cformulas <- mapM retractOrDie rawFormulas
-  content <- BChar8.readFile options.traces
+  content <- maybe BS.getContents BChar8.readFile options.traces
   msgs <- maybe (die "Failed to parse input as a JSON array of TraceMessages") pure
             (decodeStrict' content :: Maybe [TraceMessage])
   let matching = [ msg | msg <- msgs

From 5ed4e28d5693bdd1f7c95540ae23dee8ce5820a9 Mon Sep 17 00:00:00 2001
From: Russoul <ruslan.feizerakhmanov@iohk.io>
Date: Wed, 6 May 2026 16:05:30 +0400
Subject: [PATCH 5/9] cardano-recon: add --grep flag for machine-readable
 negative outcome output

---
 .../app/Cardano/ReCon.hs                      | 25 +++++++++++--------
 .../app/Cardano/ReCon/Cli.hs                  |  7 ++++++
 .../app/Cardano/ReCon/TraceMessage.hs         | 25 +++++++++++--------
 3 files changed, 36 insertions(+), 21 deletions(-)

diff --git a/bench/cardano-recon-framework/app/Cardano/ReCon.hs b/bench/cardano-recon-framework/app/Cardano/ReCon.hs
index 55e4355e41e..d442b3dd5ca 100644
--- a/bench/cardano-recon-framework/app/Cardano/ReCon.hs
+++ b/bench/cardano-recon-framework/app/Cardano/ReCon.hs
@@ -45,18 +45,18 @@ import qualified System.Metrics as EKG
 import           Streaming
 
 
-check :: OnMissingKey -> Word -> Trace IO App.TraceMessage -> Formula TemporalEvent Text -> [TemporalEvent] -> IO ()
-check omk idx {- Formula index -} tr phi events =
+check :: OnMissingKey -> Bool -> Word -> Trace IO App.TraceMessage -> Formula TemporalEvent Text -> [TemporalEvent] -> IO ()
+check omk greppable idx {- Formula index -} tr phi events =
   let result = satisfies omk phi events in
-  traceWith tr $ formulaOutcome phi result idx
+  traceWith tr $ formulaOutcome greppable phi result idx
 
-checkS' :: OnMissingKey -> Bool -> Word -> Trace IO App.TraceMessage -> Formula TemporalEvent Text -> Stream (Of TemporalEvent) IO () -> IO ()
-checkS' omk enableProgressDumps idx {- Formula index -} tr phi events = do
+checkS' :: OnMissingKey -> Bool -> Bool -> Word -> Trace IO App.TraceMessage -> Formula TemporalEvent Text -> Stream (Of TemporalEvent) IO () -> IO ()
+checkS' omk greppable enableProgressDumps idx {- Formula index -} tr phi events = do
   let initial = SatisfyMetrics 0 phi 0
   metrics <- newIORef initial
   withAsync (when enableProgressDumps $ runDisplayProgressDump initial metrics) $ \counterDisplayThread -> do
     r <- satisfiesS omk phi events metrics
-    traceWith tr $ formulaOutcome phi r idx
+    traceWith tr $ formulaOutcome greppable phi r idx
     cancel counterDisplayThread
   where
     runDisplayProgressDump :: SatisfyMetrics TemporalEvent Text -> IORef (SatisfyMetrics TemporalEvent Text) -> IO ()
@@ -69,6 +69,7 @@ checkS' omk enableProgressDumps idx {- Formula index -} tr phi events = do
       runDisplayProgressDump next counter
 
 checkOnline :: OnMissingKey
+            -> Bool
             -> Bool
             -> Trace IO App.TraceMessage
             -> TemporalEventDurationMicrosec
@@ -78,23 +79,24 @@ checkOnline :: OnMissingKey
             -> [FilePath]
             -> [Formula TemporalEvent Text]
             -> IO ()
-checkOnline omk enableProgressDumps tr eventDuration retentionMs failureMode ingestMode files phis = do
+checkOnline omk greppable enableProgressDumps tr eventDuration retentionMs failureMode ingestMode files phis = do
   ing <- mkIngestor (fromIntegral retentionMs)
   for_ files (ingestFileThreaded ing failureMode ingestMode)
   forConcurrently_ (zip [0..] phis) $ \(idx, phi) -> mkIngestorReader ing >>= \reader -> forever $ do
     traceWith tr $ FormulaStartCheck phi idx
-    checkS' omk enableProgressDumps idx tr phi (readS reader eventDuration)
+    checkS' omk greppable enableProgressDumps idx tr phi (readS reader eventDuration)
 
 checkOffline :: OnMissingKey
+             -> Bool
              -> Trace IO App.TraceMessage
              -> TemporalEventDurationMicrosec
              -> FilePath
              -> [Formula TemporalEvent Text]
              -> IO ()
-checkOffline omk tr eventDuration file phis = do
+checkOffline omk greppable tr eventDuration file phis = do
   events <- read file eventDuration
   forConcurrently_ (zip [0..] phis) $ \(idx, phi) ->
-    check omk idx tr phi events
+    check omk greppable idx tr phi events
   threadDelay 200_000 -- Give the tracer a grace period to output the logs to whatever backend
 
 setupTraceDispatcher :: Maybe FilePath -> IO (Trace IO App.TraceMessage)
@@ -157,10 +159,11 @@ main = do
       file <- case options.traces of
         [x] -> pure x
         _   -> die "Only exactly one trace file is supported in 'offline' mode"
-      checkOffline options.onMissingKey tr options.duration file formulas'
+      checkOffline options.onMissingKey options.greppable tr options.duration file formulas'
     Online -> do
       checkOnline
         options.onMissingKey
+        options.greppable
         options.enableProgressDumps
         tr
         options.duration
diff --git a/bench/cardano-recon-framework/app/Cardano/ReCon/Cli.hs b/bench/cardano-recon-framework/app/Cardano/ReCon/Cli.hs
index de1f58fded2..8917d1c5479 100644
--- a/bench/cardano-recon-framework/app/Cardano/ReCon/Cli.hs
+++ b/bench/cardano-recon-framework/app/Cardano/ReCon/Cli.hs
@@ -134,6 +134,11 @@ parseOnMissingKey = option readOnMissingKey $
   <> value BottomOnMissingKey
   <> help "behaviour when a formula atom references a missing event property key"
 
+parseGreppable :: Parser Bool
+parseGreppable = switch $
+     long "grep"
+  <> help "on formula violation print only the JSON array of relevant events; print nothing on satisfaction"
+
 data CliOptions = CliOptions
   { formulas            :: FilePath
   , mode                :: Mode
@@ -146,6 +151,7 @@ data CliOptions = CliOptions
   , enableSeekToEnd     :: Bool
   , timeunit            :: Timeunit
   , onMissingKey        :: OnMissingKey
+  , greppable           :: Bool
   }
 
 parseCliOptions :: Parser CliOptions
@@ -161,6 +167,7 @@ parseCliOptions = CliOptions
               <*> parseSeekToEnd
               <*> parseTimeunit
               <*> parseOnMissingKey
+              <*> parseGreppable
 
 opts :: ParserInfo CliOptions
 opts = info (parseCliOptions <**> helper)
diff --git a/bench/cardano-recon-framework/app/Cardano/ReCon/TraceMessage.hs b/bench/cardano-recon-framework/app/Cardano/ReCon/TraceMessage.hs
index 0521888e6f6..190d3eba1d8 100644
--- a/bench/cardano-recon-framework/app/Cardano/ReCon/TraceMessage.hs
+++ b/bench/cardano-recon-framework/app/Cardano/ReCon/TraceMessage.hs
@@ -38,17 +38,18 @@ data TraceMessage = FormulaStartCheck {
                   -- | Formula outcomes are split into (+) and (-) as we'd like to print them at distinct severity levels,
                   --   but severity level is indexed by namespace (= constructor name), hence
                   --   we can't store both outcomes in one constructor.
-                  | FormulaPositiveOutcome { formula :: Formula TemporalEvent Text, index :: Word }
+                  | FormulaPositiveOutcome { formula :: Formula TemporalEvent Text, index :: Word, greppable :: Bool }
                   | FormulaNegativeOutcome {
                       formula   :: Formula TemporalEvent Text,
                       relevance :: Relevance TemporalEvent Text,
-                      index :: Word
+                      index     :: Word,
+                      greppable :: Bool
                   }
 
 -- | Smart constructor.
-formulaOutcome :: Formula TemporalEvent Text -> SatisfactionResult TemporalEvent Text -> Word -> TraceMessage
-formulaOutcome formula Satisfied         idx = FormulaPositiveOutcome formula idx
-formulaOutcome formula (Unsatisfied rel) idx = FormulaNegativeOutcome formula rel idx
+formulaOutcome :: Bool -> Formula TemporalEvent Text -> SatisfactionResult TemporalEvent Text -> Word -> TraceMessage
+formulaOutcome greppable formula Satisfied         idx = FormulaPositiveOutcome { formula, index = idx, greppable }
+formulaOutcome greppable formula (Unsatisfied rel) idx = FormulaNegativeOutcome { formula, relevance = rel, index = idx, greppable }
 
 green :: Text -> Text
 green text = "\x001b[32m" <> text <> "\x001b[0m"
@@ -63,13 +64,17 @@ prettyTemporalEvent :: TemporalEvent -> Text -> Text
 prettyTemporalEvent (TemporalEvent _ msgs) ns =
   maybe ("<<Unexpected namespace " <> ns <> ">>") prettyTraceMessage (find (\ x -> x.tmsgNS == ns) msgs)
 
+prettyRelevanceArray :: Relevance TemporalEvent Text -> Text
+prettyRelevanceArray rel =
+  "[\n"
+  <> Text.intercalate "\n,\n" (fmap (uncurry prettyTemporalEvent) (Set.toList rel))
+  <> "\n]"
+
 prettySatisfactionResult :: Formula TemporalEvent Text -> SatisfactionResult TemporalEvent Text -> Text
 prettySatisfactionResult initial Satisfied = prettyFormula initial Prec.Universe <> " " <> green "(✔)"
 prettySatisfactionResult initial (Unsatisfied rel) =
   prettyFormula initial Prec.Universe <> red " (✗)" <> "\n"
-    <> "[\n"
-    <> Text.intercalate "\n,\n" (fmap (uncurry prettyTemporalEvent) (Set.toList rel))
-    <> "\n]"
+  <> prettyRelevanceArray rel
 
 instance LogFormatting TraceMessage where
   forMachine _ FormulaStartCheck{..} = mconcat
@@ -108,9 +113,9 @@ instance LogFormatting TraceMessage where
       <> "formula: " <> prettyFormula formula Prec.Universe <> "\n"
       <> "index: " <> showT index
   forHuman FormulaPositiveOutcome{..} =
-    prettySatisfactionResult formula Satisfied
+    if greppable then "" else prettySatisfactionResult formula Satisfied
   forHuman FormulaNegativeOutcome{..} =
-    prettySatisfactionResult formula (Unsatisfied relevance)
+    if greppable then prettyRelevanceArray relevance else prettySatisfactionResult formula (Unsatisfied relevance)
 
   asMetrics FormulaStartCheck{} = []
   asMetrics (FormulaProgressDump {catchupRatio, index}) = [DoubleM ("catchup_ratio_" <> showT index) catchupRatio]

From 2e5d448388a159a4084a6cb33d704fc22f238ad7 Mon Sep 17 00:00:00 2001
From: Russoul <ruslan.feizerakhmanov@iohk.io>
Date: Wed, 6 May 2026 16:31:56 +0400
Subject: [PATCH 6/9] cardano-recon: --grep bypasses trace-dispatcher; add
 ContextDump trace message

- --grep now prints directly to stdout, keeping greppable out of TraceMessage
- Context printout replaced with a ContextDump TraceMessage at Debug severity
---
 .../app/Cardano/ReCon.hs                      | 16 ++++++++---
 .../app/Cardano/ReCon/TraceMessage.hs         | 27 +++++++++++++------
 2 files changed, 31 insertions(+), 12 deletions(-)

diff --git a/bench/cardano-recon-framework/app/Cardano/ReCon.hs b/bench/cardano-recon-framework/app/Cardano/ReCon.hs
index d442b3dd5ca..cf0df8e3bcd 100644
--- a/bench/cardano-recon-framework/app/Cardano/ReCon.hs
+++ b/bench/cardano-recon-framework/app/Cardano/ReCon.hs
@@ -34,6 +34,7 @@ import qualified Data.Map as Map
 import           Data.Maybe (fromMaybe, listToMaybe)
 import           Data.Text (Text)
 import qualified Data.Text as Text
+import qualified Data.Text.IO as TIO
 import           Data.Traversable (for)
 import           GHC.IO.Encoding (setLocaleEncoding, utf8)
 import           Network.HostName (HostName)
@@ -48,7 +49,11 @@ import           Streaming
 check :: OnMissingKey -> Bool -> Word -> Trace IO App.TraceMessage -> Formula TemporalEvent Text -> [TemporalEvent] -> IO ()
 check omk greppable idx {- Formula index -} tr phi events =
   let result = satisfies omk phi events in
-  traceWith tr $ formulaOutcome greppable phi result idx
+  if greppable
+    then case result of
+      Satisfied       -> pure ()
+      Unsatisfied rel -> TIO.putStrLn (App.prettyRelevanceArray rel)
+    else traceWith tr $ formulaOutcome phi result idx
 
 checkS' :: OnMissingKey -> Bool -> Bool -> Word -> Trace IO App.TraceMessage -> Formula TemporalEvent Text -> Stream (Of TemporalEvent) IO () -> IO ()
 checkS' omk greppable enableProgressDumps idx {- Formula index -} tr phi events = do
@@ -56,7 +61,11 @@ checkS' omk greppable enableProgressDumps idx {- Formula index -} tr phi events
   metrics <- newIORef initial
   withAsync (when enableProgressDumps $ runDisplayProgressDump initial metrics) $ \counterDisplayThread -> do
     r <- satisfiesS omk phi events metrics
-    traceWith tr $ formulaOutcome greppable phi r idx
+    if greppable
+      then case r of
+        Satisfied       -> pure ()
+        Unsatisfied rel -> TIO.putStrLn (App.prettyRelevanceArray rel)
+      else traceWith tr $ formulaOutcome phi r idx
     cancel counterDisplayThread
   where
     runDisplayProgressDump :: SatisfyMetrics TemporalEvent Text -> IORef (SatisfyMetrics TemporalEvent Text) -> IO ()
@@ -141,8 +150,6 @@ main = do
   setLocaleEncoding utf8
   options <- execParser opts
   ctx <- Map.toList . fromMaybe Map.empty <$> for options.context (readPropValues >=> dieOnYamlException)
-  putStrLn "Context:"
-  print ctx
   formulas <- readFormulas options.formulas (Context { interpDomain = ctx, varKinds = Map.empty }) Parser.name >>= dieOnYamlException
   for_ (fmap (\phi -> (phi, checkFormula mempty phi)) formulas) $ \case
     (phi, e : es) -> die $
@@ -154,6 +161,7 @@ main = do
     (_, []) -> pure ()
   let formulas' = fmap (interpTimeunit (\u -> timeunitToMicrosecond options.timeunit u `div` fromIntegral options.duration)) formulas
   tr <- setupTraceDispatcher options.traceDispatcherCfg
+  traceWith tr $ ContextDump (map (second showT) ctx)
   case options.mode of
     Offline -> do
       file <- case options.traces of
diff --git a/bench/cardano-recon-framework/app/Cardano/ReCon/TraceMessage.hs b/bench/cardano-recon-framework/app/Cardano/ReCon/TraceMessage.hs
index 190d3eba1d8..2e5214ef549 100644
--- a/bench/cardano-recon-framework/app/Cardano/ReCon/TraceMessage.hs
+++ b/bench/cardano-recon-framework/app/Cardano/ReCon/TraceMessage.hs
@@ -38,18 +38,18 @@ data TraceMessage = FormulaStartCheck {
                   -- | Formula outcomes are split into (+) and (-) as we'd like to print them at distinct severity levels,
                   --   but severity level is indexed by namespace (= constructor name), hence
                   --   we can't store both outcomes in one constructor.
-                  | FormulaPositiveOutcome { formula :: Formula TemporalEvent Text, index :: Word, greppable :: Bool }
+                  | FormulaPositiveOutcome { formula :: Formula TemporalEvent Text, index :: Word }
                   | FormulaNegativeOutcome {
                       formula   :: Formula TemporalEvent Text,
                       relevance :: Relevance TemporalEvent Text,
-                      index     :: Word,
-                      greppable :: Bool
+                      index     :: Word
                   }
+                  | ContextDump { context :: [(Text, Text)] }
 
 -- | Smart constructor.
-formulaOutcome :: Bool -> Formula TemporalEvent Text -> SatisfactionResult TemporalEvent Text -> Word -> TraceMessage
-formulaOutcome greppable formula Satisfied         idx = FormulaPositiveOutcome { formula, index = idx, greppable }
-formulaOutcome greppable formula (Unsatisfied rel) idx = FormulaNegativeOutcome { formula, relevance = rel, index = idx, greppable }
+formulaOutcome :: Formula TemporalEvent Text -> SatisfactionResult TemporalEvent Text -> Word -> TraceMessage
+formulaOutcome formula Satisfied         idx = FormulaPositiveOutcome { formula, index = idx }
+formulaOutcome formula (Unsatisfied rel) idx = FormulaNegativeOutcome { formula, relevance = rel, index = idx }
 
 green :: Text -> Text
 green text = "\x001b[32m" <> text <> "\x001b[0m"
@@ -101,6 +101,8 @@ instance LogFormatting TraceMessage where
     ,
       "index" .= index
     ]
+  forMachine _ ContextDump{..} = mconcat
+    [ "context" .= context ]
 
   forHuman FormulaStartCheck{..} =
     "Starting satisfiability check on formula #" <> showT index <> ": " <> prettyFormula formula Prec.Universe
@@ -113,19 +115,24 @@ instance LogFormatting TraceMessage where
       <> "formula: " <> prettyFormula formula Prec.Universe <> "\n"
       <> "index: " <> showT index
   forHuman FormulaPositiveOutcome{..} =
-    if greppable then "" else prettySatisfactionResult formula Satisfied
+    prettySatisfactionResult formula Satisfied
   forHuman FormulaNegativeOutcome{..} =
-    if greppable then prettyRelevanceArray relevance else prettySatisfactionResult formula (Unsatisfied relevance)
+    prettySatisfactionResult formula (Unsatisfied relevance)
+  forHuman ContextDump{..} =
+    "Context:\n" <> Text.unlines (fmap (\(k, v) -> "  " <> k <> " = " <> v) context)
 
   asMetrics FormulaStartCheck{} = []
   asMetrics (FormulaProgressDump {catchupRatio, index}) = [DoubleM ("catchup_ratio_" <> showT index) catchupRatio]
   asMetrics FormulaPositiveOutcome{} = []
   asMetrics FormulaNegativeOutcome{} = []
+  asMetrics ContextDump{} = []
 
 
 instance MetaTrace TraceMessage where
   allNamespaces =
     [
+      Namespace [] ["ContextDump"]
+    ,
       Namespace [] ["FormulaStartCheck"]
     ,
       Namespace [] ["FormulaProgressDump"]
@@ -133,11 +140,13 @@ instance MetaTrace TraceMessage where
       Namespace [] ["FormulaOutcome"]
     ]
 
+  namespaceFor ContextDump{}            = Namespace [] ["ContextDump"]
   namespaceFor FormulaStartCheck{}      = Namespace [] ["FormulaStartCheck"]
   namespaceFor FormulaProgressDump{}    = Namespace [] ["FormulaProgressDump"]
   namespaceFor FormulaPositiveOutcome{} = Namespace [] ["FormulaPositiveOutcome"]
   namespaceFor FormulaNegativeOutcome{} = Namespace [] ["FormulaNegativeOutcome"]
 
+  severityFor (Namespace [] ["ContextDump"])            _ = Just Debug
   severityFor (Namespace [] ["FormulaStartCheck"])       _ = Just Info
   severityFor (Namespace [] ["FormulaProgressDump"])     _ = Just Debug
   severityFor (Namespace [] ["FormulaPositiveOutcome"])  _ = Just Info
@@ -146,6 +155,8 @@ instance MetaTrace TraceMessage where
 
   detailsFor _ _ =  Just DNormal
 
+  documentFor (Namespace [] ["ContextDump"]) =
+    Just "Dump of the context variables supplied to the formula parser."
   documentFor (Namespace [] ["FormulaStartCheck"]) =
     Just "Formula satisfiability check has started."
   documentFor (Namespace [] ["FormulaProgressDump"]) =

From 8f035bf457a48ce178d3dd847494a7bd5d6ed58c Mon Sep 17 00:00:00 2001
From: Russoul <ruslan.feizerakhmanov@iohk.io>
Date: Wed, 6 May 2026 16:36:23 +0400
Subject: [PATCH 7/9] cardano-recon: update README and CHANGELOG for --grep and
 ContextDump

---
 bench/cardano-recon-framework/CHANGELOG.md | 3 +++
 bench/cardano-recon-framework/README.md    | 8 +++++++-
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/bench/cardano-recon-framework/CHANGELOG.md b/bench/cardano-recon-framework/CHANGELOG.md
index 335b65f53d6..4fc549f6e93 100644
--- a/bench/cardano-recon-framework/CHANGELOG.md
+++ b/bench/cardano-recon-framework/CHANGELOG.md
@@ -6,6 +6,9 @@
   converting a `Formula` and `eval` for deciding it against a single event.
 * Add `cardano-recon-grep` executable — filters a JSON array of `TraceMessage`s by a list of
   continuous formulas, emitting only the messages that satisfy all of them.
+* Add `--grep` flag to `cardano-recon` — on a negative formula outcome prints only the JSON array
+  of relevant events to stdout (bypassing trace-dispatcher); prints nothing on a positive outcome.
+* Replace the raw context printout with a `ContextDump` trace message at `Debug` severity.
 
 ## 1.1.1 -- April 2026
 * Support atoms that refer to property keys at arbitrary depth
diff --git a/bench/cardano-recon-framework/README.md b/bench/cardano-recon-framework/README.md
index efa4132081a..75661c27010 100644
--- a/bench/cardano-recon-framework/README.md
+++ b/bench/cardano-recon-framework/README.md
@@ -16,6 +16,10 @@ The application CLI takes as input:
 The application traverses the events from the given log files and checks if each given formula is satisfied by them.
 If negative, reports as such and lists the events that have been relevant to the formula.
 
+Pass `--grep` for machine-readable output: on a negative outcome only the JSON array of relevant events is written
+to stdout (bypassing trace-dispatcher), and nothing is printed on a positive outcome. This makes it straightforward
+to pipe results directly into `cardano-recon-grep`.
+
 #### CLI Syntax
 
 ```
@@ -23,7 +27,7 @@ Usage: cardano-recon FILE --mode <offline|online> --duration INT FILES
                      [--retention INT] [--trace-dispatcher-cfg FILE]
                      [--context FILE] [--dump-metrics BOOL] [--seek-to-end BOOL]
                      [--timeunit <hour|minute|second|millisecond|microsecond>]
-                     [--on-missing-key <crash|bottom>]
+                     [--on-missing-key <crash|bottom>] [--grep]
 
   Check formula satisfiability against a log of trace messages
 
@@ -43,6 +47,8 @@ Available options:
   --on-missing-key <crash|bottom>
                            behaviour when a formula atom references a missing
                            event property key (default: bottom)
+  --grep                   on formula violation print only the JSON array of
+                           relevant events; print nothing on satisfaction
   -h,--help                Show this help text
 ```
 

From 9ef39fc7005cc9b8f21a5d3b3c606ec345e5468f Mon Sep 17 00:00:00 2001
From: Russoul <ruslan.feizerakhmanov@iohk.io>
Date: Thu, 7 May 2026 15:24:23 +0400
Subject: [PATCH 8/9] Apply review suggestion regarding the cabal file

---
 bench/cardano-recon-framework/cardano-recon-framework.cabal | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/bench/cardano-recon-framework/cardano-recon-framework.cabal b/bench/cardano-recon-framework/cardano-recon-framework.cabal
index eae578820e1..247a49efdf1 100644
--- a/bench/cardano-recon-framework/cardano-recon-framework.cabal
+++ b/bench/cardano-recon-framework/cardano-recon-framework.cabal
@@ -171,9 +171,6 @@ executable cardano-recon-grep
     main-is:          Cardano/ReConGrep.hs
 
     ghc-options:      -O2
-                      -threaded
-                      -rtsopts
-                      "-with-rtsopts=-N2"
 
     build-depends:
         base
@@ -185,7 +182,7 @@ executable cardano-recon-grep
       , mtl
       , time
       , cardano-recon-framework
-      , trace-dispatcher ^>= 2.12
+      , trace-dispatcher
       , optparse-applicative
 
     hs-source-dirs:   app

From be8e51ec30cba2f379fd280b0b55accfcf563b67 Mon Sep 17 00:00:00 2001
From: Russoul <ruslan.feizerakhmanov@iohk.io>
Date: Mon, 11 May 2026 14:55:48 +0400
Subject: [PATCH 9/9] cardano-recon: address review comments (formatting,
 camelCase JSON keys)

- Use Text.unlines in prettyRelevanceArray and forHuman ContextDump
- Rename JSON keys eventsPerSecond and catchUpRatio to camelCase
- Simplify printArray to build a single Text value
- Use maybe [] Map.toList instead of Map.toList . fromMaybe Map.empty
---
 .../app/Cardano/ReCon/TraceMessage.hs              | 10 ++++------
 .../app/Cardano/ReConGrep.hs                       | 14 ++++----------
 2 files changed, 8 insertions(+), 16 deletions(-)

diff --git a/bench/cardano-recon-framework/app/Cardano/ReCon/TraceMessage.hs b/bench/cardano-recon-framework/app/Cardano/ReCon/TraceMessage.hs
index 2e5214ef549..0fa2732843c 100644
--- a/bench/cardano-recon-framework/app/Cardano/ReCon/TraceMessage.hs
+++ b/bench/cardano-recon-framework/app/Cardano/ReCon/TraceMessage.hs
@@ -66,9 +66,7 @@ prettyTemporalEvent (TemporalEvent _ msgs) ns =
 
 prettyRelevanceArray :: Relevance TemporalEvent Text -> Text
 prettyRelevanceArray rel =
-  "[\n"
-  <> Text.intercalate "\n,\n" (fmap (uncurry prettyTemporalEvent) (Set.toList rel))
-  <> "\n]"
+  Text.unlines $ "[" : fmap (uncurry prettyTemporalEvent) (Set.toList rel) ++ ["]"]
 
 prettySatisfactionResult :: Formula TemporalEvent Text -> SatisfactionResult TemporalEvent Text -> Text
 prettySatisfactionResult initial Satisfied = prettyFormula initial Prec.Universe <> " " <> green "(✔)"
@@ -84,8 +82,8 @@ instance LogFormatting TraceMessage where
     ]
   forMachine _ FormulaProgressDump{..} = mconcat
     [
-      "events_per_second" .= (fromIntegral eventsPerSecond :: Int),
-      "catch_up_ratio" .= (realToFrac catchupRatio :: Double),
+      "eventsPerSecond" .= (fromIntegral eventsPerSecond :: Int),
+      "catchUpRatio" .= (realToFrac catchupRatio :: Double),
       "index" .= index
     ]
   forMachine _ FormulaPositiveOutcome{..} = mconcat
@@ -119,7 +117,7 @@ instance LogFormatting TraceMessage where
   forHuman FormulaNegativeOutcome{..} =
     prettySatisfactionResult formula (Unsatisfied relevance)
   forHuman ContextDump{..} =
-    "Context:\n" <> Text.unlines (fmap (\(k, v) -> "  " <> k <> " = " <> v) context)
+    Text.unlines $ "Context:" : map (\(k, v) -> "  " <> k <> " = " <> v) context
 
   asMetrics FormulaStartCheck{} = []
   asMetrics (FormulaProgressDump {catchupRatio, index}) = [DoubleM ("catchup_ratio_" <> showT index) catchupRatio]
diff --git a/bench/cardano-recon-framework/app/Cardano/ReConGrep.hs b/bench/cardano-recon-framework/app/Cardano/ReConGrep.hs
index 4e795883581..78a33cecd4a 100644
--- a/bench/cardano-recon-framework/app/Cardano/ReConGrep.hs
+++ b/bench/cardano-recon-framework/app/Cardano/ReConGrep.hs
@@ -10,7 +10,7 @@ import           Cardano.ReCon.Trace.Event ()
 import           Cardano.ReCon.Trace.Feed (TemporalEvent (..))
 
 import           Control.Arrow ((>>>))
-import           Control.Monad (forM_, (>=>))
+import           Control.Monad ((>=>))
 import           Control.Monad.Reader (runReader)
 import           Data.Aeson (decodeStrict')
 import           Data.Aeson.Encode.Pretty (encodePrettyToTextBuilder)
@@ -21,7 +21,6 @@ import           Data.Text.Lazy (toStrict)
 import           Data.Text.Lazy.Builder (toLazyText)
 import           Data.Char (toLower)
 import qualified Data.Map.Strict as Map
-import           Data.Maybe (fromMaybe)
 import           Data.Time.Clock.POSIX (utcTimeToPOSIXSeconds)
 import           Data.Text (Text)
 import qualified Data.Text as Text
@@ -78,19 +77,14 @@ prettyMsg = toStrict . toLazyText . encodePrettyToTextBuilder
 
 printArray :: [TraceMessage] -> IO ()
 printArray [] = TIO.putStrLn "[]"
-printArray (x : xs) = do
-  TIO.putStrLn "["
-  TIO.putStr (prettyMsg x)
-  forM_ xs $ \m -> do
-    TIO.putStr "\n,"
-    TIO.putStr (prettyMsg m)
-  TIO.putStrLn "\n]"
+printArray msgs =
+  TIO.putStr $ Text.unlines $ "[" : map prettyMsg msgs ++ ["]"]
 
 main :: IO ()
 main = do
   setLocaleEncoding utf8
   options <- execParser opts
-  ctx <- Map.toList . fromMaybe Map.empty <$>
+  ctx <- maybe [] Map.toList <$>
     for options.context (readPropValues >=> dieOnYamlError)
   rawFormulas <- readFormulas options.formulas
                    (Context { interpDomain = ctx, varKinds = Map.empty })