This is not a technical question, I hope this community has a room for such questions, but I will delete it in case this is inappropriate.

It has been experimentally observed (e.g. here) that when choosing a $3$-SAT formula by the following process:

On input $(n, \alpha n)$: choose $\alpha n$ clauses uniformly at random from the set of all clauses of $3$ literals over $x_1, \ldots, x_n$, and return the conjunction of these clauses.

The probability that the outputted formula is satisfiable depends on $\alpha$: if $\alpha << c$ the probability is very close to $1$, and if $\alpha >> c$ the probability is very close to $0$ (it has been observed for a general $k$-SAT instances).

My question is what is the theoretical understanding of this problem? To the best of my knowledge, for other problems it is possible to prove similar claims quite easily (e.g. the probability that a random graph $G(n,p)$ has a clique of size $4$ is almost $1$ when $p(n) = \omega(n^{-2/3})$ and is almost $0$ when $p(n) = o(n^{-2/3})$, and it can be proven by a basic use of second moments).

However, for SAT I couldn’t find proofs. Do you know of any progress in this problem?