The implementation

(Click on the :- button in the doc)

reverse(Xs, Ys) :-
  reverse(Xs, [], Ys, Ys).
  
reverse([], Ys, Ys, []).

reverse([X|Xs], Rs, Ys, [_|Bound]) :-
  reverse(Xs, [X|Rs], Ys, Bound).

It is tail-recursive, thus can be optimized into a loop by the compiler. Instead of keeping the elements on a stack with the depth of the list, to be collected and prepended to result list when coming back from the recursion, it constructs the result as a structure on the heap: [X|Rs] to be unified with the result variable Ys in the base case.

The Bound is there to make the call symmetric, and make sure the call fails early when both lists are of unequal length or makes sure the list are of equal length when there is one open list among the arguments. But I can't get my head around all of the special cases covered by it. Alien technology!

Consider

Instead of reverse/2 after a successful recursion, consider using the correct list processing idiom

... so that your list comes out right without you having to invoke reverse/2 after processing.

Open lists

Note that reverse/2 works for "open lists", i.e. lists for which the backbone ends in an empty cell.

Evidently a successful reverse/2 will not leave an open list behind. You just get longer and longer list on backtracking:

?- reverse([1,2,3|X],B).
X = [],                    B = [3, 2, 1] ;
X = [_3934],               B = [_3934, 3, 2, 1] ;
X = [_3946, _3934],        B = [_3934, _3946, 3, 2, 1] ;
X = [_3958, _3946, _3934], B = [_3934, _3946, _3958, 3, 2, 1] .

?- reverse(F,[1,2,3|X]).
F = [3, 2, 1],                      X = [] ;
F = [_9572, 3, 2, 1],               X = [_9572] ;
F = [_9572, _9584, 3, 2, 1],        X = [_9584, _9572] ;
F = [_9572, _9584, _9596, 3, 2, 1], X = [_9596, _9584, _9572] ;

?- reverse(F,B).
F = B,                        B = [] ;
F = B,                        B = [_17142] ;
F = [_17142, _17148],         B = [_17148, _17142] ;
F = [_17142, _18018, _17148], B = [_17148, _18018, _17142]

Reverse can ruin your day

By infinite loop on a cyclic structure:

?- reverse([1,2,3|X],X).
ERROR: Stack limit (1.0Gb) exceeded

A thought

This predicate could perform length determination/verification at the same time:

reversel(List1,List2,Length).

reversel(Xs, Ys, L) :-
  reversel(Xs, [], Ys, Ys, 0, L).
  
reversel([], Ys, Ys, [], L, L).

reversel([X|Xs], Rs, Ys, [_|Bound], Lc, Lf) :-
  succ(Lc,Ln),
  (nonvar(Lf) -> Ln=<Lf ; true),
  reversel(Xs, [X|Rs], Ys, Bound, Ln, Lf).

It can also fail early or order up reversed lists of a desired length if both lists are open. But it is slower than reverse/2 + length/2

?- Len=10000000,numlist(1,Len,L1),time(reversel(L1,L2,Length)).
% 20,000,002 inferences, 4.820 CPU in 4.841 seconds (100% CPU, 4149503 Lips)

?- Len=10000000,numlist(1,Len,L1),time((reverse(L1,L2),length(L1,Length))).
% 10,000,004 inferences, 3.530 CPU in 3.549 seconds (99% CPU, 2832708 Lips)