Що працює (а що ні) при продажу формальних методів!

Орігінальна стаття Майка Додса від 8 травня 2025 року про те що допомогає продавати формальні методи для мене дуже інтимна, так як вона говорить про дуже делікатні і важливі речі - як розмовляти про важливість формальних методів. Тому питання - перекладати, чи не перекладати для мене взагалі не стояло.

Ця стаття розпочала своє життя як доповідь, яку я провів наприкінці 2024 року.

Я люблю формальні методи — варто сказати це на початку, тому що ця стаття здебільшого про те, що не працює при спробах реалізувати проєкти з формальними методами. За останні 20 років формальні методи суттєво розвинулись, і я з гордістю можу сказати, що компанія Galois зробила свій внесок у цей успіх. Я зробив багато помилок під час планування та реалізації проєктів із формальними методами. Хотілося б, щоб інші змогли уникнути тих пасток, у які я потрапив, і, можливо, зробили б інші — більші й цікавіші — помилки.

За роки роботи в Galois я брав участь у багатьох продажних дзвінках. Я цього не очікував — думав, що займатимусь прикладними завданнями у сфері формальних методів. Але виявилося, що для того, щоб займатися дослідженнями для промисловості, спершу потрібно знайти відповідні промислові проєкти — а це передбачає продажні дзвінки. У результаті я спілкувався з багатьма людьми, які, можливо — лише можливо — захочуть реалізувати проєкт разом із Galois. Ось типовий приклад такої взаємодії:

Така розмова може піти в одному з двох напрямків: або нам вдається окреслити проєкт (ура!), або ми не можемо знайти проєкт, який цікавить клієнту (на жаль). Обидва варіанти дають досвід, хоча, звісно, перший — приємніший. Проте другий трапляється набагато частіше — здебільшого нам не вдається знайти проєкт із формальними методами, який би був корисний клієнтові. Це розчаровує, але водночас і викликає інтерес. Чому так?

Коли ви розмовляєте з потенційним клієнтом, ви намагаєтесь з’ясувати, що для нього важливо. У клієнтів на кону справжні гроші, тому вони дуже дбають про те, щоб отримати те, що їм справді потрібно. Доволі часто я помічав, що мої первинні інтуїції виявляються просто хибними. Я кажу: «Ну, ви як представник <такої-то> індустрії очевидно хочете ось це», а клієнт відповідає: «Ні, нас це не цікавить». З часом я усвідомив, що це насправді добре. Коли хтось прямо каже, що ти помиляєшся — це допомагає загострити інтуїцію, щойно ти подолаєш удар по власному его.

З роками в мене сформувалися певні уявлення про те, що працює, коли намагаєшся визначити рамки проєкту з формальними методами. Я зовсім не вважаю, що ці висновки є абсолютно новими, але я рідко бачу їх у обговореннях, і часто вони трохи відрізняються від загальноприйнятої думки в дослідженнях з формальних методів. Почнімо з основ.

Світогляд: Витрати проти вигод

Мій базовий світогляд доволі простий. Будь-який проєкт має очікувані витрати та вигоди. Існує певна індивідуальна для клієнта межа беззбитковості, вище якої проєкт має сенс. Якщо ж проєкт “нижче цієї лінії”, тобто занадто витратний — його реалізація не виправдана.

Тут я маю на увазі загальну, “цілісну” вартість: час, гроші, людей, ресурси — усе, що потребує зусиль з боку вашої організації; і загальну вигоду, таку як безпека, надійність, економічна цінність, задоволення, можливість спокійно спати вночі, й інші подібні речі. І, звісно, межа беззбитковості — це не пряма лінія, а, ймовірно, складна багатовимірна поверхня. Це дуже абстрактна й доволі неточна модель реальності. Але в певному сенсі вона відображає те, як ми приймаємо рішення в повсякденному житті: щось дешеве й дуже корисне — скоріш за все, варто зробити, а щось дороге й малокорисне — скоріш за все, не варто.

Потенційні замовники формальних методів загалом поводяться раціонально, коли йдеться про витрати та вигоду. Вони знають, що є пріоритетним, а що — ні. У них обмежений бюджет на проєкти, і вони зважують один проєкт проти іншого. Ті проєкти, які з точки зору співвідношення витрат і вигод мають сенс — реалізуються, а ті, які не мають — не реалізуються.

Це звучить майже як трюїзм — тож яка з цього користь? Справа в тому, що я часто бачу нерозуміння того, чому формальні методи не впроваджуються ширше. На мою думку, пояснення досить просте: багато потенційних проєктів з використанням формальних методів просто не мають сенсу з погляду балансу витрат та майбутної вигоди.

Іноді в дослідженнях з формальних методів ми говоримо про те, що можливо зробити. Наприклад, сьогодні ми маємо чудові проєкти, як-от SeL4, CompCert і HACL, які демонструють, що можливо створювати системи, корисні для промисловості, із формальними гарантіями. Це велике досягнення, але всі ці проєкти були профінансовані як дослідницькі ініціативи. Якщо ми хочемо бачити більше проєктів із формальною верифікацією, то ці проєкти мають бути не лише технічно можливими, а й ціннішими для клієнтів, ніж будь-що інше, на що вони могли б витратити свої ресурси.

Я далі поділюся кількома конкретними думками щодо визначення рамок проєктів з формальними методами. Але моя головна теза проста: проєкти мають мати сенс з точки зору витрат і вигод. Ось і все.

1: Проєкти мають приносити цінність на ранніх етапах

Я досить швидко зрозумів, що проєкти з формальними методами не реалізуються одним великим стрибком. Натомість ви поступово вкладаєте певні ресурси — і поступово отримуєте вигоду, доки не досягнете масштабнішої мети. Ось типовий вигляд кривої витрат-вигод, яку ми часто спостерігаємо в проєктах з доведенням теорем:

На цьому етапі ви створюєте початкові визначення, доводите кілька лем, а тоді переходите до основної теореми. Проблема в тому, що до моменту, поки не доведено головну теорему, ви майже не отримуєте жодної вигоди. Така крива співвідношення витрат і вигод абсолютно не підходить більшості клієнтів. Дуже далеко по цій кривій ви вже витратили багато грошей, часу, зусиль команди — а показати ще особливо нічого. Звісно, пізніше ви отримаєте значні вигоди, але це буде дуже пізно і дуже дорого.

Я часто опиняюся в такій ситуації. Клієнт каже: «Я читав ваші блоги, мені дуже цікаві формальні методи! Що я отримаю за X місяців і Y доларів?» Ми разом дивимось і розуміємо: «О ні… X місяців, Y доларів — це не так вже й багато! Ми… можемо написати початкові визначення за ці гроші.»

І тоді я звертаюся до потенційного клієнта і кажу: «А як щодо того, щоб витратити в чотири рази більше часу і вісім разів більше грошей?» І зазвичай після цього… клієнт більше не передзвонює.

У ідеалі невеликі витрати мають приносити невелику, але реальну вигоду. Наприклад, у Проєкті 1 ми використовуємо певну суму X, і клієнт бачить конкретний результат. Можливо, ми знаходимо кілька помилок або даємо клієнтові впевненість у правильності невеликого компоненту системи. І ще краще — клієнт задоволений і каже: «Давайте зробимо ще один проєкт!» Тоді ми запускаємо Проєкт 2 — більший за масштабом. І так ми можемо поступово піднімати криву цінності.

Інструменти формальних методів часто не дозволяють нам так гнучко визначати рамки проєктів, оскільки вони потребують великих початкових витрат, перш ніж ми отримаємо якісь вигоди. Потрібно писати специфікації, будувати доведення, розбиратися в предметній області, навчати інженерів, іноді — навіть клієнтів, а подекуди — ще й створювати нові інструменти. Отримати миттєвий прибуток від інвестицій у ці інструменти дуже складно.

Фахівці з формальних методів люблять кепкувати з тестування. Але перевага тестування в тому, що дуже легко запустити кілька тестів і знайти кілька багів. Напишеш ще кілька тестів — і, ймовірно, знайдеш ще кілька багів. Це дає дуже привабливу криву витрат і вигод:

Але ви можете заперечити: «Ага, зате за допомогою тестування дуже важко досягти високого рівня коректності. Формальні методи тут перемагають!» На жаль, у мене для вас погана новина — і це моя друга «гостра» теза:

2: Коректність неважлива

Це правда. Нікому не цікава коректність.

Я не хочу бути надто провокативним. Звісно, якщо ваш код взагалі не робить те, що мав би, — це проблема. Розробники справді витрачають багато зусиль на пошук і виправлення помилок. Але в формальних методах ми часто прагнемо набагато вищого стандарту — системи, яка буде повністю коректною, принаймні щодо певної специфікації.

На жаль, багато розробників не зацікавлені у досягненні цього вищого рівня коректності. Їхні поточні інструменти працюють достатньо добре, вони вже «заклали в бюджет» існування багів і проблем з безпекою. Для них цінність від меншої кількості помилок або більшої безпеки фактично дорівнює нулю — тож якщо новий інструмент коштує хоч щось, він уже занадто дорогий.

Це справедливо навіть для систем із високими вимогами до надійності, що завжди мене дивувало. Здавалось би, якщо йдеться про речі, які літають чи їздять, то ви точно хочете, щоб у них було якомога менше помилок. Але часто компаніям або людям, які розробляють та підтримують ці системи, справді байдуже, або тому, що вони вже врахували ризик багів, або тому, що їхня система спроєктована так, щоб бути стійкою до помилок.

Добре це можна зрозуміти, якщо усвідомити, що розробники стикаються з безліччю конкурентних вимог, і в багатьох випадках є важливіші речі, ніж коректність або безпека. Наприклад, команда може надавати перевагу: впровадженню нових функцій для безпеки, виправленню вже відомих проблем, розширенню команди розробників, зменшенню технічного боргу, задоволенню вимог замовників чи ринку. Ще гірше: технологія, яка підвищує коректність, може ускладнити або подорожчати інші цілі. Наприклад, переписати систему на СуперМові X звучить круто, але це може ускладнити найм розробників — і це суттєва витрата для більшості організацій.

Ось історія, яка добре ілюструє цю думку. Один із моїх колег із Galois спілкувався з керівником компанії, що створює системи з високими вимогами до надійності. І ось як пройшла розмова:

Ця відповідь у мене викликає легкий вибух мозку. Тож варто розібратися, чому так може бути. Цей розробник вважає, що їхній поточний процес забезпечення надійності та безпеки вже працює добре. Вони переконані, що їхня система вже надійніша та безпечніша, ніж у конкурентів. І найголовніше — продажі їхньої продукції не залежать від рівня надійності чи безпеки. Отже, якась нова “модна” технологія для забезпечення коректності лише додасть витрат (навчання, інженерні зусилля, притирки під час розробки), і, з їхньої точки зору, не принесе жодної реальної вигоди.

А тепер — найцікавіше. Той самий колега з Galois продовжив розмову, і вона пішла так:

Це теж змушує мій мозок трошки вибухнути, бо хіба ж тестування на відповідність стандартам не повинно стосуватися коректності та безпеки? Насправді — ні. Для досягнення відповідності потрібен дуже конкретний, регламентований процес, і для цієї компанії він надзвичайно ручний. Їм доводиться самостійно писати мільйони тестів, і це виснажує інженерну команду.

Це уповільнює графік випусків, зменшує гнучкість команди, і складно знайти людей, які б цим займалися. Але без цього тестування вони просто не можуть продавати продукт. А це вже критично — бо безпосередньо впливає на продажі, тобто на бізнес.

Іншими словами: вигоди, які важливі нам (наприклад, коректність і безпека) — можуть не збігатися з вигодами, які важливі потенційному клієнту, з яким ви розмовляєте (наприклад, швидкість, вартість, можливість найму персоналу).

Клієнти хочуть, щоб проєкт вирішував їхні проблеми — а це означає, що потрібно розуміти, що для них означає успіх.

3: Визначити та пояснити успіх складно

Отже, ви знайшли клієнта, який хоче зробити проєкт. Тепер потрібно домовитися, що саме ви будете робити. Ось карикатура результатів формальних методів:

• У вас є артефакт, який дає точне технічне визначення деякої властивості — наприклад, теорема на тисячу рядків у формальній мові.

• Ви маєте високу впевненість, що ця властивість виконується, бо провели формальні методи — доведення у Lean чи чомусь подібному.

Проблема в тому, що точне значення цієї теореми дуже важливе, але ваш клієнт, ймовірно, не розуміє, що це означає.

(Іноді навіть ви, як експерт, можете не мати достатньо глибокого розуміння того, що означає теорема. Наприклад, формальні докази ядра seL4 підтверджують, серед іншого, що реалізація ядра на C точно відповідає абстрактній моделі ядра. Це справді потужний і вражаючий результат, але щоб його зрозуміти, потрібно детально вивчати формальну модель. Я особисто ретельно не читав модель, і, мабуть, більшість користувачів seL4 також не читали. Замість цього ми покладаємося на узагальнені уявлення — «ядро seL4 було формально верифіковане».)

Цей розрив у розумінні створює кілька проблем при визначенні рамок проєктів. По-перше, як клієнт може знати, що отримує саме те, що хоче? По-друге, як пояснити компроміси між різними варіантами? І нарешті, проблема, з якою ми стикалися у багатьох проєктах: Як зрозуміти, коли роботу можна вважати завершеною?

Ось один спосіб пояснити результати формальних методів, який я не рекомендую:

Клієнт на цьому етапі дуже задоволений. Але потім проходить три місяці, і клієнт телефонує вам:

Проблема в тому, що клієнт не зрозумів, що саме він отримує. Можливо, баг не покритий доведенням, або доведення технічно допускає поведінку, яку вони вважають багом, або навіть вони змінили щось важливе й порушили ключове припущення доведення. Вони не мали достатньо чіткого розуміння результату, щоб передбачити чи уникнути цих проблем. Ймовірно, у них також немає достатньо чіткої моделі, щоб пояснити, що відбувається, тому все, що вони почують, — це ваші суперечки і спроби перекласти провину.

(Це також повертає нас до теми витрат і вигод. Клієнт не зрозумів справжню користь від того, що ви йому надали.)

Ось трішки краща версія такого пояснення.

Це в певному сенсі краще, бо принаймні клієнт правильно розуміє, що він спантеличений. У деяких випадках це може бути прийнятно. Можливо, клієнт довіряє вам і вірить, що ви зможете самі визначити, що важливо. Але все одно це не дуже задовольняє.

Я вважаю, що ще трохи кращий спосіб пояснення, який ми застосовували в деяких проєктах, і він виглядає приблизно так:

Ми так робили в проєкті AWS LibCrypto. Ось сторінка з 30 чи 40 різними застереженнями, які чітко окреслюють, що саме означають ці доведення.

Цей підхід забирає багато часу і залежить від того, наскільки технічно підкований клієнт і скільки часу він може виділити на обговорення. Він також не повністю усуває непорозуміння. Застереження дуже технічні — щоб зрозуміти, що означає конкретне застереження, потрібно розуміти AWS LibCrypto. Але водночас застереження набагато більш абстрактні, ніж реальні технічні теореми. Тож потенціал для плутанини все одно є, але принаймні розрив між розумінням клієнта і справжнім результатом зменшився.

Є ще одна тонша проблема, з якою ми стикалися: застереження з часом «згладжуються» у процесі внутрішнього пояснення. Тому можна побачити таку схему:

• Galois: [технічні результати, технічні застереження]
• Інженерна команда клієнта: [спрощені результати, спрощені застереження]
• Технічний директор клієнта: [спрощені результати]
• PR-команда клієнта: «Galois довів, що В НАШІЙ СИСТЕМІ НІЯКИХ БАГІВ НІ»

Це не означає, що хтось навмисно вводить в оману. На кожному рівні більш технічна людина дає пояснення менш технічній. Але в результаті клієнт отримує глибоке непорозуміння щодо того, що саме йому надали. Потім через три місяці знаходять жахливий баг, і всі сердяться на вас.

Припустимо, ви отримали такий дзвінок — страшний баг, клієнт сердиться. Тепер потрібно зрозуміти, чи це проблема, яку вам треба виправити. Загалом, вам потрібно мати чіткі межі проєкту, щоб можна було правильно оцінити обсяг роботи і оголосити проєкт завершеним. Саме тому дуже важливо якомога детальніше погоджувати цілі — наприклад, із переліком застережень, як ми робили для AWS LibCrypto. Найгірший варіант — це коли ви говорите клієнту: «Гарні новини, ми закінчили», а він відповідає: «Ні, ви не закінчили, потрібно прибрати ці застереження».

На жаль, мій досвід показує, що важко передбачити вартість проєктів з формальними методами. Головна причина — невеликі відмінності можуть радикально змінити вартість доведення. Наприклад, у доказах AWS LibCrypto ми перевірили дві різні варіації основних теорем. Перша працювала для фіксованих розмірів ключів, друга — для будь-якого розміру. Інтуїтивно обидва докази дуже схожі, але з технічних причин друга версія вимагала майже такої самої кількості роботи з нуля. Не дуже добре! Також ми часто бачимо, що вартість верифікації визначається кількома особливо складними рядками коду, і наперед важко сказати, які саме будуть проблемними.

Все це означає, що успіх проєкту в термінах часу і бюджету часто залежить від конкретних технічних особливостей, які хоче клієнт. Але, як ми вже бачили, клієнту зазвичай дуже складно зрозуміти, що ці застереження для нього означають.

4: Спочатку робіть дешевші речі

Добре, у вас є клієнт, який хоче реалізувати проєкт. Строки підходять, їх турбує коректність, і вони клянуться, що розуміють теорему. Потім вони дивляться вам в очі і питають: «Скажіть чесно, це дійсно найкраще використання грошей?». Ви бачили їх тестовий набір (якого не існує), і ви відповідаєте: «ем…».

Проблема в тому, що проєкти з формальними методами дорогі, а дешеві техніки — дійсно дешеві!

Я вважаю, що існує приблизна ієрархія технік, які можна використовувати для підвищення надійності та безпеки програмного забезпечення. На верхівці — такі речі, як код-рев’ю та документація, тестування, розробка з використанням CI/CD та подібне. Далі йдуть більш формальні методи, наприклад, фаззинг або property-based тестування. І внизу — серйозні формальні методи:

Дешеві методи на верхівці ієрархії насправді дуже ефективні, і саме так будується більшість систем. Наприклад, розробка програмного забезпечення з використанням CI/CD дуже успішно запобігає помилкам. І, звичайно, більшість процесів розробки програмного забезпечення у світі взагалі не використовують формальні методи. Але також правда, що багато проєктів або не застосовують дешеві методи забезпечення якості, або використовують їх явно недостатньо. Подумайте про всі ті проєкти з маленькими наборами тестів або відсутністю практик код-рев’ю.

Через це часто буває складно порадити клієнту, що йому потрібен проєкт з формальними методами. Припустимо, у нас є два можливі проєкти: «застосувати формальні методи» і «написати більше тестів»:

Окрім того, що проєкт із написанням більшої кількості тестів дешевший, він має й інші переваги. Інструменти для тестування, як правило, більш зрілі, ніж інструменти формальних методів, тому проєкт, ймовірно, буде більш передбачуваним. З тієї ж причини його легше укомплектувати кадрами. І хоча рівень гарантій нижчий, клієнт, ймовірно, зможе спробувати кілька різних методів забезпечення якості за ту ж саму вартість, що й проєкт із формальними методами, або ж спрямувати ресурси на кілька підсистем.

Це робить дуже складним виправдання багатьох проєктів із формальними методами. З погляду прихильників формальних методів я бачу два можливі підходи.

Перший підхід (я називаю його «золоте оздоблення») — застосовувати формальні методи лише після того, як усі інші, дешевші методи були використані максимально ефективно. Думаю, це описує багато проєктів у сфері формальних методів сьогодні. Наприклад, у нашій верифікації AWS-LibCrypto ми перевіряли код, який переважно походив із OpenSSL, через BoringSSL, а потім AWS-LibCrypto. Основна криптографічна бібліотека — важливий елемент інфраструктури безпеки, тому цей код протягом багатьох років був ретельно проаналізований і перевірений. Наш проєкт верифікації став завершальним етапом, який надав непорушну впевненість у правильності бібліотеки.

Проблема в тому, що це дуже обмежує цільовий ринок для формальних методів — лише на небагато критично важливих для безпеки компонентів, які використовують найбільш обережні та забезпечені організації світу.

Другий підхід (який я називаю YOLO, бо це дуже круто) — стверджувати, що формальні методи можуть замінити всі інші, дешевші методи. Формальні методи — це все, що вам потрібно! Це звучить чудово, але насправді так не в більшості випадків. По-перше, такі підходи, як код-рев’ю та документація, мають корисні побічні ефекти, окрім просто підвищення впевненості у системі. По-друге, ті набридливі вимоги сертифікації, про які я згадував раніше, часто вимагають певних типів тестування. І просто факт у тому, що формальні методи — це новинка, тому більшості людей складно їм довіряти без підтримки більш знайомих методів.

Я вважаю, що це аргумент на користь тіснішої інтеграції формальних методів і дешевших технік. Замість або–або, чому б не поєднати обидва? Це ідея, яку ми досліджуємо у CN — інструменті для тестування та верифікації С-коду, який Galois допомагає розробляти разом із партнерами, зокрема Кембриджським та Пенсильванським університетами.

Ключові важелі: витрати проти вигод

Іноді я чую, як люди стверджують, що формальні методи безперечно кращі за техніки, які здебільшого використовують сьогодні програмні інженери. Єдина причина, чому формальні методи не стали популярнішими (згідно з цією теорією), — це те, що інженерні команди не поінформовані, консервативні або їх відштовхують поверхневі труднощі, як-от незручні інтерфейси та погана документація. Я не думаю, що це зовсім правильно. Моє спостереження полягає в тому, що інженери переважно раціональні, коли оцінюють витрати та вигоди, принаймні в межах своїх конкретних систем і проблем.

Це означає, що коли ми маємо якусь формальну методику, яка здається недооціненою, у нас є фактично два важелі, які ми можемо задіяти. Ми можемо зробити її або дешевшою або більш корисною. Одна річ або обидві можуть допомогти проєкту перейти межу беззбитковості.

Згадайте, що ми говоримо про загальні витрати й загальні вигоди. Вигоди можуть включати безпеку, можливість продавати продукт, відповідність стандартам тощо. Витрати — це люди, час, гроші, ресурси. І все це — щодо дуже конкретної межі беззбитковості для кожного окремого клієнта. Те, що не має цінності для одного клієнта, може виявитися надзвичайно цінним для іншого.

Лінія витрат має велике значення, особливо людська вартість — навчання, підтримка, використання інструментів. Але я вважаю, що рух уздовж лінії вигод іноді може бути простішим, адже це означає створення інструментів, які вирішують конкретні проблеми клієнта. Кожного разу, коли Galois виконує проєкт для клієнта, ми дізнаємося щось нове, наше співвідношення витрат і вигод покращується, і наступного разу ми можемо робити більш цікаві помилки.