If you are asking me personally, my verification experience has been a mixture of manual tests, and writing test scripts in either Python or a custom in-house l

If you are asking me personally, my verification experience has been a mixture of manual tests, and writing test scripts in either Python or a custom in-house language. These scripts run in an avionics simulation environment, in which typically there is one avionics component under test, which is running either a desktop build of its code, or running as the actual hardware unit, attached to a desktop via Ethernet or ARINC 429 connections. The other avionics components are then either simulated, or, as needed, running actual code. (The majority of my avionics work has actually been directly working on such simulation systems, building and certifying them for formal verification use, but I have done some verification work on avionics boxes as well.) Outside of my personal experience, I am aware of projects using things like TLA+. I suspect that is more common the higher up you go in system criticality. Even within avionics, not every system requires the same level of scrutiny... for example, you need to more exhaustively test a flight controls system than a flight management system. In any case, the FAA does not dictate particular tools. They dictate a level of quality that any tools used must adhere to (the tools themselves must be certified based on how they are used), but otherwise a project is welcome to use whatever tools they wish. Or, no tools.