Programming

the cryptography module has unit tests and formal verification.

I suspect your formal proof refers to the following files: https://github.com/positive-intentions/signal-protocol/tree/staging/formal-proofs

It contains 6 files each with less than 100 lines of code, and the claim seems to be it almost prove the entire security of the signal protocol.

There are three possiblities here: (1) the formal proof community has advanced so much without me knowing (2) your AI produced complete garbage (3) your AI made ground breaking advancements in formal method. Since my best known state of the art is Signal* from project everest. It involves tens of components, and years of works for top academics and proof engineers.

• Here is the website: https://project-everest.github.io/
• Here is the paper: https://www.computer.org/csdl/proceedings-article/sp/2019/666000b256/1dlwheTvbEI
• Here is the code: https://github.com/Inria-Prosecco/libsignal-protocol-wasm-fstar

Each file here, like fstar/Impl.Signal.Core.fst would already be longer than your entire proof, even just the hints provided to the SMT solvers fstar/Impl.Signal.Core.fst.hints are longer than your entire proof.

So I am interested in what technique did you apply to acheive the almost same effect as this monumental project with less than 5% of the code?

You have also claimed there is support for Rocq, Lean, and F*, and the code is here https://github.com/positive-intentions/signal-protocol/tree/staging/signal-protocol-core/proofs

I looked into the Rocq and Lean part of the proof, and there is no proof, all the "correctness" claims are all declared as axioms, which are not proven.

So far, I have sit down and read your code, and I feel it is either a major breakthrough or a complete waste of my time (I am unfortunately leaning towards the latter). I would be furious if my student or colleagues handed me a work of this quality, and I imagine all the experts reading your code will likely feel the same.

I am not angry because your work involves LLM (I don't like that, but I won't be angry about it), but because you disrespected my time and effort to review your code by not putting out a product of reasonable quality. In turn, I also cannot provide you constructive and technical feedback to you, as the technical part of your project seems hollow to me. IMO, disrespecting the time of your peer is a very good reason to ban people from their community.

Academia is currently being flooded with AI, many are used by compotent individuals so AI is able to hide error in obscure process. For the first time, academia need to deal with a large amount of submission are not in good faith, and that is frustrating for us volunteering reviewers. Your reader, who are also volunteering their time to help you improve, will likely feel the same.

AI is just a tool, that is, you will get as much expertise out of it as you put into it. Like a computer, it will make producing work easier and faster, but it cannot help you build anything you do not understand yourself.

I am glad you are interested in crypto and verification. But to make meaningful contribution will take honest effort as opposed to just prompting a couple so called artificial "intelligence".

I can and I will.

I think you need to speak to a mental health specialist, because AI psychosis can be really destructive. We all have problems, but using chat bots to make us feel better is dangerous for you and those around you, even if it feels good in the moment. These bots are designed to tell you exactly what you want to hear so that you become addicted to them.

I'm going to guess you didn't accomplish much as a software engineer before AI? The personal deficiencies at the core of that are still there even if you use AI to tell you otherwise. I won't speculate what those deficiencies are, but I just want you to engage in some honest introspection. Absolutely nobody will trust someone like you to handle such a sensitive topic like cryptography. Stop wasting your short time on this earth on something so stupid. Go make literally anything else.

I've read some other comments and wanted to add.

You cannot use a LLM to verify its own work

They have no ability to think. Any intelligence they have is extremely limited. There a mostly automatic copy and paste machines. They pull code from their training data and online and attempt to compose the.

Using a LLM to verify its own work is like asking a criminal to run their own trial.

That's just now any of this works. I think you should take a step back from the LLM and really start evaluating your work more critically. There is more to software then "it works!"

Cryptography is notoriously easy to get wrong. If you don't know enough about it - you should not offload it to the hallucination machine, because you will not be able to verify it properly, and those who can - will not bother to.

This is not what a real audit looks like and it should not be presented as such. This "audit" is, in fact, slop.

Auditor: Security Analysis (Automated + Manual Review)

Do you not see the problem in this line?

The implementation uses real cryptographic primitives

Or this?

I avoid slop code like yours because typically the user of the slop generator has no real idea of how things actually work, the slop is over-"engineered", and it's likely full of security issues. Further, it also wastes tons of resources just for poorly written slop.

I especially wouldn't ever touch your cryptographic slop.

In my opinion, slop is slop. AI tends to result in slop, but it doesn't have to. But to ensure it's not slop, one has to put in effort and time. Which kind of defeats the purpose of using AI in the first place. So I think it's obvious why most people default to AI involvement = slop.

Unless you invented some new form of encryption why are you generating so much ai slop?

Just reuse human made cryptography libraries that are battle tested. Then you won't have to do disastrous things like putting ai to review your ai slop.

You know that it lies, gaslights, writes or deletes production databases, tests etc as it pleases.

No matter how hard you pet your LLM, this project is not your work. LLM output attribution is a gray zone by design. Your assumption that vibe coding has overtaken software development is a big red flag imho. I wonder where you've acquired this belief. If you've been banned from multiple communities already I recommend you reflect upon this.

I don't think everything is getting called ai slop, but I would say if any part of your project is ai slop (like your "lazy uis") I'd also immediately lose trust in the entirety of the project, especially if it's intended to be around security. I do think most projects that use AI for code generation are slop though, I've seen far fewer examples of good use (i.e. where the output looks human written because the operator reviewed and refactored every part of it, or where it was used to write small parts of functions rather than entire functionalities)

Your last sentence I think provides a great argument for why people here (and more and more broadly in engineering) hate on ai generated code in general. It produces such vast quantities of code (and often unnecessarily) that it becomes infeasible for a human to review it, immediately requiring us to place trust in the machine to both generate it and review it, and to continue maintaining it while the human operator probably does not even have full understanding of what's changing. A machine, that we all know hallucinates and generates often low quality garbage, including severe security vulnerabilities by design. According to GitHub, your project has millions of lines of changes on a weekly basis in the earlier days, that does scream slop to me.

Last, AI is more and more hated due to the increasing number of horrible impacts it has on our world, personally I'd not support AI generated projects just on that principle alone.

Yes we can. Watch me

look I'm all for using LLMs for tedious or straight forward transformations of easily verifiable logic. The issue is they LLMs are sycophantic by nature and we are seeing a lot of newly freed "geniuses" who have promised "no no no. You see! I know the secret to using them for good!"

It's like the one ring. If you start using it for doing anything beyond reformating, anything that requires critical thinking, you've already trapped yourself.

You'll feel like your work is quality when it isn't.

Personally I still think the quality of LLM code is crap for pretty much anything. Much better done by a well seasoned developer, which is harder to come by then people think. A LLM can help in some narrow cases but not many.

Was the AI you're using trained like most; scrapping the internet and disregarding the licenses of code?

using AI is now common practice for developers of all levels

is not a fact.

but one person standing in front of their (in part) dice-rolled "work" is not a welcomed sight is one.

any dev much rather would brown their own greenfields than help you regreen your AI-brownies...

So many critical bugs and security holes have been made from an oversight of the people handling the code.

Now you want to tell me that instead of having people write code that tries to make sense, and then review it (sometimes a bit too late), you want to have an hallucination machine produce some code randomly, then have people "fix" it, then review it?

This is just a recipe for disaster.

AIs are not "AIs", they're just bullshit generators that everyone is falling for. Technical debt and lack of code reliability were the main problems of software dev, and AIs are sacrificing those two specifically, just in exchange for the illusion of speed.

If you train monkeys to pile up bricks, it doesn't make a house, it makes a disaster waiting to happen. And monkeys, unlike AIs, are actually intelligent and sentient, which would make them more reliable still.

Some communities have "no-AI" rules. If you didn't break any, maybe you've been targeted by moderators that partake in cancel culture?

If that's the case, at least helps to sift through communities. And worse comes worst, maybe start a personal community to share what you make?

It's a broad topic. Everytime I see some new AI-coded project linked in the selfhosted community, it's kinda shit... I had hallucinated installation instructions. Very overexagerrated claims of what it's supposed to do... Sometimes it looks okay but some buttons don't do anything and then I look at the code and everything is more of a stub. Some projects have ridiculous security issues like someone finds a master key buried in the code, and of course none of the "developers" ever noticed because noone ever had a look at the code...

You're somewhere in the same territory. Maybe you're the one who gets it applied properly. But once I'm going to notice the tell-tale signs of vibe-coding, I'm going to start looking at it with the prejudice that got shaped by my prior experience. And I tend to be right most of the times.

But with that said, I don't think it's healthy to have a war over it, ban people and yell at each other. Most I want is transparency. I think all software projects should just disclose if and how they use AI, to what extent. And the users can make up their mind.

And with cryptography code... Isn't that a bit dangerous? From my own experience, AI models tend to learn a lot of example code and the standard documentation of libraries... Wikipedia articles and such... And then generate responses closer to that, than completely new thoughts... But(!) all these examples, tutorials and boilerplate code use a lot of shortcuts to explain it in simpler terms. Shortcuts that weaken security. And I wouldn't be surprised if your AI is then going ahead to reproduce that, and casually forget about the steps to prepare the numbers and follow up on the next steps if that wasn't ever in the Wikipedia example code. And I've seen a lot of wrong advice on StackOverflow and Reddit, so you better hope it also didn't internalize that. There's some fairly common myths about security or cryptography details out there. And I never know if your average Claude learned more from Reddit discussions, or from computer science technical literature... And you probably used Claude to skip reading the computer science books as well (and have a really close look at the code), or you probably would have just typed it down yourself. So I'd expect your software to be roughly as sound as newbie code, up to the average of projects that's out there on GitHub, which your AI has probably learned from. Not any better than that.

Why is your App cryptography-heavy if it's a messanger? Don't you just have to call msg.encrypt() or similar and then the library handles the rest?

You might be expecting too much nuance from online communities. It's easy and fun to oversimplify and dunk on a perceived common enemy. Lemmy has a very AI critical community. I imagine on reddit you might get less backlash, at least depending on the community. You might also find more AI friendly places here. In any case, trying to fight against a community bias is often a fools errand. I'm sure your code isn't slop, but I don't think you'll be able to change the minds of random, biased people on the internet with no incentive to really listen to you anyways.

I'm sure you already know all the reasons why people are against AI and are sick of having to defend yourself. Still, I want to add that even if you use AI as a tool instead of vibe-coding, as a consumer I wouldn't trust any privacy/security critical software that's developed with the use of AI. As a layman I can't check how secure your software is, so I have to rely on simple signifiers to make my judgements. At this point in time, AI is a red flag for me for security reasons alone. I know it's not "fair" or "accurate", but I don't have the time and knowledge to individually check every software to that extend. I know allegedly every programmer now uses AI in some form to code (I personally don't and most people I know don't either, but I'm sure it's just my bubble), but it's not a sign of quality code in my mind.

Another thing I want to add is that your hammer comparison should probably include how the hammer was produced and how much resources your hammer consumes to function. There is a strong ethical argument against the use of AI for most use cases. I'd include coding and code reviews. Again, that doesn't make your code slop, but it might help you understand why so many people are ready to dismiss it as that.