There are many approaches for verifying linked structures---arguably, more suitable than the B method---that you might want to use, depending on the language and properties you want to verify. Most of the approaches rely on separation logic (which was in big part motivated for verification of linked structures).

Some tools include:

• Full Functional Verification of Linked Data Structures -- where you write Java code with specifications in classical higher-order logic, while the verifier uses integrated reasoning of multiple different provers
• Linked list, imperative separation logic in Isabelle -- uses separation logic in Isabelle theorem prover (other similar data structure examples might be found in the archive of formal proofs)
• Dafny: A Language and Program Verifier for Functional Correctness -- which allows specifying and verifying wide range of data structures in C# (many examples for linked lists exist, e.g. this one)

To quote this answer (which answers a very similar question), even though you did not give details about what are you trying to verify, it seems that properties you might want to prove about the "reverse linked list" might be formulated as properties for a regular linked list. (If the reverse list requires some additional (non-standard) implementations, not already declared for the linked list, you might be able to model those in addition.)

I am not sure what was the purpose of your example, but your code seems similar to an example of modelling a linked list with B (which includes other standard operations) method in Program Development by Refinement Case Studies Using the B Method.

There are many approaches for verifying linked structures---arguably, more suitable than the B method---that you might want to use, depending on the language and properties you want to verify. Most of the approaches rely on separation logic (which was in big part motivated for verification of linked structures).

Some tools include:

• Full Functional Verification of Linked Data Structures -- where you write Java code with specifications in classical higher-order logic, while the verifier uses integrated reasoning of multiple different provers
• Linked list, imperative separation logic in Isabelle -- uses separation logic in Isabelle theorem prover (other similar data structure examples might be found in the archive of formal proofs)
• Dafny: A Language and Program Verifier for Functional Correctness -- which allows specifying and verifying wide range of data structures in C# (many examples for linked lists exist, e.g. this one)

To quote this answer (which answers a very similar question), even though you did not give details about what are you trying to verify, it seems that properties you might want to prove about the "reverse linked list" might be formulated as properties for a regular linked list. (If the reverse list requires some additional (non-standard) implementations, not already declared for the linked list, you might be able to model those in addition.)

I am not sure what was the purpose of your example, but your code seems similar to an example of modelling a linked list with B (which includes other standard operations) method in Program Development by Refinement Case Studies Using the B Method.