diff --git a/pallas-applying/docs/byron-validation-rules.md b/pallas-applying/docs/byron-validation-rules.md
new file mode 100644
index 0000000..59b86b3
--- /dev/null
+++ b/pallas-applying/docs/byron-validation-rules.md
@@ -0,0 +1,67 @@
+# Byron transaction validation rules
+
+Refer to the [Byron's ledger white paper](https://github.com/input-output-hk/cardano-ledger/releases/latest/download/byron-ledger.pdf) for further information.
+
+## Definitions and notation
+- ***Tx*** is the set of Byron transactions, made of a ***TxBody*** (see below).
+	- ***txSize : Tx -> ℕ*** gives the size of the transaction.
+	- ***TxBody := P(TxIn) x P(TxOut)*** is the type of transaction bodies, each one composed of some inputs and some outputs.
+		- ***txBody : Tx → TxBody***.
+		- ***TxOut := Addr x Lovelace*** is the set of transaction outputs, where
+			- ***Addr*** is the set of transaction output addresses.
+			- ***Lovelace := ℕ***.
+			- ***txOuts : Tx → P(TxOut)*** gives the set of transaction outputs of a transaction.
+		- ***TxIn := TxId x Ix*** is the set of transaction inputs, where
+			- ***TxId*** is the set of transaction IDs.
+			- ***Ix := ℕ*** is the set of indices (used to refer to a specific transaction output).
+			- ***utxo : TxIn → TxOut*** gives the unspent transaction output (UTxO) associated with a transaction input.
+			- ***txIns : Tx → P(TxIn)*** gives the set of transaction inputs of a transaction.
+				- We write ***txIns(tx) ◁ utxo := {to ∈ TxOut / ∃ ti ∈ dom(utxo): utxo(ti) = to}*** to express the set of unspent transaction outputs associated with a set of transaction inputs.
+	- ***fees: Tx → ℕ*** gives the fees paid by a transaction, defined as follows:
+		- ***fees(tx) := balance (txIns(tx) ◁ utxo) − balance (txOuts(tx))***, where
+			- ***balance : P(TxOut) → ℕ*** gives the summation of all the lovelaces in a set of transaction outputs.
+
+- **Serialization**:
+	- ***Bytes*** is the set of byte arrays (a.k.a. data, upon which signatures are built).
+	- ***⟦_⟧<sub>A</sub> : A -> Bytes*** takes an element of type ***A*** and returns a byte array resulting from serializing it.
+- **Hashing**:
+	- ***KeyHash ⊆ Bytes*** is the set of fixed-size byte arrays resulting from hashing processes.
+	- ***hash: Bytes -> KeyHash*** is the hashing function.
+	- ***addrHash<sub>utxo</sub> : TxIn -> KeyHash*** takes a transaction input, extracts its associated transaction output from ***utxo***, extracts the address contained in it, and returns its hash. In other words, given ***utxo*** and transaction input ***i*** such that ***utxo(i) = (a, _)***, we have that ***addrHash<sub>utxo</sub>(i) := hash(a)***.
+- **Protocol Parameters**:
+	- ***pps ∈ PParams*** is the set of (Byron) protocol parameters, with the following associated functions:
+		- ***minFees : PParams x Tx → ℕ*** gives the minimum amount of fees that must be paid for the transaction as determined by the protocol parameters.
+		- ***maxTxSize : PParams → ℕ*** gives the (global) maximum transaction size.
+- ***Witnesses***:
+	- ***VKey*** is the set of verification keys (a.k.a. public keys).
+	- ***SKey*** is the set of signing keys (a.k.a. private keys).
+	- ***Sig*** is the set of signatures (i.e., the result of signing a byte array using a signing key).
+	- ***sig : SKey x Bytes -> Sig*** is the signing function.
+	- ***verify : VKey x Sig x Bytes -> Bool*** assesses whether the verification key applied to the signature yields the byte array as expected.
+		- The assumption is that if ***sk*** and ***vk*** are, respectively, a pair of secret and verification keys associated with one another, then ***sig(sk, d) = σ*** implies that ***verify(vk, σ, d) = true***.
+	- ***wits : Tx -> P(VKey x Sig)*** gives the list of pairs of verification keys and signatures of the transaction.
+
+## Validation rules
+Byron phase-1 validation is successful on ***tx ∈ Tx*** if and only if
+
+- **The set of transaction inputs is not empty**:
+
+	<code>txIns(tx) ≠ ∅</code>
+- **The set of transaction outputs is not empty**:
+
+	<code>txOuts(tx) ≠ ∅</code>
+- **All transaction outputs contain non-null Lovelace values**:
+
+	<code>∀ (_, c) ∈ txOuts(tx): 0 < c</code>
+- **All transaction inputs are in the set of (yet) unspent transaction outputs**:
+
+	<code>txIns(tx) ⊆ dom(utxo)</code>
+- **Fees are not less than what is determined by the protocol**:
+
+	<code>fees(tx) ≥ minFees(pps, tx)</code>
+- **The transaction size does not exceed the protocol limit**:
+
+	<code>txSize(tx) ≤ maxTxSize(pps)</code>
+- **The owner of each transaction input signed the transaction**: for each ***i ∈ txIns(tx)*** there exists ***(vk, σ) ∈ wits(tx)*** such that:
+	- <code>verify(vk, σ, ⟦txBody(tx)⟧<sub>TxBody</sub>)</code>
+	- <code>addr_hash<sub>utxo</sub>(i) = hash(vk)</code>
diff --git a/pallas/src/lib.rs b/pallas/src/lib.rs
index 29b6cd2..330d0b2 100644
--- a/pallas/src/lib.rs
+++ b/pallas/src/lib.rs
@@ -49,4 +49,6 @@ pub mod storage {
     pub use pallas_rolldb as rolldb;
 }
 
+#[doc(inline)]
+#[cfg(feature = "unstable")]
 pub use pallas_applying as applying;