Feferman-Schütte ordinal is sometimes said to be:
....first impredicative ordinal, though this is controversial, partly because there is no generally accepted precise definition of "predicative". Sometimes an ordinal is said to be predicative if it is less than $Γ_0$.
Now Nik Weaver introduces a formal system called Tarski-something-something which I do not even understand.
As I searched it seemed there has been a correspondence between Nik Weaver and Solomon Feferman which is linked here. At this stage, the concept has become highly abstract for me to understand.
Has any research been done on formalizing the concept? And does the vicious circle principle inhibit from "sort of" going beyond the "system", (intuitively speaking of course)? I am cognizant of Takeuti's ordinal diagram, which again is beyond scope of my understanding at this phase.
Also, how accepted is Nik Weaver's formal system of Tarski? Can one formalize predicativity without invoking vague, philosophical notions?
Edit: As I was searching I found that a question of this nature was asked in Discussion in nLab