In an ever-evolving technological landscape, Large Language Models (LLMs) and generative AI are becoming game-changers, offering innovative ways to automate routine business activities. One such innovation is in the realm of Human Resources (HR) management, where chatbots have emerged from their nascent and somewhat annoying phase to become genuinely useful tools.
Read MoreHardening Signal Messenger with Formal Verification
Ilia Zaichuk, proof engineer at Digamma.ai
You’ve probably heard of Signal, right? It’s that messaging app that doesn’t suck. Okay, it might not have all the fancy features that some other apps have, but at least with Signal, you’re not handing over your private chats to the likes of Mark Zuckerberg or the NSA.
Now, I’m not here to get you to use Signal or to tell you it’s the ultimate secure messaging app. Actually, I’m here to say it could be even more secure! Sure, it’s good enough for sharing cute pics of your pup, but it’s not quite ready for something as important as, say, nuclear codes.
The thing is, Signal is built on some seriously strong math, using algorithms that claim to offer top-notch security and privacy for users. If these algorithms are implemented right, they should be pretty solid. But that’s the big question – is Signal’s code as trustworthy as the math it’s based on?
Luckily, there’s a way to find out. There are techniques that can actually prove, mathematically speaking, that Signal’s algorithms, protocols, and code are on point, making it super secure. These techniques are called formal verification. But before we dive into how that works, let’s take a closer look at what Signal promises in terms of security.
Read MoreHow to Discover and Prevent Linux Kernel Zero-day Exploit using Formal Verification
Recently a zero-day exploit (CVE-2021-31440) was found in the Linux kernel eBPF module. We will show how this bug could have been discovered and prevented using formal verification. A relatively simple logical error caused this bug, but it is easy to overlook and could lead to grave security implications. The bugs like this are difficult to find via exhaustive testing as the space of value combinations you need to test to stumble on it is relatively big. The typical way to find these bugs is by expert code reviews. Formal verification is offering another way to prevent or find bugs like this. Instead of spending the expert’s time pouring over the code looking for potential bugs, the specification is created, formally stating what the code is supposed to do. Then, using a proof assistant, a proof is developed that the given implementation satisfies this specification. If this proof is successful, it provides a bullet-proof guarantee that the code is correct wrt spec. Sometimes, as we will see in this example, the correctness could not be proved, which indicates that the implementation contains a bug. In this example, we will:
- Write a formal specification.
- Try to prove correctness for the buggy version of the code.
- Prove the correctness of the patched version of the code.
Purple Turtle Google Assistant Action
Not only has the recent wildfire crisis throughout the American west had a devastating effect on the local environment and the people living in affected areas, but the effects have become wide-spread across the nation as weather patterns carry thick smoke outside of the immediate wildfire areas. As air quality plummets, a significant risk is posed to communities. In a scientific study by the Climate Central Organization, it was found that following the San Diego wildfires of 2007, emergency room diagnoses for respiratory syndrome went up by 25%, while asthma diagnoses doubled. During the 2003 California wildfires, pregnant women were noted to have lowered birth weights, and children were 2-4 times more likely to develop respiratory problems. Read More
Digamma.ai’s guide to remote work. Tools, tips and best practices.
With the number of COVID-19 cases rising, government officials around the world are taking various measures to stop the virus spread by canceling events, issuing warnings against public gatherings and closing offices. Many organizations are faced with the reality of remote work and not all of them are ready. Read More
Digamma.ai was selected to receive Microsoft AI for Earth Innovation Grant

We are very excited to announce that Digamma.ai was selected to receive Microsoft AI for Earth Innovation Grant to apply Artificial Intelligence to help understand and protect the planet. Read More
New Office Space in Kiev

Earlier this month, Digamma.ai Kiev branch moved into a new, larger office space to accommodate business growth. Instead of trying to fit into an existing office space, we opted to design and build one from scratch. We carefully selected a location that provides convenient access by public transportation or car, located in a secure, business-friendly neighborhood with nearby local facilities like hotels, restaurants, and cafes. As we did not need a whole building, we opted to lease a floor in a modern business center with 24-hour access, security, and a cafeteria. Read More
Designing Chatbot Dialog Management
People are always fascinated by intelligent devices, and today they are software “chatbots”, which are becoming more and more human-like and automated. The combination of an immediate response and a permanent connection makes them an attractive way to expand or replace the web applications. The high-level diagram of an architecture for a chat-bot shown in Figure 1. Natural Language Understanding component tries to determine the purpose of the user’s input (intent) and useful data (entities). Also, the chatbot has a Dialog Manager to define the flow of conversation and paths that the system will take. Finally, a Language Generation component generates user output. Read More
Fast color transfer based on image statistics
Color transfer is a long-standing problem that seeks to transfer the color style of a reference image onto a source image. By using different references, one can alter the color style without changing the original image content in order to emulate different illumination, weather conditions, scene materials, or even artistic color effects. It can be used for color correction for rendered imagery, artistic style transfer, turning a day scene into a night scene, image analogies. Read More
Adoption of AI in Healthcare, insights from HIMSS19
Last month, we’ve attended HIMSS19. If you are not familiar with the event, Healthcare information and Management Systems Society (HIMSS) is an annual healthcare information conference, which brings together more than 45,000 healthcare and information technology professionals from all over the world.
Artificial Intelligence was a big topic at HIMSS this year. On Monday, we attended “Machine Learning and AI for Healthcare” pre-conference event where health systems, technology companies and clinicians discussed their efforts to utilize AI and Machine Learning to improve healthcare system, boost medical outcomes and reduce costs.