The current trend to globalize the supply chain in the Integrated Circuits (ICs) industry has raised several security concerns including, among others, IC overproduction. Over the past years, logic locking has grown into a prominent countermeasure to tackle this threat in particular. Logic locking consists of "locking" an IC with an added primary input, the so-called key, which, unless fed with the correct secret value, renders the ICs unusable. One of the first criteria ensuring the quality of a logic locking technique was the output corruption, i.e., the corruption at the outputs of a locked circuit, for any wrong key value. However, since the introduction of SAT-based attacks, resulting countermeasures have compromised this criterion in favor of a better resilience against such attacks. In this work, we propose SKG-Lock+, a Provably Secure Logic Locking scheme that can thwart SAT-based attacks while maintaining significant output corruption. We perform a comprehensive security analysis of SKG-Lock+ and show its resilience against SAT-based attacks, as well as various other state-of-the-art attacks. Compared with related works, SKG-Lock+ provides higher output corruption and incurs acceptable overhead.