why3 VS sol2

With Frama-C you can prove doubly linked lists and all manner of complicated pointer manipulating graph algorithms. It does not impose a Rust-like pointer ownership policy as does SPARK.

However, for embedded development, SPARK's restrictions are a good trade-off, as the more restrictive rules allow more proofs to be fully automated than with Frama-C and simplify diagnostic messages. A fly-by-wire avionics computer doesn't need to dynamically allocate a billion graph nodes. But SPARK is not "general purpose" like C with Frama-C is.

AdaCore's SPARK tool stack is not actually written in SPARK as far as I can see, much of it is actually OCaml and Coq/Gallina for the Why3 component also used by Frama-C. See all the .ml OCaml and .v Gallina source code for yourself:

https://github.com/AdaCore/why3

And of course the compiler backend for Ada/SPARK is GNU GCC, written in unverified C:

https://github.com/gcc-mirror/gcc/tree/master/gcc/config

Compare with CompCert, the formally verified C compiler:

https://github.com/AbsInt/CompCert

Frama-C unfortunately requires a user to be mathematician-logician logic programming expert to fully utilize. One can begin training in Coq/Gallina with the large free online Software Foundations course:

https://softwarefoundations.cis.upenn.edu/

As someone said, make the game data-driven is a good first step but I will say, also have some sort of way to add additional game logic. For C++ games, lua is really easy to embed the interpreter in your C++ binary, read in the files from a directory (like /mods) with the C++ filesystem api new in C++17, and it's very easy to use SoL to write an API for lua specific to your game. Many games use lua in this way and it's probably the most common mod path setup.

I've only ever done this from C++, but it's using the same lua C library, so should be durable from C as well. You can look up how sol2 or any other wrapper libraries do it.

Consider sol2

This version relies on a Lua C++ wrapper called sol2 to hide Lua stack management from the developer, so creating new bindings can be done by adding a few lines of human-readable C++. It still has to be done manually, but at least sol2 is able to automatically figure out types of objects being bound, so it's not much different from our de-/serialization code.

Here's an example: sol2

Here is link number 2 - Previous text "Sol"

Have you considered using sol2? https://github.com/ThePhD/sol2 Or if you don't want to switch over, you can at least look at their code and see how they handle this.

It is half of a pun as I was inspired by [sol3](https://github.com/ThePhD/sol2) which is a lua <-> c++ wrapper. Sol means sun and the julia c-api prefixes all it's functions with jl, luna means moon so it is pronounced "jay luna"

If you want to be portable I'd recommend C++ and Lua, I used those for years and it runs on everything and there's this most amazing wrapper API which was a huge inspiration