fare/What do Formal Methods actually Guarantee.csv

## What do Formal Methods actually Guarantee.csv

          
            Limits to Formal Methods
            What Formal Methods CAN do

            
              Formal methods are not a magic powder that you can sprinkle over your code to make it correct.
              Formal methods are a structural backbone around which you can develop more robust code.

            
              Formal methods are only methods. You still need to apply them correctly, to the right things to have useful results.
              When applied correctly, formal methods can eliminate not only single bugs, but entire classes of bugs and attacks, that your model can express as absent.

            
              Formal methods won’t prevent bugs on aspects of your code that you haven’t formalized yet.
              Formal methods can ensure the non regression of your code with respect to those classes of defects you formalized. Unlike other methods, they provide a ratchet that ensures progress even as the code evolves.

            
              Formal methods can’t eliminate bugs and prevent attacks that go below the model you use (e.g. SPECTRE attack).
              Formal methods allow you to reason at one high level of abstraction and transport your result to a lower level of abstraction, provided you also can prove full abstraction.

            
              Formal methods can’t be used to prove “everything” correct. There are always more things you could reason about.
              While there are infinite further issues, previous issues are finite and those that can be solved can be fully solved with finite effort.

            
              Formal methods suppose your domain is well-defined and limited enough to be specifiable, and that you actually understand it enough to specify it.
              Formal methods are a discipline that will ensure that you understand your domain well.

            
              Formal methods cost a lot in terms of time and talent. They cost even more as you explore new spaces that require reasoning infrastructure.
              In many applications where millions of dollars worth of assets, or even lives, are at stake, it can be even more expensive not to use formal methods.

            
              Not everyone can use formal methods.
              A large fraction of developers can be trained to use formal methods. As for those who really can’t, they are probably a liability when it comes to security-critical code.

            
              Formal methods can only prove formal guarantees, and only based on a lot of formal assumptions (axioms). And they cannot establish the informal guarantees that matter to humans.
              You can make explicit what your assumptions and your guarantees are and ruthlessly eliminate any flaw between the assumptions and guarantees.

            
              Formal methods won’t save you from having to make a lot of assumptions about the vast amount of software and hardware that you depend on under your system.
              Formal methods will prevent the multiplication of implicit assumptions you don’t know about, don’t track, and don’t check as your system evolves, that may once have been true yet will cause catastrophic errors when they stop being valid (see Ariane V).

            
              Just because it’s true doesn’t mean it’s provable. There are correct programs that formal methods can’t prove correct.
              You shouldn’t deploy an unprovable program in a setting where safety matters unless you at least have an informal proof of safety. Then, making that informal proof formal is not only possible, but doable and useful. Formal methods are not magic, but neither are informal methods.

            
              Even for the things you can prove, often you can’t afford to prove them.
              You can use formal methods strategically: study what kind of serious or catastrophic issues similar projects have had that are worth eliminating, and build your model accordingly.

            
              Formal methods can’t prove the correctness of a system that isn’t correct to begin with.
              Formal methods help you identify flaws in your reasoning, find bugs and attacks you hadn’t thought of, abandon false solutions and pursue actual solutions.
	Limits to Formal Methods	What Formal Methods CAN do
	Formal methods are not a magic powder that you can sprinkle over your code to make it correct.	Formal methods are a structural backbone around which you can develop more robust code.
	Formal methods are only methods. You still need to apply them correctly, to the right things to have useful results.	When applied correctly, formal methods can eliminate not only single bugs, but entire classes of bugs and attacks, that your model can express as absent.
	Formal methods won’t prevent bugs on aspects of your code that you haven’t formalized yet.	Formal methods can ensure the non regression of your code with respect to those classes of defects you formalized. Unlike other methods, they provide a ratchet that ensures progress even as the code evolves.
	Formal methods can’t eliminate bugs and prevent attacks that go below the model you use (e.g. SPECTRE attack).	Formal methods allow you to reason at one high level of abstraction and transport your result to a lower level of abstraction, provided you also can prove full abstraction.
	Formal methods can’t be used to prove “everything” correct. There are always more things you could reason about.	While there are infinite further issues, previous issues are finite and those that can be solved can be fully solved with finite effort.
	Formal methods suppose your domain is well-defined and limited enough to be specifiable, and that you actually understand it enough to specify it.	Formal methods are a discipline that will ensure that you understand your domain well.
	Formal methods cost a lot in terms of time and talent. They cost even more as you explore new spaces that require reasoning infrastructure.	In many applications where millions of dollars worth of assets, or even lives, are at stake, it can be even more expensive not to use formal methods.
	Not everyone can use formal methods.	A large fraction of developers can be trained to use formal methods. As for those who really can’t, they are probably a liability when it comes to security-critical code.
	Formal methods can only prove formal guarantees, and only based on a lot of formal assumptions (axioms). And they cannot establish the informal guarantees that matter to humans.	You can make explicit what your assumptions and your guarantees are and ruthlessly eliminate any flaw between the assumptions and guarantees.
	Formal methods won’t save you from having to make a lot of assumptions about the vast amount of software and hardware that you depend on under your system.	Formal methods will prevent the multiplication of implicit assumptions you don’t know about, don’t track, and don’t check as your system evolves, that may once have been true yet will cause catastrophic errors when they stop being valid (see Ariane V).
	Just because it’s true doesn’t mean it’s provable. There are correct programs that formal methods can’t prove correct.	You shouldn’t deploy an unprovable program in a setting where safety matters unless you at least have an informal proof of safety. Then, making that informal proof formal is not only possible, but doable and useful. Formal methods are not magic, but neither are informal methods.
	Even for the things you can prove, often you can’t afford to prove them.	You can use formal methods strategically: study what kind of serious or catastrophic issues similar projects have had that are worth eliminating, and build your model accordingly.
	Formal methods can’t prove the correctness of a system that isn’t correct to begin with.	Formal methods help you identify flaws in your reasoning, find bugs and attacks you hadn’t thought of, abandon false solutions and pursue actual solutions.