diff --git a/doc/introduction.rst b/doc/introduction.rst
index 09a23a79..12d62691 100644
--- a/doc/introduction.rst
+++ b/doc/introduction.rst
@@ -46,9 +46,8 @@ The two register-file flavors are described in :ref:`register-file`.
 The control and status registers are explained in :ref:`cs-registers`.
 :ref:`performance-counters` gives an overview of the performance monitors and event counters available in Ibex.
 :ref:`exceptions-interrupts` deals with the infrastructure for handling exceptions and interrupts,
-
 :ref:`debug-support` gives a brief overview on the debug infrastructure.
-
+For information regarding formal verification support, check out :ref:`rvfi`.
 
 
 History
diff --git a/doc/rvfi.rst b/doc/rvfi.rst
index e82aee7d..066fd29c 100644
--- a/doc/rvfi.rst
+++ b/doc/rvfi.rst
@@ -3,21 +3,16 @@
 RISC-V Formal Interface
 =======================
 
-Ibex is adapted to support the interface defined by RISC-V Formal Interface
-(`riscv-formal <https://github.com/SymbioticEDA/riscv-formal/blob/master/docs/rvfi.md>`_).
-The signals provide an insight to the state of the core.
-Generally speaking the interface decodes the current instruction.
-This includes the opcode, the source and destination registers,
-the program counter and for memory operations the memory location and data.
+Ibex supports the `RISC-V Formal Interface (RVFI) <https://github.com/SymbioticEDA/riscv-formal/blob/master/docs/rvfi.md>`_.
+This interface basically decodes the current instruction and provides additional insight into the core state thereby enabling formal verification.
+Examples of such information include opcode, source and destination registers, program counter, as well as address and data for memory operations.
 
 
 Formal Verification
 -------------------
 
-The signals provided by RVFI can be used to formally verify the adherents of
-Ibex to the RISC-V `specification <https://riscv.org/specifications/>`_.
-Currently the implementation is restricted to support the `I` and `C` extensions.
+The signals provided by RVFI can be used to formally verify compliance of Ibex with the `RISC-V specification <https://riscv.org/specifications/>`_.
 
-At the moment Ibex is not formally verified, a previous version (zero-riscy)
-was tested, but this required changes to the core as well as to the tool used
-in the process (`yosys <https://github.com/YosysHQ/yosys>`_). Support is work in progress.
+Currently, the implementation is restricted to support the "I" and "C" extensions, and Ibex is not yet formally verified.
+It predecessor "Zero-riscy" had been tested, but this required changes to the core as well as to the tool used in the process (`yosys <https://github.com/YosysHQ/yosys>`_).
+The formal verification of the Ibex core is work in progress.