Nope! Not a troll question. At the end of the day, we're human beings interacting with a bunch of electrified rocks. There will always be a layer of subjectivity and expertise involved in translating informal (or perhaps even unknown) desires into formal specs. It gets even worse when you are designing software that needs to take into account the underlying behavior of hardware; you wouldn't program an autopilot for a jumbo jet whose certification only exists in the context of some simplified formal model for how computers work, do you?
But I'm catastrophizing. If you think going through the definitions of a spec are painstaking and require expert insight to get right, it is miniscule compared to e.g. auditing every line of a codebase written in an imperative language. And not only that, to even get close to the same correctness guarantees of e.g. a formally verified pipeline through CompCert, you would have to audit every line of the codebases of every compiler that touches your code (https://r6.ca/blog/20200929T023701Z.html "It Is Never a Compiler Bug Until It Is"), together with analysis of the underlying hardware models.
All this to say, technology is more complicated than traditional programmers exposed only to high-level languages might be led to believe. That complication can only be reduced, consolidated, or blackboxed so much.
Yeah Lean is actually pretty interesting in that sense because it’s designed to have a small kernel that actually does the type theory checking, and that kernel has a specification, tests, and independent reimplementations. The kernel really is very small compared to the entirety of Lean syntax and behavior — everything else runs and is elaborated before stuff feeds into the kernel. So the surface area for actual proof checking bugs is greatly reduced.
Yeah, the goal for formal methods boils down to only two things: reduce surface area necessary for auditing (e.g. high-level Lean theorem and definitions file), and consolidate that surface area into preexisting, pre-audited technologies (e.g. the Lean kernel).