Is there any solution to write C code free from undefined behavior and vulnerability without paying for any tools?
You can use Frama-C open-source toolset, notably its (Evolved) Value Analysis and WP plug-ins:
Value analysis is more used to prove absence of undefined
behavior, while WP could be used to prove functional properties.
Of course, proving complex system-wide properties like in seL4
needs another toolset (Isabelle, Haskell, ...).
Both Value analysis and moreover WP are complex tools, so you need some practice to use them. But you'll find good documentation and tutorials on the web, e.g.:
Best regards,
david