I believe BSV can generate formally verified adders. I will soon take a look at how it handles formal verification. This is mainly a research/investigation bug.
From what I can tell, formal is mostly applied in BSV to make sure that rules are activated once their conditions are met.
The bsc source for generating a floating point adder is here: https://github.com/B-Lang-org/bsc/blob/master/src/Libraries/Base3-Math/FloatingPoint.bsv#L1822 I'm not sure if it is formally verified.
(In reply to Yehowshua from comment #1) > From what I can tell, formal is mostly applied in BSV to make sure that > rules are activated once their conditions are met. it's... complicated. the "rules" are a bit like pre-conditions from advanced (very obscure) software engineering languages. in combination with extremely strict (strong) typing (which i can tell you from experience MASSIVELY interferes with and impedes development progress), the end result is code that is absolutely 100% guaranteed to be synthesiseable. it's actually stronger than that: because they are using Haskell, they have an internal Formal Correctness Proof that a program that compiles is 100% *mathematically* guaranteed to be gate-level synthesiseable. verilog as you know is completely incapable of making such guarantees. this tends to fit with what you've heard about it being "able to generate formally verified adders". *actual* formal verification however i believe is done slightly differently, and i've not investigated it, other than i saw a talk by Nihil for a RVF presentation, and the code that he wrote looked extremely obvious and easy to understand and read. the "magic" i expect was happening somewhere behind the scenes.