Best current space lower bound for SAT?
Looks like the best bound known (for multitape Turing machines) is logarithmic.

Suppose $\delta\log n$ bits of binary worktape is enough to decide whether any $n$-bit CNF formula is satisfiable, for all large enough $n$.
By the standard simulation, a TM with $q$ states that uses at most $s$ bits of space can be simulated by a TM that has at most $qns2^s = 2^{s+\log n + \log s + \log q}$ different configurations.
Whenever the machine accepts, there is a sequence of (nondeterministic) moves reaching an accepting state that is at most as long as this number of configurations.
When $s = \Omega(\log n)$, this is at most $2^{s(2+o(1))}$ (note that $q$ remains the same for all input lengths $n$).
On a separate counter tape, $M$ can first write this quantity in unary, then at each step of the simulation erase one of the symbols of the counter, and terminate the computation if it ever runs out of counter symbols.
This creates a constant factor of overhead (something like 3), which is absorbed by the $o(1)$ term in the exponent.
Hence $2^{s(2+o(1))}$ steps are sufficient.

By assumption $s \le \delta\log n$, so the time-space product is at most $\delta\log n2^{\delta\log n(2+o(1))} = n^{\delta(2+o(1))}$.

Rahul Santhanam showed in 2001 (see doi:10.1016/S0020-0190(00)00227-1) that the space-time product for a Turing machine deciding SAT must be at least $\Omega(n^{2-o(1)})$; his argument applies also to nondeterministic machines.
Hence $\delta \ge 1$, and at least $\log n$ bits of binary worktape are needed.

More generally, additional worktapes and a larger worktape alphabet change the exponent by a constant factor.  This ultimately reduces the factor $\delta$, but the space lower bound is still $\Omega(\log n)$.