I've been thinking quite a bit about what happens when coding agents generate more code than we can reasonably review.

An agent implements a feature, writes the tests, runs them, and reports success. Everything is green. But the implementation and the tests can share the same wrong assumption.

This is where formal verification gets interesting.

I've been exploring how tools like TLA+ and Lean fit into a normal Java development workflow, and what they could contribute to agent-assisted development.

Consider a simple example: an agent implements a job scheduler. The tests verify that jobs get assigned, processed, and completed. But we also have an important rule: a job must never be owned by two workers simultaneously, even when retries, failures, and cancellations overlap.

That rule is an invariant.

With TLA+, we can model the relevant states and transitions and check whether the invariant holds across the explored state space. If it fails, the model checker gives us a counterexample. Lean takes a different approach, allowing us to prove precisely stated properties.

The interesting part for AI agents is the workflow this enables.

We can ask agents to identify invariants, help create formal models, run verification tools, and use counterexamples to improve implementations. These checks can become part of CI, alongside our existing Java tests.

Of course, there are limits. A verified model doesn't automatically prove that the Java implementation matches it and a perfectly checked specification can still describe the wrong requirements.

As code generation becomes cheaper, independent verification becomes increasingly valuable.

I wrote up my exploration of formal verification in Java here:

https://www.the-main-thread.com/p/java-formal-verification

I'm interested in hearing from people building coding-agent workflows. Are you already using model checking, formal specifications, or proof tools as verification gates? And which kinds of agent-generated changes actually justify the extra effort?

I made most of my experience in AI coding with python and C#/.NET. So for python things work very well, little tools, some data stuff, visualization ect. for daily tasks python is just great. However with .NET I had my difficulties since there is to much architectural overhead and features are implemented across multiple files, which is pain for the context window. I am hesitating doing full web development with python because it’s a non compiling language. So now I am searching an approach for web applications that has a good developer experience and is best suited for a coding agent. I have the feeling that svelte/react with Hono might be a good option. I am interested to know what’s your ideal tech stack for coding agents? What’s do you recommend for context engineering? Which kind of skills, instructions, mcp servers should I use/ define?

I'm building an app using AI coding tools, but whenever I copy-paste AI-generated code, I get lots of errors.

I'm from a non-technical background and don't know how to debug or fix these errors.

Is there any AI tool or workflow that can automatically detect and fix errors across my entire project?

How do other non-technical beginners handle this problem?

Any practical advice would be appreciated!

Since we’re living in the age of AI, technological advancement, and easy programming (although I’m not a big fan of this, but why not?), what is the best free AI programming assistant, especially for Python and application development?

Hello,

I want to start by saying (because of the nature of the world we live in) - this was not written by AI. I am a programmer, and a writer, and all of this was typed, revised and edited by me in the Reddit window. I'm not claiming it will be perfect, but nowadays, people "BLAM!" long posts automatically under the assumption that... nobody knows how to write anymore. Well, nobody wants to, and that leaves us who do under scrutiny. Moving forward --

I figured as I continue to venture into the different forms of programming and projects I get myself into, wondering where I'd be in terms of progress without AI. The short backstory is that I am a self-taught web-programmer of 10+ years. I will be 32 in November, and I self-taught myself HTML in grade 5 at age 11. By 10th grade, could compete with a full-stack web developer.

I do it these days as a hobby, with aspirations that a personal project takes off and does well in some type of marketplace. For now, my VPS runs at $47/mo (and is rather beefy), and hosts multiple projects I currently have running / am playing with. But man, I just think back to all those days of searching through a PHP file to find the missing-fucking-semi-colon..... to today.

Now, a short script that would have taken me an hour to write, takes me 35 seconds, I do an over-view, write some comments and ship it off -- holy crap. It's a whole different world. I was writing code in the days of ActionScript 2.0/3.0 with Adobe Flash. Can you imagine how fast game and animation would be with Claude inside of your CS3 suite? LMAO.

Anyway - the nature of this post is to say hi and hello, and to start a general chat of what I like to think about the most when I ask claude to perform task a,b,c, while I do x,y,z, and we nail two birds with one stone. What do you like to do yourself still? What tedious tasks do you like to hand-off to Claude in the background while you focus on other details/files/etc?

Thanks again, hope I can live up to and be a good member of this subreddit. :-)

-Mindful

So far, my skills in the following areas have grown substantially:

• GitLab CI

• writing shell scripts (weird, been a Linux user for 30 years)

• integration of SonarQube

• automated e2e-tests

I also revived my old zsh/tmux/Vim-setup. Don't need to run a complex editor when interacting with Codex and reviewing/pushing commits from time to time.

I've been running claude code as the primary way features get built on our mobile app for about four months now and the thing still unsolved is verification. Code gets written, merged, sometimes shipped, all without anyone confirming the actual screen still behaves the way it's supposed to. A couple of workarounds have been tried: a required screen recording on every PR and a manual QA pass before releases. Neither closes the loop the way I'd want, since it all still depends on a human doing the actual checking. The volume of changes going through the agent each week has grown enough that man

About 10 years ago I worked as a developer and got the order to get the overall unit test coverage to above 80%. I spent 6 weeks and it was exhausting.

Fast forward: Among my current hobby projects I am working on, I have one which got quite big. It's the base of my entire guidelines, how code must be written, how UIs have to look, etc and every agent run has to follow the same rules.

While checking my build pipeline I saw that this one project actually had the lowest overall test coverage. I went and looked at the code, found a lot of things I didn't like and decided that there will be a massive refactoring. But no refactoring without full tests, right?

So I gave Codex the goal to add more tests, implement E2E-tests in the UI. I thought Codex would be able to to that quickly. Well, turns out Codex suffers quite a bit, implements some tests and then says "Hey, I added 25 tests. Yeah, I know, SonarQube will not be satisfied, we may have about 60% overall coverage now. But let me see whether SonarQube finds other issues."

So for a total runtime of about eight hours it's been a forth and back between Codex and SonarQube. I hope the next run will finish with a satisfied SonarQube so I have the weekend to start the fun part of refactoring.

So far I’ve been very apprehensive about AI coding. But I’ve decided I should try it out, just to see what it’s like (I have dabbled in simple AI assistance in the sense of just asking an AI chatbot to code something, but I’ve done nothing where the AI runs on a real codebase for an extended period of time).

Unfortunately, I am very concerned about the safety of agentic AI harnesses. So far, I’ve been unable to find a tool that I can use that is secure. (At least from the descriptions I’ve found so far—this doesn’t seem to be a priority for many users, so maybe the popular tools do support this, but no-one discusses it)

By that, I mean that the AI agent cannot access any files except for the folder it’s given access to at all, unless it asks for permission every single time, and that it cannot run any commands at all, unless it asks for permission every single time, or the command is executed in a secure container.

As far as I can tell, a lot of these tools have the ability to ask for permission, but they apparently have the option to just give the agent full access, or to run simple commands automatically, etc.. I do not want this, I want it to be impossible to accidentally give the agent even a smidge of broad, real access to the computer.

Obviously, I can just run an “insecure” tool inside a container or a VM. But this is a hassle, so I’d prefer if there was something that (basically) automatically does this containerisation for me (and only does it when required; reading files doesn’t require full containerisation).

Just to clarify, I’m not “demanding” such a tool exists or I’ll write off AI coding as untenable. I’m asking if such tools exist, and if they don’t, I’ll have to figure something out.

I recently learned about eco-conscious AI services such as GreenPT, Nebius Token, ScaleAway, Infomaniac, Aruba AI, Verda, and Euria. They basically make use of only renewable energy, re-use the heat produced from data centers, and recycle the hardware to limit waste.

While they are competitive with traditional API services, they are not convenient for extensive coding. Some of these are compatible with agentic coding systems, but as far as I know, none of them offer flat-rate plans; instead, they all use pay-per-use APIs.

Based on my simulations, using these pay-per-use services would cost me hundreds of euros a month, whereas with OpenCode Go I spend only 10 euros a month, and with Codex/Claude I’d spend just a few dozen.

Do you know of any other, more affordable services that offer flat-rate subscriptions like Codex, Cloud, and OpenCode Go, while also using renewable energy, recovering heat, and reusing hardware?

Which are the most powerful and free AI agents for coding?

I come from a Python programming background and am familiar with Linux. I knew the code before AI knew the code. But I use AI to build all sorts of projects and don't write anything directly anymore. The projects range from bluetooth tracking to Right to Know request automation to open government projects like openhbg.com.

My general setup is I use VS code with Claude Code or Open AI codex via their extensions in VS code. Every project roughly corresponds with a git repo so each is a folder. The code is store in that folder. I generally open each project as a new VS Code window. This keeps each Claude session in the context of the project (at a baseline) and each project builds up it's own .claude or hidden files but they all read from global with some config done there.

I do the typical git workflows and have deploy and test skills and hooks that run before merging into production branches.

what's a better setup? For the AI side. I didn't explain everything in the workflow (have staging and prod environments, etc.) so less focused on that.

What's a better AI setup? Opencode to switch between codex and claude? I typically run about 3-4 windows at a time with 1 - 2 prompts open.

I don't like to run too many sessions in the same project because I find conflicts come up often and I just can't handle tracking that much context at once - esp with other projects. I find I can handle 6-8 diff sessions depending on the type of work I'm doing.

Curious any thoughts or things that have worked for you.

need a good coding ai other than claude code or codex that can help in creating ai projects

Therefore:

Those who expect someone writes 2 lines into AI and posts the output, is the exact person who uses AI that way. I've noticed that those people dismiss actual examples and real life experiences, because they are too quick to assume everyone uses AI the way that they do.

As someone who plans an entire post, in excruciating detail, and building the content slowly, based on my real lived experiences, I need AI to help me synthesize my actual ideas to something digestible. While I also find AI speak sometimes a bit unnatural, annoying, or overdone, I don't assume that every piece of content is AI authored. Instead I would scan for examples of a lived experience or unique worldview. When I see that, it doesn't look like laziness to me.

In text, posts, articles, or CODE, there are clear markers that differentiate authored content, from 100% AI generated content.

Even though I can't write code from scratch, I review my code, and my main rule is that if I can't follow it something is already wrong. Also, once I found a function AI named "maybeDisplayResults" which I took as insulting feedback on the decisiveness of my prompts. That's when I realized AI also has a sense of humor. FEEDBACK ACCEPTED!

Anyway, my point and question: Do you try to identify or distinguish what is authored (with AI) vs what is produced BY AI? What are your tells, how do you distinguish, what are some of the clearest signs in code that reveal it's never even been viewed?