I released lpnext today, an interactive and automated program verifier. (I'm not actively working on it now, but I thought it would be fun to share!)
A program verifier checks all the contracts you've defined on your program. Think "If this is true about the state of your program before running this code, Then that will be true about the state after." Verifiers take these logical statements and "push them through your program" to generate "verification conditions" as little logic programs that are run through heavily optimized automated theorem prover executables like Z3 or CVC5. (These provers are known as SMT solvers, and the logic programs are SMT-LIB scripts.) In the end, hopefully, we get a yes or a no: yes, your program always satisfies the contract; no, it could violate it; or dunno, can't tell!
Writing verified software is extremely difficult. First, you have to write your program. Second, you have to write contracts faithful to your intentions for your program. And third, you have to coerce a finnicky machine to check the contracts against your program! This often involves long cycles of refining and rechecking. lpnext is an experiment implementing an interactive mode for verification that allows one to stop and reflect on the current proof state. Systems like these can be hooked into an AI harness to perform Monte Carlo Tree Search through the space of proof scripts. For example, Deepseek Prover used MCTS to find proofs in the Lean programming language.
As for where the project stands now, ultimately I was frustrated by the performance of this class of automated systems in some moderately complex situations. Many runs end in a "dunno," and moreover it can even take a long time to get that! I've switched gears in my current work - give me reasoning that's finite, decidable, and incremental!