Looks like v3.0 just dropped, though after a very cursory glance at the release notes, I wonder what motivated the major bump specifically.
I deploy on a single machine with Docker, as my apps are both small scale and non-critical (people pay for them though). Kubero popped up when I researched how I would do a multi-server setup should the need for High Availability arise. It might flatten the learning curve and drop the operational overhead of Kubernetes enough to push me in this direction.
As for running the cluster myself, I probably would try to run K8s on talos.dev as well.
I will peruse your learning path when I am done with writing my master's thesis. Thanks for putting it together!
Lots of bullet points and keywords about the "What" : provable recursion, next-token prediction, and formal verification... and all items in "What makes it special". Can you provide a practical motivation, even speculative for people like me who have little time? Not necessarily "What use does it have right now", but "The qualitative difference with other models might enable use case XYZ in the future".
I have noticed it is low power and this is great in itself. What does the more rigorous formalism bring to the table? No snark at all, I am fascinated by formal methods, but still looking at them from afar.
Thanks for the thoughtful question— and good luck wrapping up the thesis!
Here’s the shortest road-map I can give for why the heavier formalism matters once you already have low-power execution nailed down.
First, the grammar + proof layer lets you guarantee properties that today’s neural LLMs can only hope to satisfy. Because every production rule carries a machine-checkable proof obligation, you can show that responses will always terminate, stay within a memory budget, or never emit strings outside a whitelisted alphabet. In practice that means the model can be certified for safety-critical or compliance-heavy settings where a probabilistic network is a non-starter.
Second, the same proofs make the system auditable and patchable by domain experts instead of ML engineers. An agronomist can inspect the maize-disease module, see that the recursion proving “all advice paths end with a referenced citation,” and swap in an updated pest table without breaking that guarantee. The edit-compile-prove cycle is minutes, not GPU-months.
Third, formal hooks open the door to hybrid workflows. You can embed the micro-LM inside a larger pipeline—say, a standard transformer model proposes a draft, and our verified core acts as a “lint pass” that repairs grammar, checks facts against a local SQLite cache, and signs the result with a proof artifact. That could be huge for regulated industries that want the creativity of big models and the certainty of formal methods.
Finally, on the speculative side, once responses are proof-carrying you can imagine device-to-device marketplaces of small, composable skills: my weather module proves bounds on forecast error, your SMS gateway proves it redacts PII, we link them and the combined proof still holds. That’s hard to do with opaque neural weights.
So the low-power story gets us in the door; the rigorous formalism is what keeps the door open when reliability, certification, or composability become the bottleneck. Hope that gives you a clearer picture—and when the thesis dust settles I’d love to hear your perspective on how formal methods could push this even further.
My work is about inferring solutions to Constraint Satisfaction Problem by using belief propagation in the corresponding constraint network, a few keywords caught my eye here :)
Do you have any illustrative example so I can understand better what you are hinting at?
Not exactly the approach your describing, but Futhark[0] offers an alternative to CPU execution, it compiles to CUDA or OpenCL to run on GPU (or multi-threaded CPU).
That one I am aware of, as language geek, I am always curious to GPU alternatives that aren't always the same old story only C and C++ get to party, which is actually an advantage of CUDA's polyglot approach.
Is the amount of data transfer the main reason to use JSON or do you find Web Components play better with JSON payloads? I could imagine the template string being rendered on the server, fetch()-ed by the client and swapped with this.innerHTML.
Do you manage any amount of cross-component state? It's one use case where JSON would win over "HTML over the wire".
> I suspect that all the free hobbyist FOSS labor artificially depresses dev salaries, hurting everyone else. Otherwise, the FAANGs would have to hire people to replicate what they currently get for free.
The way I see it, FOSS enables a ton of smaller entities to launch products when they would not have the capital otherwise (see: anything built on Django). Those represent a lot of jobs too! This could be the software version of the Jevons Paradox.
Megacorp are a different problem. They do contribute back to the commons, but this seems like a drop from the bucket of the quintillion dollars they represent. Is it fair? That's a moral judgement, because software being FOSS means its legal in any case.
This is a good line of thinking, and you're right that smaller entities get the benefit of software they couldn't otherwise afford.
Of course, a more directly equitable arrangement would be a software co-operative. If prices are tied to usage, then everyone should be able to afford to fund a FOSS project's development at whatever level they can bear.
Eventually-open-source commercial licenses are already a bit like this, in that those who can pay, do so, and those who want it for free, can still get it, albeit delayed by a couple years. Ditto for projects that are funded by bounties, where only funders get access up to some dollar amount, after which it's FOSS to all.
> Moreover, well-known algorithms for linear programming like simplex and primal-dual methods have straightforward (and illuminating!) combinatorial interpretations when restricted to minimum-weight bipartite matching.
I you have any resource illustrating this point, please share. I would be very interested.
I liked this video [0] about how the Hungarian Algorithm is a particular case of the primal-dual method and I am eager to dig further.
This was a popular topic in '80s linear programming books. Chvatal's "Linear programming," for instance, is carefully-written and devotes about 100 pages devoted to network simplex. Papadimitriou and Stieglitz's "Combinatorial optimization: algorithms and complexity" explicitly goes through primal-dual derivations of algorithms for shortest path, max flow, and min-cost flow (including bipartite matching). I haven't read it in any detail, but https://math.mit.edu/~goemans/PAPERS/book-ch4.pdf is online and might be to your liking.
I deploy on a single machine with Docker, as my apps are both small scale and non-critical (people pay for them though). Kubero popped up when I researched how I would do a multi-server setup should the need for High Availability arise. It might flatten the learning curve and drop the operational overhead of Kubernetes enough to push me in this direction.
As for running the cluster myself, I probably would try to run K8s on talos.dev as well.
Congrats on an inspiring project!